CristalCaveGem » LustreC

11/05/2014

05:16 PM Revision 8107d368 (lustrec): add coq proof

Guillaume Davy

05:15 PM Revision bff13707 (lustrec): ALT_2 working with modification made by hand

Guillaume Davy

10:46 AM Revision a93ebdab (lustrec): Correct bug option exists

Guillaume Davy

09:48 AM Revision 7b01bcd2 (lustrec): ALT2_inlined

Guillaume Davy

09:29 AM Revision 23c510d0 (lustrec): Update on c backend proof

Guillaume Davy

11/03/2014

09:52 PM Revision 4865b45f (lustrec): Two current frama c bugs

Pierre-Loïc Garoche

10/29/2014

11:55 PM Revision 0ba542d7 (lustrec): Bugfixes and coq proof generation for lemma inv_inv

Guillaume Davy

10/27/2014

10:12 AM Revision f5fd1afd (lustrec): Last version of frama-c. We should work from thisone.

Pierre-Loïc Garoche

10/24/2014

04:45 PM Revision cc8e2ef3 (lustrec): modified guide 120 full

Teme Kahsai

06:33 AM Revision 99201654 (lustrec): removed uncessary files

Teme Kahsai

10/23/2014

01:00 PM Revision faa5c6db (lustrec): solved the bug of multiple definition of assert exists ...

Pierre-Loïc Garoche

12:59 PM Revision bd09b789 (lustrec): add coq support

Guillaume Davy

10:47 AM Revision d1c06a39 (lustrec): Expliciting asserts in C code

Pierre-Loïc Garoche

10/22/2014

03:26 PM Revision 498c7c82 (lustrec): Patch for frama-c/wp. Solve the typing bug

Pierre-Loïc Garoche

09:38 AM Revision 9d3480a4 (lustrec): the frama-c typing bug

Pierre-Loïc Garoche

08:58 AM Revision dc6c92b2 (lustrec): correct bug in proof printing

Guillaume Davy

07:55 AM Revision e3608bbf (lustrec): playing with ALT2

Pierre-Loïc Garoche

10/21/2014

11:18 PM Revision 14dfe3f3 (lustrec): k steps

Pierre-Loïc Garoche

11:13 PM Revision 41da3cf2 (lustrec): Lustre contracts version of ALT2.lus

Pierre-Loïc Garoche

10:42 PM Revision eb56a02a (lustrec): removed GUIDE_150

Teme Kahsai

10/20/2014

09:23 PM Revision 41e1bdd0 (lustrec): added tcm code

Teme Kahsai

10/13/2014

09:20 AM Revision e3945827 (lustrec): Push current status of proof backend

Guillaume Davy