Added declaration/definition of stateless/stateful nodes. The 'function' keyword is for stateless nodes only, the 'node' keyword is any kind of node. Improves compilation and paves the way for more optimizations.
- work in progress for stateless/stateful status computation (to turn conditionals into merges, which yield more efficient C code)
corrected bugs in clock generalization that produced pessimistic C code (not wrong though); corrected bug with node importation policy wrt (re)declaration, (re)definition...
- added struct types declaration - added constant definition with a struct type - added checking for multiple definitions of nodes (behavior was buggy) - better and more uniform error messages for undefined/already defined symbols
We still need struct expressions...
work in progress for struct types...
more steps towards struct types...Cette ligne, et les suivantes ci-dessous, seront ignorées--
M trunk/src/corelang.mliM trunk/src/type_predef.mlM trunk/src/main_lustre_compiler.mlM trunk/src/types.mlM trunk/src/printers.mlM trunk/src/typing.ml...
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.
- stupid svn had removed a file, again
- 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
Updated script. Does not seem to be fully functional yet.
Added default ensures statements
- added dummy_lib.lusi (accidentally removed !?)
- 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
Updated version of test script: timeout for z3
Fixed bug on the main part
Cleaning useless files
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
Manually corrected version of ex3. Should integrate the modifications
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
lego robot example
missing dummy lib for arrays
- 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
Lustre interfaces: lusi files are generated and used. Remaining work: create a good makefile and add the appropriate #include, fix issues with Arnaud's benchmarks (old syntax)
Moved files to trunk in lustre_compiler