Tiny verifier: better control of the print commands
Updated tiny plugin to deal with boolean variables, since the latest extension of tiny now deals with these!
add thread dependency required by z3 lib
moved from Num to Zarith. IMpacted main.ml ad uses of Z3 in zustre_cex and seal-extract
Using deriving_ppx to derive show_ functions for the main types defined in lib/Applying the same procedure of operator specialization taken from the C backend to TinyLustrev has now a functional Tiny plugin : * -unrolling option has been renamed -duration because from an outside observer it is the length in steps of the abstract simulation...
Merge branch 'dune_transition' of https://cavale.enseeiht.fr/git/lustrec into dune_transition
Mise à jour README.md
adding lusic building of libraries when installing includes
Cleaning up configure.ac by removing now useless informations
Zustre/Z3 dependency: switched from -R to -rpath to solve compatibility issues with Linux/Gcc vs OSX/Clang
reactivating all plugins
restricting opam to core install
fixed some code in salsa plugin migration
Opam not generated by dune
Explanation about the Makefile
Add explanation for mlmpfr and mpfr version pinning
Transition to dune build systemImprovement of opam integrationDockerfile based on AlpineDockerfile based on UbuntuUpdate the README.md
...
added some cleaning about hash-tables used for typing, clocking, etc.
Correctif
Passage à dune v2
Passage à dune
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
disable lustret and tiny error
Merge branch 'lustrec-seal' into cocosim_master
- 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
disable lustrev and lustresf
[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
No more when suffix in clocked variables with kind2 option
Produce true/false statements as constants
removed reload of external modules when checking algebraic loop.
scheduling now report unused vars and remove their definition instead of stopping processing.
kind2 output for printer. global option available
Seal: solved issue with guards merging
Sorting expressions: less bugs
valid _verif node for seal-export lustre
No space in comments
Seal export lustre
Work in progress: higher level constructs for lustre elements
Contract printer cocospec
No space before contract kwd
Printing trailing zeros in real constants
Export cocospec contract
configure.ac
Remove dep
Seal deps + Z3 pin opam
Output folder for seal-extract
Seal-export to a new file
seal-export: produce the output as well. Could be simpler
Seal-extract: first serious version. Guards are gathered as a single expression
Updated version seal-extract
Working version of seal-extract. Heavy load on z3.TODO: improvement through memoization
Corelang function: push_negations that propagate negations in leafs of the expression
Better extraction in lustrev-seal
Zustre: Bug solved in const injection for reals
Addressed a TODO in MCDC Pathconditions: simpler condition for single expression
- More systematic translation for mutation- copy_var_decl now keeps the generated type
Mutation translates now ids in cocospec import
Also available in: Atom