pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2025-01-07 16:44:14 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

AbstractInterpretation: flow-insensitive analysis

Browse source
This commit is contained in:
Adam Chlipala 2016-03-05 18:36:39 -05:00
parent 062119d6a2
commit c568a047cd
2 changed files with 837 additions and 486 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1321
AbstractInterpretation.v
View file

File diff suppressed because it is too large Load diff

2
Frap.v
View file

@ -215,3 +215,5 @@ Ltac simplify_map :=
simplify_map' (m $+ (k, v)) tt ltac:(fun m' => simplify_map' (m $+ (k, v)) tt ltac:(fun m' =>
replace (@add A B m k v) with m' by maps_equal) replace (@add A B m k v) with m' by maps_equal)
end. end.
Ltac sets := Sets.sets ltac:(simpl in *; intuition (subst; auto)).