corrections on loggers + spec in AST
patch de Xavier pour réparer -O 3
generic ACSL spec generation
Merge branch 'dune'
fix almost all warnings
migration draft on dune
1) log messages are now flushed. 2) very long computation times due to naive code to check for unused variables are now much shorter
[bug cavale 93] solved: issue when resetting a stateless node. Now generating a warning and forcing the stateful status. Could be improved to remove the reset statement. (TODO)
- 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
better location error
removed reload of external modules when checking algebraic loop.
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.
- Dep type with a tuple has been replaced by a record type- Modules now is more integrated and performed the building of the type/clock env. previously some computation were performed twice by different functions. Some of these functions have been moved from compiler_common to modules
Merge branch 'unstable' into lustrec-seal
Merlin files
Removed Contract contruct: imported node should be enough. Solved some warning at compile time
- 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