You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

Josh Berdine d72d83bfb4 [sledge] Freshen nested existentials also wrt ancestor universals ... Summary: Previously Sh had a representation invariant which ensured that existentials of a subformula did not shadow universals of its superformulas. The current implementation of Sh.freshen_nested_xs mistakenly still assumes this invariant, but it no longer holds. This diff fixes freshen_nested_xs to freshen nested existentials with respect to not only ancestor universals in addition to existentials. Reviewed By: jvillard Differential Revision: D25756551 fbshipit-source-id: 54c48b067		5 years ago
..
fol	[sledge] Use unsat context and ff pure constraints in unsat symbolic heaps	5 years ago
llair	[sledge] Additional tracing	5 years ago
test	[sledge] Use unsat context and ff pure constraints in unsat symbolic heaps	5 years ago
control.ml	[sledge] Change execution options from a record to a module	5 years ago
control.mli	[sledge] Change execution options from a record to a module	5 years ago
domain_intf.ml	[sledge] Remove dead Domain.is_false	5 years ago
domain_relation.ml	[sledge] Remove dead Domain.is_false	5 years ago
domain_relation.mli	[sledge] Represent function formal parameters and actual arguments in order	5 years ago
domain_sh.ml	[sledge] Delay unsat check in exec_assume until after simplify	5 years ago
domain_sh.mli	[sledge] Represent function formal parameters and actual arguments in order	5 years ago
domain_unit.ml	[sledge] Remove dead Domain.is_false	5 years ago
domain_unit.mli	[sledge] Rename lib to src	5 years ago
domain_used_globals.ml	[sledge] Remove dead Domain.is_false	5 years ago
domain_used_globals.mli	[sledge] Change execution options from a record to a module	5 years ago
exec.ml	[sledge] Delay unsat check in exec_assume until after simplify	5 years ago
exec.mli	[sledge] Delay unsat check in exec_assume until after simplify	5 years ago
llair_to_Fol.ml	[sledge] Strengthen dynamic resolution of indirect calls	5 years ago
llair_to_Fol.mli	[sledge] Strengthen dynamic resolution of indirect calls	5 years ago
report.ml	[sledge] Statically resolve known function calls	5 years ago
report.mli	[sledge] Add coverage statistics to test report	5 years ago
sh.ml	[sledge] Freshen nested existentials also wrt ancestor universals	5 years ago
sh.mli	[sledge] Rename Sh.is_false to is_unsat	5 years ago
solver.ml	[sledge] Rename Sh.is_false to is_unsat	5 years ago
solver.mli	[sledge] Reorganize first-order logic support into separate library	5 years ago
stop.ml	[sledge] Rename lib to src	5 years ago
stop.mli	[sledge] Rename lib to src	5 years ago