Project

General

Profile

Activity

From 02/13/2014 to 03/14/2014

03/14/2014

05:45 PM Revision d3e4c22f (lustrec): - work in progress for stateless/stateful status computation
(to turn conditionals into merges, which yield more efficient C code) Xavier Thirioux
05:45 PM Revision 52cfee34 (lustrec): - work in progress for stateless/stateful status computation
(to turn conditionals into merges, which yield more efficient C code)
git-svn-id: https://cavale.enseeiht.fr/svn/lu...
Xavier Thirioux
03:28 PM Revision 1d3e339d (lustrec): Bug solved: comma in function calls
Pierre-Loïc Garoche
02:49 PM Revision f2a319ff (lustrec): ACSL spec: produce memory related properties: valid pointers, sperat...
Pierre-Loïc Garoche
01:56 AM Revision 302670bb (lustrec): Bug solved when using arrows in annotations.
- arrows are inlined
- specification memories are initialized in the reset function.
Pierre-Loïc Garoche

03/13/2014

05:30 PM Revision 2ea1e4a6 (lustrec): corrected bugs in clock generalization that produced pessimistic C c...
Xavier Thirioux
05:30 PM Revision 89b9e25c (lustrec): corrected bugs in clock generalization that produced pessimistic C c...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@194 041b043f-8d7c-46b2-b46e-ef0dd855326e Xavier Thirioux

03/12/2014

07:12 PM Revision a64d9fe9 (lustrec): Bug solved on complex ACSL predicates
Pierre-Loïc Garoche
06:10 PM Revision df52f39b (lustrec): Default is "no ghost mode"
Pierre-Loïc Garoche
06:08 PM Revision 2196a0a6 (lustrec): Cleaned tons of useless debugging prints
Pierre-Loïc Garoche
05:59 PM Revision 96fecb0f (lustrec): Lots of changes: mainly solved bugs
- specification is now stored as a set of equations
- the tuple splitting is performed during normalization and not a...
Pierre-Loïc Garoche
05:55 PM Revision cfff99fd (lustrec): Solved bug when loading preexisting lusi files
Pierre-Loïc Garoche

03/11/2014

11:41 PM Revision 26031546 (lustrec): Merged trunk modifs up to r186.
Pierre-Loïc Garoche
11:21 PM Revision 0b0a959a (lustrec): First working version of the ACSL generation.
Pierre-Loïc Garoche
03:41 PM Revision 6affc9f5 (lustrec): - added struct types declaration
- added constant definition with a struct type
- added checking for multiple definitions of nodes (behavior was bugg...
Xavier Thirioux
03:41 PM Revision 21485807 (lustrec): - added struct types declaration
- added constant definition with a struct type
- added checking for multiple definitions of nodes (behavior was bugg...
Xavier Thirioux
01:42 AM Revision 5eded996 (lustrec): Ongoing work on specification compilation
- Integrated changes of trunk
- changed the types of extended expressions: only allow prenex forms
- normalization an...
Pierre-Loïc Garoche

03/10/2014

05:56 PM Revision 51768260 (lustrec): work in progress for struct types...
Xavier Thirioux
05:56 PM Revision b174e673 (lustrec): work in progress for struct types...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@184 041b043f-8d7c-46b2-b46e-ef0dd855326e Xavier Thirioux
09:55 AM Revision aa223e69 (lustrec): more steps towards struct types...
Cette ligne, et les suivantes ci-dessous, seront ignorées--
M trunk/src/corelang.mli
M trunk/src/type_predef.m...
Xavier Thirioux
09:55 AM Revision 12af4908 (lustrec): more steps towards struct types...
Cette ligne, et les suivantes ci-dessous, seront ignorées--
M trunk/src/corelang.mli
M trunk/src/type_predef.m...
Xavier Thirioux

03/06/2014

04:33 PM Revision 6560bb94 (lustrec): first steps towards struct types...
Xavier Thirioux
04:33 PM Revision 6a6abd76 (lustrec): first steps towards struct types...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@182 041b043f-8d7c-46b2-b46e-ef0dd855326e Xavier Thirioux
03:39 PM Revision 9bdfc99f (lustrec): corrected bug in arrow macros names, added storage attribute for sta...
Xavier Thirioux
03:39 PM Revision fa090c4e (lustrec): corrected bug in arrow macros names, added storage attribute for sta...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@181 041b043f-8d7c-46b2-b46e-ef0dd855326e Xavier Thirioux

03/05/2014

04:32 PM Revision c6acbdaa (lustrec): answer to #feature 50:
- arrows are now factorized out and become part of include
as files arrow.h and arrow.c
- no more arrows in gener...
Xavier Thirioux
04:32 PM Revision 04e26a3f (lustrec): answer to #feature 50:
- arrows are now factorized out and become part of include
as files arrow.h and arrow.c
- no more arrows in gener...
Xavier Thirioux
02:35 PM Revision 6bab3787 (lustrec): In order to export any type of constants, moved type definitions fro...
Xavier Thirioux
02:35 PM Revision 2fa10a44 (lustrec): In order to export any type of constants, moved type definitions fro...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@179 041b043f-8d7c-46b2-b46e-ef0dd855326e Xavier Thirioux

03/04/2014

02:41 PM Revision b3202935 (lustrec): Generate extern declarations for constant as well.
Eric Noulard
02:41 PM Revision e772c6ef (lustrec): Generate extern declarations for constant as well.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@178 041b043f-8d7c-46b2-b46e-ef0dd855326e Eric Noulard

03/01/2014

03:38 PM Revision 3e79b3a5 (lustrec): - stupid svn had removed a file, again
Xavier Thirioux
03:38 PM Revision 5e925ce8 (lustrec): - stupid svn had removed a file, again
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@177 041b043f-8d7c-46b2-b46e-ef0dd855326e Xavier Thirioux
03:37 PM Revision c518d082 (lustrec): - added generation of clock information in interface (.lusi) files
- added clock checking between interface and implementation files Xavier Thirioux
03:37 PM Revision 8f1c7e91 (lustrec): - added generation of clock information in interface (.lusi) files
- added clock checking between interface and implementation files
git-svn-id: https://cavale.enseeiht.fr/svn/lustre...
Xavier Thirioux

02/28/2014

12:01 AM Revision 2842f7ca (lustrec): Reenabled the generation of witnesses for inline process.
Systematic use of the build path Pierre-Loïc Garoche
12:01 AM Revision 592f508c (lustrec): Reenabled the generation of witnesses for inline process.
Systematic use of the build path
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@175 041b...
Pierre-Loïc Garoche
11:59 PM Revision 626e6f03 (lustrec): Updated script. Does not seem to be fully functional yet.
Pierre-Loïc Garoche
11:59 PM Revision c3bbc76e (lustrec): Updated script. Does not seem to be fully functional yet.
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@174 041b043f-8d7c-46b2-b46e-ef0dd855326e Pierre-Loïc Garoche
11:59 PM Revision 3e36d4e0 (lustrec): Added default ensures statements
Pierre-Loïc Garoche
11:59 PM Revision 65f71d05 (lustrec): Added default ensures statements
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@173 041b043f-8d7c-46b2-b46e-ef0dd855326e Pierre-Loïc Garoche
05:09 PM Revision 7f611a35 (lustrec): - added dummy_lib.lusi (accidentally removed !?)
Xavier Thirioux
05:09 PM Revision a6c265f5 (lustrec): - added dummy_lib.lusi (accidentally removed !?)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@172 041b043f-8d7c-46b2-b46e-ef0dd855326e Xavier Thirioux
04:56 PM Revision 8b3afe43 (lustrec): - merged test script
- added -d support
- corrected #open parser problem
- corrected interface/implementation (.lusi/.lus) checking
f...
Xavier Thirioux
04:56 PM Revision 7291cb80 (lustrec): - merged test script
- added -d support
- corrected #open parser problem
- corrected interface/implementation (.lusi/.lus) checking
f...
Xavier Thirioux
03:50 PM Revision 483bbbe9 (lustrec): New branch to work on generation of ACSL
Pierre-Loïc Garoche
03:28 PM Revision 29ad4531 (lustrec): Merge back horn backend branch in trunk
Pierre-Loïc Garoche
03:28 PM Revision 0777a7be (lustrec): Merge back horn backend branch in trunk
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@169 041b043f-8d7c-46b2-b46e-ef0dd855326e Pierre-Loïc Garoche
02:05 PM Revision 64aa99c4 (lustrec): Merge trunk modif in branch
Pierre-Loïc Garoche
02:05 PM Revision c6f61bd7 (lustrec): Merge trunk modif in branch
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@168 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche
02:04 PM Revision addb1a3a (lustrec): desome
Pierre-Loïc Garoche
02:04 PM Revision c11dbf10 (lustrec): desome
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@167 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche
01:52 PM Revision 49b32cb6 (lustrec): Merge inlining branch within trunk.
The test target requires branch lustrec/horn as binary lustreh. Pierre-Loïc Garoche
01:52 PM Revision 867595f2 (lustrec): Merge inlining branch within trunk.
The test target requires branch lustrec/horn as binary lustreh.
git-svn-id: https://cavale.enseeiht.fr/svn/lustre...
Pierre-Loïc Garoche
01:43 PM Revision 274c72ec (lustrec): inliner function
Pierre-Loïc Garoche
01:43 PM Revision b09a175c (lustrec): inliner function
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/inlining@165 041b043f-8d7c-46b2-b46e-ef0d... Pierre-Loïc Garoche
10:39 AM Revision b63536a0 (lustrec): Minor bugs
Pierre-Loïc Garoche
10:39 AM Revision c653e640 (lustrec): Minor bugs
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@164 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche
10:35 AM Revision ae78dfee (lustrec): Do not use stable sort because it requires recent ocamlgraph
library (1.8.3) which is not widely available in distro repository.
Moreover "stable" sort is not necessary, sort wil...
Eric Noulard
10:35 AM Revision 64dfa450 (lustrec): Do not use stable sort because it requires recent ocamlgraph
library (1.8.3) which is not widely available in distro repository.
Moreover "stable" sort is not necessary, sort wil...
Eric Noulard
10:33 AM Revision c02d255e (lustrec): Solved some bugs in the lustre printer
Generation of a witness with both the main node and hte inlined main node
Test script modified to check consistency ...
Pierre-Loïc Garoche
10:33 AM Revision e2380d4d (lustrec): Solved some bugs in the lustre printer
Generation of a witness with both the main node and hte inlined main node
Test script modified to check consistency ...
Pierre-Loïc Garoche

02/26/2014

03:37 PM Revision 06fa8b5e (lustrec): better error message for tuple type mismatch
Xavier Thirioux
03:37 PM Revision 1577dc7e (lustrec): better error message for tuple type mismatch
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@161 041b043f-8d7c-46b2-b46e-ef0dd855326e Xavier Thirioux
02:37 PM Revision fbda2f96 (lustrec): again, debugged tuple subtyping
Xavier Thirioux
02:37 PM Revision 11242500 (lustrec): again, debugged tuple subtyping
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@160 041b043f-8d7c-46b2-b46e-ef0dd855326e Xavier Thirioux
02:04 PM Revision 45ca90f5 (lustrec): removed debug printing
Xavier Thirioux
02:04 PM Revision 17249d2e (lustrec): removed debug printing
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@159 041b043f-8d7c-46b2-b46e-ef0dd855326e Xavier Thirioux
02:02 PM Revision 1cb216b4 (lustrec): corrected wrong subtyping rule for tuple assignment
Xavier Thirioux
02:02 PM Revision 9b5969d4 (lustrec): corrected wrong subtyping rule for tuple assignment
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@158 041b043f-8d7c-46b2-b46e-ef0dd855326e Xavier Thirioux
01:42 PM Revision b580c8f8 (lustrec): added subtyping in equations (rhs may be a subtype of lhs)
Xavier Thirioux
01:42 PM Revision 4a840259 (lustrec): added subtyping in equations (rhs may be a subtype of lhs)
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@157 041b043f-8d7c-46b2-b46e-ef0dd855326e Xavier Thirioux
07:48 AM Revision b8ae1bbc (lustrec): Improvements as suggested by e. Noulard: better install of include; ...
Pierre-Loïc Garoche
07:48 AM Revision 71513f0e (lustrec): Improvements as suggested by e. Noulard: better install of include; ...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@156 041b043f-8d7c-46b2-b46e-ef0dd855326e Pierre-Loïc Garoche

02/24/2014

04:47 PM Revision f1da5111 (lustrec): Updated version of test script: timeout for z3
Pierre-Loïc Garoche
04:47 PM Revision aea225b9 (lustrec): Updated version of test script: timeout for z3
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@155 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche
04:26 PM Revision 9334747d (lustrec): Fixed bug on the main part
Pierre-Loïc Garoche
04:26 PM Revision 4be0d54a (lustrec): Fixed bug on the main part
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@154 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche
11:48 AM Revision 433b1e6b (lustrec): Cleaning useless files
Pierre-Loïc Garoche
11:48 AM Revision 1f674c15 (lustrec): Cleaning useless files
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@153 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche
11:47 AM Revision 3e209698 (lustrec): First fully working version of horn backend.
Has to be called with "-horn -node main_node"
The test script compute the smt2 file and calls z3 on them.
Pierre-Loïc Garoche
11:47 AM Revision cd6efd9b (lustrec): First fully working version of horn backend.
Has to be called with "-horn -node main_node"
The test script compute the smt2 file and calls z3 on them.
git-svn-...
Pierre-Loïc Garoche
11:25 AM Revision 3a60ec17 (lustrec): ...
Pierre-Loïc Garoche
11:25 AM Revision 9cab57c9 (lustrec): ...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@151 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche
10:50 AM Revision 4f3cc9f3 (lustrec): Is it working?
Pierre-Loïc Garoche
10:50 AM Revision 2f44a4cc (lustrec): Is it working?
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@150 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche
09:46 AM Revision c0003810 (lustrec): Working on bugs
Pierre-Loïc Garoche
09:46 AM Revision c76f1d66 (lustrec): Working on bugs
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@149 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche

02/21/2014

05:34 PM Revision 3a9e1fe8 (lustrec): Manually corrected version of ex3. Should integrate the modifications
Pierre-Loïc Garoche
05:34 PM Revision 2b8eca7f (lustrec): Manually corrected version of ex3. Should integrate the modifications
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@148 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche
05:11 PM Revision 40f8d0f9 (lustrec): Second (almost) working version
Pierre-Loïc Garoche
05:11 PM Revision f19eb2fd (lustrec): Second (almost) working version
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@147 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche
04:39 PM Revision faa5e5c5 (lustrec): First (almost) working version
Pierre-Loïc Garoche
04:39 PM Revision 20e9de2d (lustrec): First (almost) working version
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@146 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche
12:42 PM Revision fc7a01ce (lustrec): Ongoing ...
Pierre-Loïc Garoche
12:42 PM Revision 96babff4 (lustrec): Ongoing ...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@145 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche
12:38 PM Revision 23bdf881 (lustrec): Ongoing ...
Pierre-Loïc Garoche
12:38 PM Revision 8605c4a4 (lustrec): Ongoing ...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@144 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche
08:37 AM Revision 04a7df69 (lustrec): In the middle of the coding process. Just pushing thinks
Pierre-Loïc Garoche
08:37 AM Revision 7a19992d (lustrec): In the middle of the coding process. Just pushing thinks
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@143 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche

02/20/2014

06:45 AM Revision aa6b7d46 (lustrec): The missing file
Pierre-Loïc Garoche
06:45 AM Revision dcbf9d3a (lustrec): The missing file
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@142 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche

02/19/2014

05:02 PM Revision f6923c9e (lustrec): Initial copy of the horn output version. Not really working yet
Pierre-Loïc Garoche
05:02 PM Revision 3ee1012f (lustrec): Initial copy of the horn output version. Not really working yet
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@141 041b043f-8d7c-46b2-b46e... Pierre-Loïc Garoche
 

Also available in: Atom