Project

General

Profile

Revision:

Revisions

# Date Author Comment
bd771bbe 03/24/2014 09:22 AM Xavier Thirioux

- some minor adjustments...

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

a1f57a52 03/24/2014 09:22 AM Xavier Thirioux

- some minor adjustments...

d4807c3d 03/24/2014 09:05 AM Xavier Thirioux

- corrected causality bug (cf. previous commit)

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

84d9893e 03/24/2014 09:05 AM Xavier Thirioux

- corrected causality bug (cf. previous commit)

f062bf3f 03/24/2014 07:19 AM Pierre-Loïc Garoche

Update scripts

50d06a28 03/23/2014 09:34 PM Pierre-Loïc Garoche

all benchs

7afcba5a 03/20/2014 03:41 PM Xavier Thirioux

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

e8c0f452 03/20/2014 03:41 PM Xavier Thirioux

liveness analysis improved. BUG found in causality wrt clocks...

b4694176 03/20/2014 06:08 AM Pierre-Loïc Garoche

Pushing last benchs in misc

53aa0cb0 03/20/2014 01:44 AM Pierre-Loïc Garoche

Pushing some benchs

f1f3758a 03/20/2014 01:35 AM Pierre-Loïc Garoche

Pushing some benchs

43a2cae9 03/20/2014 01:23 AM Pierre-Loïc Garoche

Pushing some benchs

6423979f 03/20/2014 12:53 AM Pierre-Loïc Garoche

update on script

b7c58c24 03/19/2014 11:46 PM Pierre-Loïc Garoche

iMinor modifs + improved script

a5784e75 03/19/2014 11:00 PM Xavier Thirioux

- modified example (arguments are now in the right order wrt clock declaration).
- debugged liveness analysis...

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

3c48346d 03/19/2014 11:00 PM Xavier Thirioux

- modified example (arguments are now in the right order wrt clock declaration).
- debugged liveness analysis...

695d6f2f 03/19/2014 06:08 PM Xavier Thirioux

- reimplemented computation of dead variables
- added computation of a reuse policy (depending on types)
- not yet used though, would have to change code generation
in order to be useful...

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

d4101ea0 03/19/2014 06:08 PM Xavier Thirioux

- reimplemented computation of dead variables
- added computation of a reuse policy (depending on types)
- not yet used though, would have to change code generation
in order to be useful...

8ea13d96 03/18/2014 06:05 PM Xavier Thirioux

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

6cf31814 03/18/2014 06:05 PM Xavier Thirioux

added liveness analysis for reusing dead variables. Not yet used.

d5a5678c 03/17/2014 11:42 PM Pierre-Loïc Garoche

Separated generation from compilation for mutants

5cab37f0 03/17/2014 11:03 PM Pierre-Loïc Garoche

New version of the script: gen new tests

d9970c39 03/17/2014 10:42 PM Pierre-Loïc Garoche

no rename

1e6a908f 03/17/2014 10:21 PM Pierre-Loïc Garoche

Missing file

78b04ee1 03/17/2014 10:04 PM Pierre-Loïc Garoche

Merged with trunk

04555efc 03/17/2014 08:52 PM Pierre-Loïc Garoche

Missing file Mmap

df924fb3 03/17/2014 08:50 PM Pierre-Loïc Garoche

Cleaning example files
Tiny optimization.

2e6f9ba8 03/17/2014 01:01 PM Xavier Thirioux

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

14ebde97 03/17/2014 01:01 PM Xavier Thirioux

improved code generation by factorizing out arrows

6955f956 03/17/2014 12:46 PM Pierre-Loïc Garoche

Version compatible avec le francais

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

8a5f633d 03/17/2014 12:46 PM Pierre-Loïc Garoche

Version compatible avec le francais

1692756a 03/17/2014 09:06 AM Pierre-Loïc Garoche

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

1699b8ff 03/17/2014 09:06 AM Pierre-Loïc Garoche

Updated test script: changed path and verbose mode

3f9600bb 03/17/2014 07:44 AM Pierre-Loïc Garoche

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

701b0c0a 03/17/2014 07:44 AM Pierre-Loïc Garoche

Moved tests outside of source code to avoid useless duplication.

67ba882b 03/17/2014 07:44 AM Pierre-Loïc Garoche

Moved tests outside of source code to avoid useless duplication.

443f0686 03/17/2014 07:40 AM Pierre-Loïc Garoche

Added Alice Tailliar example

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

cbe93c65 03/17/2014 07:40 AM Pierre-Loïc Garoche

Added Alice Tailliar example

e135421f 03/17/2014 12:17 AM Xavier Thirioux

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 and paves the way for more optimizations.

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

5538b7ac 03/17/2014 12:17 AM Xavier Thirioux

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 and paves the way for more optimizations.

224d9d76 03/15/2014 02:01 PM Pierre-Loïc Garoche

Hack to avoid empty struct. This is mandatory for frama-c (for the moment)

57ec37a1 03/15/2014 01:56 PM Pierre-Loïc Garoche

New functions to identify stateless machines

07f1f2e1 03/15/2014 12:16 AM Pierre-Loïc Garoche

Modified the makefile to fit eacsl issues

52cfee34 03/14/2014 05:45 PM Xavier Thirioux

- 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/lustrec/lustre_compiler/trunk@198 041b043f-8d7c-46b2-b46e-ef0dd855326e

d3e4c22f 03/14/2014 05:45 PM Xavier Thirioux

- work in progress for stateless/stateful status computation
(to turn conditionals into merges, which yield more efficient C code)

1d3e339d 03/14/2014 03:28 PM Pierre-Loïc Garoche

Bug solved: comma in function calls

f2a319ff 03/14/2014 02:49 PM Pierre-Loïc Garoche

ACSL spec: produce memory related properties: valid pointers, speration, assigns

302670bb 03/14/2014 01:56 AM Pierre-Loïc Garoche

Bug solved when using arrows in annotations.
- arrows are inlined
- specification memories are initialized in the reset function.

89b9e25c 03/13/2014 05:30 PM Xavier Thirioux

corrected bugs in clock generalization that produced pessimistic C code (not wrong though); corrected bug with node importation policy wrt (re)declaration, (re)definition...

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

2ea1e4a6 03/13/2014 05:30 PM Xavier Thirioux

corrected bugs in clock generalization that produced pessimistic C code (not wrong though); corrected bug with node importation policy wrt (re)declaration, (re)definition...

a64d9fe9 03/12/2014 07:12 PM Pierre-Loïc Garoche

Bug solved on complex ACSL predicates

df52f39b 03/12/2014 06:10 PM Pierre-Loïc Garoche

Default is "no ghost mode"

2196a0a6 03/12/2014 06:08 PM Pierre-Loïc Garoche

Cleaned tons of useless debugging prints

96fecb0f 03/12/2014 05:59 PM Pierre-Loïc Garoche

Lots of changes: mainly solved bugs
- specification is now stored as a set of equations
- the tuple splitting is performed during normalization and not anymore in machine code
- solved bug with tuple equalities, ie. x = (a,b,c) = (c,d,e)
- better handling of acsl generation including quantifiers...

cfff99fd 03/12/2014 05:55 PM Pierre-Loïc Garoche

Solved bug when loading preexisting lusi files

26031546 03/11/2014 11:41 PM Pierre-Loïc Garoche

Merged trunk modifs up to r186.

0b0a959a 03/11/2014 11:21 PM Pierre-Loïc Garoche

First working version of the ACSL generation.

21485807 03/11/2014 03:41 PM Xavier Thirioux

- added struct types declaration
- added constant definition with a struct type
- added checking for multiple definitions of nodes (behavior was buggy)
- better and more uniform error messages
for undefined/already defined symbols

We still need struct expressions......
6affc9f5 03/11/2014 03:41 PM Xavier Thirioux

- added struct types declaration
- added constant definition with a struct type
- added checking for multiple definitions of nodes (behavior was buggy)
- better and more uniform error messages
for undefined/already defined symbols

We still need struct expressions...
5eded996 03/11/2014 01:42 AM Pierre-Loïc Garoche

Ongoing work on specification compilation

- Integrated changes of trunk
- changed the types of extended expressions: only allow prenex forms
- normalization and machine code extended to deal with compilation of spec
- other annotations are almost not considered yet....

b174e673 03/10/2014 05:56 PM Xavier Thirioux

work in progress for struct types...

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

51768260 03/10/2014 05:56 PM Xavier Thirioux

work in progress for struct types...

12af4908 03/10/2014 09:55 AM Xavier Thirioux

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.ml
M trunk/src/main_lustre_compiler.ml
M trunk/src/types.ml
M trunk/src/printers.ml
M trunk/src/typing.ml...

aa223e69 03/10/2014 09:55 AM Xavier Thirioux

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.ml
M trunk/src/main_lustre_compiler.ml
M trunk/src/types.ml
M trunk/src/printers.ml
M trunk/src/typing.ml...

6a6abd76 03/06/2014 04:33 PM Xavier Thirioux

first steps towards struct types...

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

6560bb94 03/06/2014 04:33 PM Xavier Thirioux

first steps towards struct types...

fa090c4e 03/06/2014 03:39 PM Xavier Thirioux

corrected bug in arrow macros names, added storage attribute for static alloc macros, option -d now creates the destination directory if needed, with current dir as file permissions

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

9bdfc99f 03/06/2014 03:39 PM Xavier Thirioux

corrected bug in arrow macros names, added storage attribute for static alloc macros, option -d now creates the destination directory if needed, with current dir as file permissions

04e26a3f 03/05/2014 04:32 PM Xavier Thirioux

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 generated code
- compiling and linking arrow.c is only necessary
in case of dynamic allocation
- version now includes installation prefix (for the standard lib)...

c6acbdaa 03/05/2014 04:32 PM Xavier Thirioux

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 generated code
- compiling and linking arrow.c is only necessary
in case of dynamic allocation
- version now includes installation prefix (for the standard lib)...

2fa10a44 03/05/2014 02:35 PM Xavier Thirioux

In order to export any type of constants, moved type definitions from .c to .h

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

6bab3787 03/05/2014 02:35 PM Xavier Thirioux

In order to export any type of constants, moved type definitions from .c to .h

e772c6ef 03/04/2014 02:41 PM Eric Noulard

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

b3202935 03/04/2014 02:41 PM Eric Noulard

Generate extern declarations for constant as well.

5e925ce8 03/01/2014 03:38 PM Xavier Thirioux

- 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

3e79b3a5 03/01/2014 03:38 PM Xavier Thirioux

- stupid svn had removed a file, again

8f1c7e91 03/01/2014 03:37 PM Xavier Thirioux

- 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/lustrec/lustre_compiler/trunk@176 041b043f-8d7c-46b2-b46e-ef0dd855326e

c518d082 03/01/2014 03:37 PM Xavier Thirioux

- added generation of clock information in interface (.lusi) files
- added clock checking between interface and implementation files

592f508c 03/01/2014 12:01 AM Pierre-Loïc Garoche

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 041b043f-8d7c-46b2-b46e-ef0dd855326e

2842f7ca 03/01/2014 12:01 AM Pierre-Loïc Garoche

Reenabled the generation of witnesses for inline process.
Systematic use of the build path

c3bbc76e 02/28/2014 11:59 PM Pierre-Loïc Garoche

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

626e6f03 02/28/2014 11:59 PM Pierre-Loïc Garoche

Updated script. Does not seem to be fully functional yet.

65f71d05 02/28/2014 11:59 PM Pierre-Loïc Garoche

Added default ensures statements

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

3e36d4e0 02/28/2014 11:59 PM Pierre-Loïc Garoche

Added default ensures statements

a6c265f5 02/28/2014 05:09 PM Xavier Thirioux

- added dummy_lib.lusi (accidentally removed !?)

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

7f611a35 02/28/2014 05:09 PM Xavier Thirioux

- added dummy_lib.lusi (accidentally removed !?)

7291cb80 02/28/2014 04:56 PM Xavier Thirioux

- merged test script
- added -d support
- corrected #open parser problem
- corrected interface/implementation (.lusi/.lus) checking
for types (not yet for clocks)

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

8b3afe43 02/28/2014 04:56 PM Xavier Thirioux

- merged test script
- added -d support
- corrected #open parser problem
- corrected interface/implementation (.lusi/.lus) checking
for types (not yet for clocks)

483bbbe9 02/28/2014 03:50 PM Pierre-Loïc Garoche

New branch to work on generation of ACSL

0777a7be 02/28/2014 03:28 PM Pierre-Loïc Garoche

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

29ad4531 02/28/2014 03:28 PM Pierre-Loïc Garoche

Merge back horn backend branch in trunk

c6f61bd7 02/28/2014 02:05 PM Pierre-Loïc Garoche

Merge trunk modif in branch

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@168 041b043f-8d7c-46b2-b46e-ef0dd855326e

64aa99c4 02/28/2014 02:05 PM Pierre-Loïc Garoche

Merge trunk modif in branch

c11dbf10 02/28/2014 02:04 PM Pierre-Loïc Garoche

desome

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@167 041b043f-8d7c-46b2-b46e-ef0dd855326e

addb1a3a 02/28/2014 02:04 PM Pierre-Loïc Garoche

desome

867595f2 02/28/2014 01:52 PM Pierre-Loïc Garoche

Merge inlining branch within trunk.
The test target requires branch lustrec/horn as binary lustreh.

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

49b32cb6 02/28/2014 01:52 PM Pierre-Loïc Garoche

Merge inlining branch within trunk.
The test target requires branch lustrec/horn as binary lustreh.

b09a175c 02/28/2014 01:43 PM Pierre-Loïc Garoche

inliner function

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/inlining@165 041b043f-8d7c-46b2-b46e-ef0dd855326e

274c72ec 02/28/2014 01:43 PM Pierre-Loïc Garoche

inliner function

c653e640 02/28/2014 10:39 AM Pierre-Loïc Garoche

Minor bugs

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@164 041b043f-8d7c-46b2-b46e-ef0dd855326e

(1301-1400/1482) Per page: 25, 50, 100

Also available in: Atom