Activity
From 02/27/2014 to 03/28/2014
03/27/2014
- 09:26 PM Revision 8e5fd1d1 (lustrec): Some updates on scripts
- 09:45 AM Revision 78a35eae (lustrec): Creating a new branch for proof in ACSL
03/24/2014
- 09:05 PM Revision 8fdeb449 (lustrec): Updated scripts
- 08:49 PM Revision 6f765157 (lustrec): Moving files around
- 02:37 PM Revision 66e38617 (lustrec): removed debug message
- 02:37 PM Revision b35da910 (lustrec): removed debug message
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@230 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 02:36 PM Revision 0b78e972 (lustrec): changed name generation to avoid conflict with C predefined symbols;...
- 02:36 PM Revision 96f5fe18 (lustrec): changed name generation to avoid conflict with C predefined symbols;...
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@229 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 09:22 AM Revision a1f57a52 (lustrec): - some minor adjustments...
- 09:22 AM Revision bd771bbe (lustrec): - some minor adjustments...
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@228 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 09:05 AM Revision 84d9893e (lustrec): - corrected causality bug (cf. previous commit)
- 09:05 AM Revision d4807c3d (lustrec): - corrected causality bug (cf. previous commit)
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@227 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 07:19 AM Revision f062bf3f (lustrec): Update scripts
03/23/2014
03/20/2014
- 03:41 PM Revision e8c0f452 (lustrec): liveness analysis improved. BUG found in causality wrt clocks...
- 03:41 PM Revision 7afcba5a (lustrec): liveness analysis improved. BUG found in causality wrt clocks...
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@224 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 06:08 AM Revision b4694176 (lustrec): Pushing last benchs in misc
- 01:44 AM Revision 53aa0cb0 (lustrec): Pushing some benchs
- 01:35 AM Revision f1f3758a (lustrec): Pushing some benchs
- 01:23 AM Revision 43a2cae9 (lustrec): Pushing some benchs
03/19/2014
- 12:53 AM Revision 6423979f (lustrec): update on script
- 11:46 PM Revision b7c58c24 (lustrec): iMinor modifs + improved script
- 11:00 PM Revision 3c48346d (lustrec): - modified example (arguments are now in the right order wrt clock d...
- - debugged liveness analysis...
- 11:00 PM Revision a5784e75 (lustrec): - modified example (arguments are now in the right order wrt clock d...
- - debugged liveness analysis...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@217 041b04... - 06:08 PM Revision d4101ea0 (lustrec): - reimplemented computation of dead variables
- - added computation of a reuse policy (depending on types)
- not yet used though, would have to change code generati... - 06:08 PM Revision 695d6f2f (lustrec): - reimplemented computation of dead variables
- - added computation of a reuse policy (depending on types)
- not yet used though, would have to change code generati...
03/18/2014
- 06:05 PM Revision 6cf31814 (lustrec): added liveness analysis for reusing dead variables. Not yet used.
- 06:05 PM Revision 8ea13d96 (lustrec): added liveness analysis for reusing dead variables. Not yet used.
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@215 041b043f-8d7c-46b2-b46e-ef0dd855326e
03/17/2014
- 11:42 PM Revision d5a5678c (lustrec): Separated generation from compilation for mutants
- 11:03 PM Revision 5cab37f0 (lustrec): New version of the script: gen new tests
- 10:42 PM Revision d9970c39 (lustrec): no rename
- 10:21 PM Revision 1e6a908f (lustrec): Missing file
- 10:04 PM Revision 78b04ee1 (lustrec): Merged with trunk
- 08:52 PM Revision 04555efc (lustrec): Missing file Mmap
- 08:50 PM Revision df924fb3 (lustrec): Cleaning example files
- Tiny optimization.
- 01:01 PM Revision 14ebde97 (lustrec): improved code generation by factorizing out arrows
- 01:01 PM Revision 2e6f9ba8 (lustrec): improved code generation by factorizing out arrows
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@207 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 12:46 PM Revision 8a5f633d (lustrec): Version compatible avec le francais
- 12:46 PM Revision 6955f956 (lustrec): Version compatible avec le francais
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@206 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 09:06 AM Revision 1699b8ff (lustrec): Updated test script: changed path and verbose mode
- 09:06 AM Revision 1692756a (lustrec): Updated test script: changed path and verbose mode
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@205 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 07:44 AM Revision 67ba882b (lustrec): Moved tests outside of source code to avoid useless duplication.
- 07:44 AM Revision 701b0c0a (lustrec): Moved tests outside of source code to avoid useless duplication.
- 07:44 AM Revision 3f9600bb (lustrec): Moved tests outside of source code to avoid useless duplication.
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@204 041b043f-8d7c-46b2-b46e-ef0dd855326e
- 07:40 AM Revision cbe93c65 (lustrec): Added Alice Tailliar example
- 07:40 AM Revision 443f0686 (lustrec): Added Alice Tailliar example
- git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@203 041b043f-8d7c-46b2-b46e-ef0dd855326e
03/16/2014
- 12:17 AM Revision 5538b7ac (lustrec): Added declaration/definition of stateless/stateful nodes.
- The 'function' keyword is for stateless nodes only,
the 'node' keyword is any kind of node.
Improves compilation an... - 12:17 AM Revision e135421f (lustrec): Added declaration/definition of stateless/stateful nodes.
- The 'function' keyword is for stateless nodes only,
the 'node' keyword is any kind of node.
Improves compilation an...
03/15/2014
- 02:01 PM Revision 224d9d76 (lustrec): Hack to avoid empty struct. This is mandatory for frama-c (for the m...
- 01:56 PM Revision 57ec37a1 (lustrec): New functions to identify stateless machines
03/14/2014
- 12:16 AM Revision 07f1f2e1 (lustrec): Modified the makefile to fit eacsl issues
- 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)
- 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... - 03:28 PM Revision 1d3e339d (lustrec): Bug solved: comma in function calls
- 02:49 PM Revision f2a319ff (lustrec): ACSL spec: produce memory related properties: valid pointers, sperat...
- 01:56 AM Revision 302670bb (lustrec): Bug solved when using arrows in annotations.
- - arrows are inlined
- specification memories are initialized in the reset function.
03/13/2014
- 05:30 PM Revision 2ea1e4a6 (lustrec): corrected bugs in clock generalization that produced pessimistic C c...
- 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
03/12/2014
- 07:12 PM Revision a64d9fe9 (lustrec): Bug solved on complex ACSL predicates
- 06:10 PM Revision df52f39b (lustrec): Default is "no ghost mode"
- 06:08 PM Revision 2196a0a6 (lustrec): Cleaned tons of useless debugging prints
- 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... - 05:55 PM Revision cfff99fd (lustrec): Solved bug when loading preexisting lusi files
03/11/2014
- 11:41 PM Revision 26031546 (lustrec): Merged trunk modifs up to r186.
- 11:21 PM Revision 0b0a959a (lustrec): First working version of the ACSL generation.
- 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... - 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... - 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...
03/10/2014
- 05:56 PM Revision 51768260 (lustrec): work in progress for struct types...
- 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
- 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... - 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...
03/06/2014
- 04:33 PM Revision 6560bb94 (lustrec): first steps towards struct types...
- 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
- 03:39 PM Revision 9bdfc99f (lustrec): corrected bug in arrow macros names, added storage attribute for sta...
- 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
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... - 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... - 02:35 PM Revision 6bab3787 (lustrec): In order to export any type of constants, moved type definitions fro...
- 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
03/04/2014
- 02:41 PM Revision b3202935 (lustrec): Generate extern declarations for constant as well.
- 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
03/01/2014
- 03:38 PM Revision 3e79b3a5 (lustrec): - stupid svn had removed a file, again
- 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
- 03:37 PM Revision c518d082 (lustrec): - added generation of clock information in interface (.lusi) files
- - added clock checking between interface and implementation files
- 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...
02/28/2014
- 12:01 AM Revision 2842f7ca (lustrec): Reenabled the generation of witnesses for inline process.
- Systematic use of the build path
- 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... - 11:59 PM Revision 626e6f03 (lustrec): Updated script. Does not seem to be fully functional yet.
- 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
- 11:59 PM Revision 3e36d4e0 (lustrec): Added default ensures statements
- 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
- 05:09 PM Revision 7f611a35 (lustrec): - added dummy_lib.lusi (accidentally removed !?)
- 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
- 04:56 PM Revision 8b3afe43 (lustrec): - merged test script
- - added -d support
- corrected #open parser problem
- corrected interface/implementation (.lusi/.lus) checking
f... - 04:56 PM Revision 7291cb80 (lustrec): - merged test script
- - added -d support
- corrected #open parser problem
- corrected interface/implementation (.lusi/.lus) checking
f... - 03:50 PM Revision 483bbbe9 (lustrec): New branch to work on generation of ACSL
- 03:28 PM Revision 29ad4531 (lustrec): Merge back horn backend branch in trunk
- 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
- 02:05 PM Revision 64aa99c4 (lustrec): Merge trunk modif in branch
- 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...
- 02:04 PM Revision addb1a3a (lustrec): desome
- 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...
- 01:52 PM Revision 49b32cb6 (lustrec): Merge inlining branch within trunk.
- The test target requires branch lustrec/horn as binary lustreh.
- 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... - 01:43 PM Revision 274c72ec (lustrec): inliner function
- 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...
- 10:39 AM Revision b63536a0 (lustrec): Minor bugs
- 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...
- 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... - 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... - 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 ... - 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 ...
Also available in: Atom