Project

General

Profile

Activity

From 12/02/2014 to 12/31/2014

12/26/2014

10:18 PM Revision cc9e1901 (lustrec): Added results of the first analysis
Pierre-Loïc Garoche

12/23/2014

08:03 AM Revision 08bbd713 (lustrec): uploaded scripts
Pierre-Loïc Garoche
07:25 AM Revision e5d5c450 (lustrec): Mem limit + issues with log and pdflatex log
Pierre-Loïc Garoche

12/22/2014

10:21 PM Revision 13b22bd5 (lustrec): Solved some bugs in the scripts: invalid path for report style files and blocking pdflatex
Pierre-Loïc Garoche
04:36 PM Revision 0ec278d2 (lustrec): cleaning
Pierre-Loïc Garoche
04:28 PM Revision a06b22fd (lustrec): Moved scripts here
Pierre-Loïc Garoche
04:28 PM Revision 94a4b867 (lustrec): worklist for parallel
Pierre-Loïc Garoche
02:28 PM Revision 82398d1d (lustrec): Frama-C WP report templates
Pierre-Loïc Garoche
02:27 PM Revision 2b7729d4 (lustrec): On going work. Generating report focusing on proved vs unproved part
Pierre-Loïc Garoche

12/19/2014

11:04 PM Revision 6bc919cb (lustrec): Move gen_contracts.py
Guillaume Davy
10:50 PM Revision 4174a469 (lustrec): Correct some problem related to new bool encoding
Guillaume Davy
10:50 PM Revision 105b3645 (lustrec): Delete tests files that have no k
Guillaume Davy

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.
Pierre-Loïc Garoche
02:45 PM Revision 995bfad5 (lustrec): Add the script used to add k annotation to tests.
Guillaume Davy
02:40 PM Revision 2bdbbe54 (lustrec): Add tests from fmcad with k annotation to new_backend branch
Guillaume Davy

12/17/2014

09:11 PM Revision e8b5876f (lustrec): modified version with pure k induction
Pierre-Loïc Garoche

12/16/2014

08:10 AM Revision af0ff493 (lustrec): Removed unused predicate
Pierre-Loïc Garoche
12:23 AM Revision 5b12f571 (lustrec): Example on possible encoding using the 5-inductive two counter example.
Pierre-Loïc Garoche

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 Pierre-Loïc Garoche
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.
Pierre-Loïc Garoche
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 Pierre-Loïc Garoche
11:14 AM Revision 5d8ddbf7 (lustrec): Added an install target in the src folder
Pierre-Loïc Garoche

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 Xavier Thirioux
04:54 PM Revision 86b99b69 (lustrec): modified optimization info printout (option -print_reuse)
Xavier Thirioux
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 Xavier Thirioux
04:30 PM Revision fb8b1da7 (lustrec): supports again relative path for lustre source file (regression bug)
Xavier Thirioux
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...
Xavier Thirioux
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...
Xavier Thirioux
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 Pierre-Loïc Garoche
01:41 PM Revision bed8ea64 (lustrec): Moved Makefile into src folder
Pierre-Loïc Garoche
01:29 PM Revision f6ce2ae9 (lustrec): New branch ... again
Pierre-Loïc Garoche

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 Pierre-Loïc Garoche
09:09 PM Revision 830de634 (lustrec): Added a construct for Dependencies (was a tuple before) and a boolean attribute stateful
Pierre-Loïc Garoche
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 Pierre-Loïc Garoche
09:06 PM Revision a6208edd (lustrec): Almost nothing
Pierre-Loïc Garoche
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 Eric Noulard
02:36 PM Revision 76b2936d (lustrec): Properly handle generated files
Eric Noulard
 

Also available in: Atom