CristalCaveGem » LustreC

clean handling of undefined node application

Math lusi (trigo)

Solved bug:
- loading lusi
- loading lib in lusi files: "in m" is now "lib m"

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.

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

more steps towards struct types...
Cette ligne, et les suivantes ci-dessous, seront ignorées--

M trunk/src/corelang.mli
M trunk/src/type_predef.ml
M trunk/src/main_lustre_compiler.ml
M trunk/src/types.ml
M trunk/src/printers.ml
M trunk/src/typing.ml...

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

- 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 trunk modif in branch

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

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?

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

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

Moved files to trunk in lustre_compiler