work on spec generation almost done
forgotten file
start again with spec representation
start with Spec AST generation
add -O -1 flag to disable fusion of conditionals
missing file
corrections on loggers + spec in AST
patch de Xavier pour réparer -O 3
the generation of ACSL from machine code reveal too fragile as it occurs after several transformations (eg. fusion)
Update .gitlab-ci.yml file
update CI
Merge branch 'master' of gitlab.isae-supaero.fr:l.brun/lustrec
move arrow spec in its own header
working proto
Almost works!
first version that is parsed correctly by Frama-C
first draft: to be tested with frama-c
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
generic ACSL spec generation
start generating ACSL spec
Merge branch 'dune'
some rewriting in C backend pretty-printer
minor rewriting
missing header files in dune install targets
disable tests in gitlab CI
setup tests for dune
add gmp dep
fix almost all warnings
rewrite a bit the menhir parser
forgot to generate opam file
missing dune-site dep
missing zarith dep
try to fix ci
isae gitlab version does not support parallel jobs matrices
migration draft on dune
add thread dependency required by z3 lib
Merge remote-tracking branch 'origin/unstable'
master creation
moved from Num to Zarith. IMpacted main.ml ad uses of Z3 in zustre_cex and seal-extract
work in progress for ACSL support
Merge branch 'lustrec-seal' of https://cavale.enseeiht.fr/git/lustrec into lustrec-seal
Added some missing locations in tiny plugin
Tiny: solved issue with a change in the Location.dummy signature
forgotten to uodate log.ml
1) log messages are now flushed. 2) very long computation times due to naive code to check for unused variables are now much shorter
- Primitive Tiny backend- Renamed Mpfr to lustrec_mpfr- Introduced dependency in Zarith. Trying to move away from Num
[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)
printing nodes + more progress on seal export
[MPFR] add more functions and better treatment of print output variables in main.c
temporary changed in the expression printer
preserving types/clocks when possible
Moved some code
- 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
Commenting out unused variables
Array access: solved issues in C backend when basic operations in array access dimensions. Also better handling in EMF, ie further normalization through new equations
comment some code to avoid warning at compile time
solved bug 91 on cavale: spurious commas in emf backend
Merge branch 'unstable' into lustrec-seal
better location error
Optimize_machine- Constants were improperly unfolded- Do not unfold clock definition
big: missing case with substituting expressions
- tag_true and tag_false moved to lustre_types- real constants are hidden in Real.ml{i} module
[seal] more progress on seal extract
sort of slicing for machine code
kind2 option for printing expressions
Reactivated Unfold constant
partial evaluation for basic lib
Module to manipulate real constants. For the moment we Num
cleaning debug logs
reactivating the unfolding of constants
flatten dependencies in schedule to make sure all required equations are used
[emf] added the names of the cocospec properties in the output json
better negation of constants
Better treatment of arrays in EMF backend. Be careful it may have changed the way enum types are declared
More kind2 outputs: clocked fun call + clocked and restart fun call
seal: now deals with enum
when condition in kind2 printer
EMF backend issue
seal: stateless systems
every in kind2 syntax
[seal] delt with Merge and when[printer] more kind2 syntax