CristalCaveGem » LustreC

Restructured the main: call to optimization, scheduling performed out of machine_code, etc
Merge Xavier last commits
Unfinished lustre backend

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

Updated list with new tests

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

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

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

Version compatible avec le francais

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

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

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

Added Alice Tailliar example

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

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

- 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

- 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

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

Added default ensures statements

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

- added dummy_lib.lusi (accidentally removed !?)

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

- 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

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

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

Minor bugs

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

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 of the inlining process

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

Improvements as suggested by e. Noulard: better install of include; modified generated makefile

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

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-ef0dd855326e

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-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@152 041b043f-8d7c-46b2-b46e-ef0dd855326e

lego robot example

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

missing dummy lib for arrays

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

- small bug correction in dimension typing
- #open keyword instead of open
- dummy generic matrix/vector library interface added
- modified examples according to the new syntax

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

Merge (if it works) of the lustre interfaces branche providing lusi files into trunk

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

Moved files to trunk in lustre_compiler

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