CristalCaveGem » LustreC

12/01/2014

11:37 PM Revision 3d134f43 (lustrec): Doc file

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@377 041b043f-8d7c-46b2-b46e-ef0dd855326e Pierre-Loïc Garoche

11:37 PM Revision 24d59df8 (lustrec): Doc file

Pierre-Loïc Garoche

11:35 PM Revision bd612a7b (lustrec): Removed oasis, now use the classical autoconf; ./configure; make

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@376 041b043f-8d7c-46b2-b46e-ef0dd855326e Pierre-Loïc Garoche

11:35 PM Revision a8e66e98 (lustrec): Removed oasis, now use the classical autoconf; ./configure; make

Pierre-Loïc Garoche

11:32 PM Revision 1e48ef45 (lustrec): - Dealt with compiling lusic from distant lusi files.

- Header now do not allow the generation of function previously declared as C prototype
git-svn-id: https://cavale... Pierre-Loïc Garoche

11:32 PM Revision 5ae8db15 (lustrec): - Dealt with compiling lusic from distant lusi files.

- Header now do not allow the generation of function previously declared as C prototype Pierre-Loïc Garoche

03:13 PM Revision 17db36ed (lustrec): Small update

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@374 041b043f-8d7c-46b2-b46e-ef0dd855326e Eric Noulard

03:13 PM Revision 30a4debf (lustrec): Small update

Eric Noulard

02:53 PM Revision 615b63f1 (lustrec): Add first version of FindLustre.cmake

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@373 041b043f-8d7c-46b2-b46e-ef0dd855326e Eric Noulard

02:53 PM Revision 801f63fa (lustrec): Add first version of FindLustre.cmake

Eric Noulard

01:56 PM Revision 871b34d7 (lustrec): Added compilation and install of include/*.lusi

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@372 041b043f-8d7c-46b2-b46e-ef0dd855326e Pierre-Loïc Garoche

01:56 PM Revision c7879e4f (lustrec): Added compilation and install of include/*.lusi

Pierre-Loïc Garoche

12:58 PM Revision cb430a2b (lustrec): Add more functions in math.lusi

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@371 041b043f-8d7c-46b2-b46e-ef0dd855326e Eric Noulard

12:58 PM Revision ab51e2a7 (lustrec): Add more functions in math.lusi

Eric Noulard

11/27/2014

03:30 PM Revision d1baac41 (lustrec): corrected a bug that made an error silent, confusing users...

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@370 041b043f-8d7c-46b2-b46e-ef0dd855326e Xavier Thirioux

03:30 PM Revision 95763423 (lustrec): corrected a bug that made an error silent, confusing users...

Xavier Thirioux

11/15/2014

01:30 PM Revision 93d16170 (lustrec): Correct a bug in ensures stack generation related to existential

Guillaume Davy

11/13/2014

11:48 AM Revision 97602f7c (lustrec): Correct bug when there is no precondition and change reprensentation

of boolean in ACSL Guillaume Davy

10:59 AM Revision 690cde69 (lustrec): Added an option for let vs exists axiomatization

Pierre-Loïc Garoche

11/07/2014

04:59 PM Revision 81125539 (lustrec): Add lustrec files for ALT1 and ALT2

Guillaume Davy

04:29 PM Revision c306bf6b (lustrec): my notes

Pierre-Loïc Garoche

11/06/2014

09:31 PM Revision 052da31c (lustrec): add makefile

Guillaume Davy

02:54 PM Revision 65de0e13 (lustrec): ALT2 proved by framaC without human interaction

Guillaume Davy

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