Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec @ ea1c2906

Name Size Revision Age Author Comment
  doc a2d97a3e over 6 years Pierre-Loïc Garoche Updated the licence info and header for each fi...
  include 1e48ef45 almost 6 years Pierre-Loïc Garoche - Dealt with compiling lusic from distant lusi ...
  share 3fd9f1f2 almost 6 years Eric Noulard Properly handle generated files git-svn-id: h...
  src ea1c2906 over 5 years Pierre-Loïc Garoche Changed the option horntraces to a general trac...
  test 3ca6d126 over 5 years Pierre-Loïc Garoche Reactivated the generation of traceability info...
.gitignore 77 Bytes be3dd43f over 6 years Teme Kahsai Fixed horn backend to make query for properties...
AUTHORS 133 Bytes a2d97a3e over 6 years Pierre-Loïc Garoche Updated the licence info and header for each fi...
LICENSE-LGPL.txt 25.8 KB 22fe1c93 about 7 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler git-sv...
Makefile.in 820 Bytes e8b6d5ca almost 6 years Pierre-Loïc Garoche Moved Makefile into src folder git-svn-id: ht...
README.lustrec 802 Bytes 22fe1c93 about 7 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler git-sv...
README.md 151 Bytes 8b34da11 over 5 years Teme Kahsai README.md edited online with Bitbucket git-svn...
TODO.org 1.13 KB 22fe1c93 about 7 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler git-sv...
configure.ac 3.21 KB e8b6d5ca almost 6 years Pierre-Loïc Garoche Moved Makefile into src folder git-svn-id: ht...
lustrec.odocl 623 Bytes 3d134f43 almost 6 years Pierre-Loïc Garoche Doc file git-svn-id: https://cavale.enseeiht....
setup.ml 153 KB d1baac41 almost 6 years Xavier Thirioux corrected a bug that made an error silent, conf...
svnignore 103 Bytes 22fe1c93 about 7 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler git-sv...

Latest revisions

# Date Author Comment
ea1c2906 03/06/2015 11:09 AM Pierre-Loïc Garoche

Changed the option horntraces to a general traces option
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

3ca6d126 03/05/2015 11:48 PM Pierre-Loïc Garoche

Reactivated the generation of traceability information
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

8b34da11 03/03/2015 09:10 PM Teme Kahsai

README.md edited online with Bitbucket

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

7d9df109 03/03/2015 09:10 PM Teme Kahsai

added invariants

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

8d4fddd8 03/03/2015 09:10 PM Teme Kahsai

including invariants

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

5cf953ec 03/03/2015 09:10 PM Teme Kahsai

Fixed horn backend to make query for properties. More work needed for cex

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

f2b1c245 02/16/2015 11:52 PM Pierre-Loïc Garoche

Solved bug found by Teme about asserts.

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

e3373485 12/10/2014 11:15 AM Pierre-Loïc Garoche

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

40875a30 12/10/2014 11:14 AM Pierre-Loïc Garoche

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

790765c0 12/09/2014 04:54 PM Xavier Thirioux

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

View all revisions | View revisions

Also available in: Atom