CristalCaveGem » LustreC

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

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

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

Merge back horn backend branch in trunk

Merge trunk modif in branch

desome

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

inliner function

Minor bugs

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 will do.
Fixes Issue #49: https://cavale.enseeiht.fr/redmine/issues/49

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

better error message for tuple type mismatch

again, debugged tuple subtyping

removed debug printing

corrected wrong subtyping rule for tuple assignment

added subtyping in equations (rhs may be a subtype of lhs)

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

Fixed bug on the main part

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.

...

Is it working?

Working on bugs

Second (almost) working version

First (almost) working version

Ongoing ...

Ongoing ...

In the middle of the coding process. Just pushing thinks

The missing file

Initial copy of the horn output version. Not really working yet

- Renamed the only target of the generated makefile
- Solved bug: xor are now printed as bitwise xor in c : a ^ b and not a xor b.

- work in progress for interface typing

- 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

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

Moved files to trunk in lustre_compiler