messages d'erreurs terminés
more error messages
some more error messages
start to write error messages
prepare for the modern error handling of Menhir
minor rewriting
setup tests for dune
rewrite a bit the menhir parser
migration draft on dune
- Refactored Error exception and messages- Bugs in partial evaluation for equalities among bool constants and a nice recursive call generating a stack overflow! Now solved- Setup a timeout for z3 in seal- Better log for seal
Merge branch 'unstable' into lustrec-seal
better location error
- tag_true and tag_false moved to lustre_types- real constants are hidden in Real.ml{i} module
Better treatment of arrays in EMF backend. Be careful it may have changed the way enum types are declared
Produce true/false statements as constants
Cocospec: parsing, normalizing and processing machines for contracts.
Some progress on compiling cocospec contract.Contract resolution still need to be done as well as dealing with the machine code level and so on.
Moved lusic to .h printer after normalizing in case we want one day to produce ACSL from a normalized specTrying also to extend the parser to deal with imported nodes....
Unified compilation of lusi and lus filesDifferent parsers yet but shared process.In case of lusi input the C backend is bypassed since the .h is generated from the lusic and no C code should be generated since it may overwrite existing manually written code...
Added include directive that directly inject a lustre source file in the prog
- Module.load_header and load_program were merged.- Contract were extended with list of statements.
Merlin files
- Global type env and clock env now availble as a global reference (Global module)- Adapted the parsing of specification with a cocospec compatible one- The data structure of contracts is now almost cocospec compatible- Lustrec-test has been updated to use the newest syntax
Some refactoringAdapted the parser/types/constructors for cocospec syntax