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
minor bugs solved in printer: guarantee vs guarantees in cocospec. Imported node shall not be printed as regular code since it is not part of the grammar yet. Kept them as comment.
keep the open top declaration when loading a module. It may be useful later when producing a lustre file
lustret: do not reload opened modules when generating the mcdc output
lustrev seal: ongoing work on extraction as dynamical system. Still not working yet
lustrev: removed the check of no dependencies
comestic changes, removing useless logs
z3 as an optional pacage in configure
Merge branch 'ada' into lustrec-seal
Solved issue btw mpfr and conv functions (int_to_real was not handled)
Merge lustrec-salsa
Correction d'import
Merge branch 'unstable' of https://cavale.enseeiht.fr/git/lustrec into vhdl
Solved scopes print order
Ada: Start cleaning Ada to prepare for why beckend
Merge branch 'ada' of https://cavale.enseeiht.fr/git/lustrec into ada
Ada: Lot of specification is exported in Ada. We use ghost code to store all states,we generate the transition pridicate but also the invariant. But two problems, occured.The first one is a visibility problem for the record which is private but must bepublic for ghost variable which have to be public for specifaction. The second...
No need for open lustrec_math inside simulink_math_fcn. It creates an error when they are both imported in the same lustre file.
Debug en cours sur les calculs Salsa
doc: use SVG format instead of PNG for dependency graph
Doc: update rule and remove old module in odocl
Ada: First support for transition predicate generation.
Machine_code: Make a correction in the arrow machine creation : use the same polymorphic type in variables and values.
Ada: Correct some errors in printing
Ada: Refactor Ada Backend to reduce redundancy, make it more modular and more simple.
Merge branch 'lustrec-seal' into ada
Ada: Correct ada main to handle statelles top level node
Merge branch 'lustrec-seal' of https://cavale.enseeiht.fr/git/lustrec into lustrec-seal
install notes
rev machines in emf
JSON EMF
more explanation in case of failure. Still dirty
Better JSON for EMF backend
Resolved sort order of nodes
Ada: - Correct the merge with lustrec-seal - Improve support for builtin function(still work to do) - Add generation of a gpr file for lib(without main). - Add var initialisation in the reset, still work to do.
Cocospec: parsing, normalizing and processing machines for contracts.
Better EMF output, solved some invalid JSON produced
Cleaning C backend - removing unused functiionsPreparing for coming ACSL
INSTALL file
Merging branches, disabling the specification print in Ada backend. Should be re-enabled at some point
Minor modif on seal
Reorganizing folders
Merge branch 'salsa' into lustrec-seal
Reformating plugin signatures. Better report management
Better production of trace files.By default traces are not produced. Requires the option -t to produce them
Serious refactoring of scopes plug-in:- now properly records the scopes- only register requested ones
Merge branch 'unstable' into salsa
bug solved: issues with main node input access when using scope plugin
Ada: Correct branch exporting to handle boolean match(using an ada if)
Ada: Improve input/output of main ada file
New -salsa-disable option
num as a package
Ada: Add pretty printer for case
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.
Ada: Some indentation
Ada: Add generation of step calls and refactor prototypes and ads printing to handle staless instance.
Ada: Refactor the instantiation code and instance code, instead of passing the machine listto the pp_file and all subfunction in adb generation we pass a list of typed instance whichcontains the submachines directly with the instance name and the substitution.
Ada: Corrections of some bugs discovered with lustrec-tests
Ada: Add readers and printers for main.adb to match c tests.
Ada: Add the prefix ada for variable named with an Ada reserved name.
Ada: Correct contract printing
Also available in: Atom