bug correction in homomorphic extension
typo corrected in code generation for array memories (bad parentheses)
Math lusi (trigo)
bug corrected for allocation of dynamic arrays in node memory
node memory namespace bug corrected; library linear_ctl/arrays corrected
Updated list with new tests
Solved bug:- loading lusi- loading lib in lusi files: "in m" is now "lib m"
Additional checks in transpose
Check node is stateful
Bug solved on tuple equalities in expressions (eg. OK = (a,b,c) = (d,e,f))
Changed the load of lusi files: imported nodes or function can specify the linking lib and/or use a classical C prototype (without pointers).Parse updated as well as Makefile generation.
still computing disjoint clock information (for reusing more variables)
computing statically disjoint variables (to enhance resusability)
removed debug message
changed name generation to avoid conflict with C predefined symbols; added checking for declared but not defined node symbol
- some minor adjustments...
- corrected causality bug (cf. previous commit)
liveness analysis improved. BUG found in causality wrt clocks...
- modified example (arguments are now in the right order wrt clock declaration). - debugged liveness analysis...
- reimplemented computation of dead variables - added computation of a reuse policy (depending on types) - not yet used though, would have to change code generation in order to be useful...
added liveness analysis for reusing dead variables. Not yet used.
improved code generation by factorizing out arrows
Version compatible avec le francais
Updated test script: changed path and verbose mode
Moved tests outside of source code to avoid useless duplication.
Added Alice Tailliar example
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