Correct some problem related to new bool encoding
SMT2 file generated by frama-c/why3/z3-edit - it is the second base case of kinduction of ALT3. And it is not provable.
Add tests from fmcad with k annotation to new_backend branch
Correct a bug in ensures stack generation related to existential
Correct bug when there is no precondition and change reprensentationof boolean in ACSL
Add lustrec files for ALT1 and ALT2
my notes
add makefile
ALT2 proved by framaC without human interaction
add coq proof
ALT_2 working with modification made by hand
Correct bug option exists
ALT2_inlined
Update on c backend proof
Two current frama c bugs
Bugfixes and coq proof generation for lemma inv_inv
Last version of frama-c. We should work from thisone.
modified guide 120 full
removed uncessary files
add coq support
Patch for frama-c/wp. Solve the typing bug
the frama-c typing bug
correct bug in proof printing
playing with ALT2
k steps
Lustre contracts version of ALT2.lus
removed GUIDE_150
added tcm code