Activity
From 11/19/2014 to 12/18/2014
12/18/2014
- 10:07 PM Revision d3a3e7e9 (lustrec): SMT2 file generated by frama-c/why3/z3-edit - it is the second base case of kinduction of ALT3. And it is not provable.
- 02:45 PM Revision 995bfad5 (lustrec): Add the script used to add k annotation to tests.
- 02:40 PM Revision 2bdbbe54 (lustrec): Add tests from fmcad with k annotation to new_backend branch
12/17/2014
12/16/2014
- 08:10 AM Revision af0ff493 (lustrec): Removed unused predicate
- 12:23 AM Revision 5b12f571 (lustrec): Example on possible encoding using the 5-inductive two counter example.
12/10/2014
- 11:15 AM Revision e3373485 (lustrec): Revert the commit 384 by Xavier: adding dirname to the source_name introduced a bug: the .h file is empty!!! Strange behavior.
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@387 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 11:15 AM Revision 13fa31c2 (lustrec): Revert the commit 384 by Xavier: adding dirname to the source_name introduced a bug: the .h file is empty!!! Strange behavior.
- 11:14 AM Revision 40875a30 (lustrec): Added an install target in the src folder
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@386 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 11:14 AM Revision 5d8ddbf7 (lustrec): Added an install target in the src folder
12/09/2014
- 04:54 PM Revision 790765c0 (lustrec): modified optimization info printout (option -print_reuse)
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@385 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 04:54 PM Revision 86b99b69 (lustrec): modified optimization info printout (option -print_reuse)
- 04:30 PM Revision 862ccfb1 (lustrec): supports again relative path for lustre source file (regression bug)
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@384 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 04:30 PM Revision fb8b1da7 (lustrec): supports again relative path for lustre source file (regression bug)
- 02:03 PM Revision 89a70069 (lustrec): added a new option -print_reuse that prints clock disjoint variables and reuse policy.
- useful for debugging and carrying correctness proofs to the C code level.
non trivial result only when option -O 3 o... - 02:03 PM Revision c825868a (lustrec): added a new option -print_reuse that prints clock disjoint variables and reuse policy.
- useful for debugging and carrying correctness proofs to the C code level.
non trivial result only when option -O 3 o... - 01:41 PM Revision e8b6d5ca (lustrec): Moved Makefile into src folder
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@382 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 01:41 PM Revision bed8ea64 (lustrec): Moved Makefile into src folder
- 01:29 PM Revision f6ce2ae9 (lustrec): New branch ... again
12/08/2014
- 09:09 PM Revision 58a463e7 (lustrec): Added a construct for Dependencies (was a tuple before) and a boolean attribute stateful
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@380 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 09:09 PM Revision 830de634 (lustrec): Added a construct for Dependencies (was a tuple before) and a boolean attribute stateful
- 09:06 PM Revision ff580eb7 (lustrec): Almost nothing
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@379 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 09:06 PM Revision a6208edd (lustrec): Almost nothing
- 02:36 PM Revision 3fd9f1f2 (lustrec): Properly handle generated files
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@378 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 02:36 PM Revision 76b2936d (lustrec): Properly handle generated files
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
- 11:37 PM Revision 24d59df8 (lustrec): Doc file
- 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
- 11:35 PM Revision a8e66e98 (lustrec): Removed oasis, now use the classical autoconf; ./configure; make
- 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... - 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
- 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
- 03:13 PM Revision 30a4debf (lustrec): Small update
- 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
- 02:53 PM Revision 801f63fa (lustrec): Add first version of FindLustre.cmake
- 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
- 01:56 PM Revision c7879e4f (lustrec): Added compilation and install of include/*.lusi
- 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
- 12:58 PM Revision ab51e2a7 (lustrec): Add more functions in math.lusi
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
- 03:30 PM Revision 95763423 (lustrec): corrected a bug that made an error silent, confusing users...
Also available in: Atom