Commits · fc886259c38b160f6ac376c166d5c071fb7844c4 · LustreC / Lustrec

Apr 03, 2015

LOTS of bug correction wrt inlining, still a work in progress... · fc886259

THIRIOUX Xavier authored 10 years ago

 - global constants were not accounted for
 - no good avoidance of name capture when inlining
 - static parameters (array sizes and clocks) not handled
 - ill-typed generated expressions, when inlining array expressions



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

fc886259

Apr 01, 2015

added some test files · 77a61575

THIRIOUX Xavier authored 10 years ago

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

77a61575

correction of bugs: · 6efbcb73

THIRIOUX Xavier authored 10 years ago

 - a small problem in the parser
 - regarding the handling of destination directory, source directory, current directory, etc.
   It seems to be working now. A nice chasing after weird behaviors...



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

6efbcb73

Mar 24, 2015

synch with svn · c89faaa4

Temesghen Kahsai authored 10 years ago

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

c89faaa4

fixing double printing of horn rules · 3a87efb8

Temesghen Kahsai authored 10 years ago

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

3a87efb8

Fixed conflict with the svn trunk version · d41b874a

Temesghen Kahsai authored 10 years ago

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

d41b874a

Added local inlining using the keyword (*! /inlining/:true *) · 566dbf49
Pierre Loic Garoche authored 10 years ago
```
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@426 041b043f-8d7c-46b2-b46e-ef0dd855326e
```
566dbf49

Mar 17, 2015

Print the types · 228ebb2c

Pierre Loic Garoche authored 10 years ago

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

228ebb2c

revert back to previous expression for path · b9c40119

Pierre Loic Garoche authored 10 years ago

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

b9c40119

Mar 16, 2015

mapping horn values to lustre values in xml format · 922ed789

Temesghen Kahsai authored 10 years ago

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

922ed789

sync horn backend · b701409d

Temesghen Kahsai authored 10 years ago

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

b701409d

sync horn backend · 193a5ca6

Temesghen Kahsai authored 10 years ago

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

193a5ca6

modifed / to div in horn backend · e9b71779

Temesghen Kahsai authored 10 years ago

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

e9b71779

fixing double printing of horn rules · 99d9ac94

Temesghen Kahsai authored 10 years ago

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

99d9ac94

Changed configuration and update the horn_backend.ml · 53a9b564

Temesghen Kahsai authored 10 years ago

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

53a9b564

Fixed conflict with the svn trunk version · c7c6ef4c

Temesghen Kahsai authored 10 years ago

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

c7c6ef4c

Mar 12, 2015

Install FindLustre.cmake as well · 2e6dfb46

Eric Noulard authored 10 years ago

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

2e6dfb46

Mar 06, 2015

Changed the option horntraces to a general traces option · ea1c2906

Pierre Loic Garoche authored 10 years ago

This annotation phases would have to be moved in optimization of normalized code


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

ea1c2906

Mar 05, 2015

Reactivated the generation of traceability information · 3ca6d126

Pierre Loic Garoche authored 10 years ago

Changed the test-compile to use the horn-traces and the horn-queries option


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

3ca6d126

Mar 03, 2015

README.md edited online with Bitbucket · 8b34da11

Temesghen Kahsai authored 10 years ago

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

8b34da11

added invariants · 7d9df109

Temesghen Kahsai authored 10 years ago

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

7d9df109

including invariants · 8d4fddd8

Temesghen Kahsai authored 10 years ago

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

8d4fddd8

Fixed horn backend to make query for properties. More work needed for cex · 5cf953ec
Temesghen Kahsai authored 10 years ago
```
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@410 041b043f-8d7c-46b2-b46e-ef0dd855326e
```
5cf953ec

Feb 16, 2015

Solved bug found by Teme about asserts. · f2b1c245

Pierre Loic Garoche authored 10 years ago

Previously assert expression containing -> would lead to unnormalized ite. Now each expression within the assert is normalized and may bind new node equations.
This could be later optimized but is working now.

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

f2b1c245

Dec 10, 2014

Revert the commit 384 by Xavier: adding dirname to the source_name introduced... · e3373485

Pierre Loic Garoche authored 10 years ago

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

e3373485

Added an install target in the src folder · 40875a30

Pierre Loic Garoche authored 10 years ago

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

40875a30

Dec 09, 2014

modified optimization info printout (option -print_reuse) · 790765c0

THIRIOUX Xavier authored 10 years ago

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

790765c0

supports again relative path for lustre source file (regression bug) · 862ccfb1
THIRIOUX Xavier authored 10 years ago
```
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@384 041b043f-8d7c-46b2-b46e-ef0dd855326e
```
862ccfb1

added a new option -print_reuse that prints clock disjoint variables and reuse policy. · 89a70069

THIRIOUX Xavier authored 10 years ago

useful for debugging and carrying correctness proofs to the C code level.
non trivial result only when option -O 3 or above is activated.

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

89a70069

Moved Makefile into src folder · e8b6d5ca

Pierre Loic Garoche authored 10 years ago

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

e8b6d5ca

Dec 08, 2014

Added a construct for Dependencies (was a tuple before) and a boolean attribute stateful · 58a463e7
Pierre Loic Garoche authored 10 years ago
```
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@380 041b043f-8d7c-46b2-b46e-ef0dd855326e
```
58a463e7

Almost nothing · ff580eb7

Pierre Loic Garoche authored 10 years ago

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

ff580eb7

Properly handle generated files · 3fd9f1f2

Eric Noulard authored 10 years ago

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

3fd9f1f2

Dec 01, 2014

Doc file · 3d134f43

Pierre Loic Garoche authored 10 years ago

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

3d134f43

Removed oasis, now use the classical autoconf; ./configure; make · bd612a7b
Pierre Loic Garoche authored 10 years ago
```
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@376 041b043f-8d7c-46b2-b46e-ef0dd855326e
```
bd612a7b

- Dealt with compiling lusic from distant lusi files. · 1e48ef45

Pierre Loic Garoche authored 10 years ago

- Header now do not allow the generation of function previously declared as C prototype



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

1e48ef45

Small update · 17db36ed

Eric Noulard authored 10 years ago

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

17db36ed

Add first version of FindLustre.cmake · 615b63f1

Eric Noulard authored 10 years ago

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

615b63f1

Added compilation and install of include/*.lusi · 871b34d7

Pierre Loic Garoche authored 10 years ago

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

871b34d7

Add more functions in math.lusi · cb430a2b

Eric Noulard authored 10 years ago

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

cb430a2b