first steps towards struct types...
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
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)...
In order to export any type of constants, moved type definitions from .c to .h
Generate extern declarations for constant as well.
- 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
Merge inlining branch within trunk.The test target requires branch lustrec/horn as binary lustreh.
Do not use stable sort because it requires recent ocamlgraphlibrary (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 printerGeneration of a witness with both the main node and hte inlined main nodeTest 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
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