more precise spec for stdout
working spec in the main function
start instrumenting the main C function
comment dead code with (* XXX: UNUSED *) disclaimer
another step towards refactoring
refactoring first step
implement optimization on spec: IT WORKS
add memory instances to footprint lemmas
corrections for stateless nodes
reformatting
it works
work on new reset functions generation
work on spec generation almost done
start with Spec AST generation
add -O -1 flag to disable fusion of conditionals
corrections on loggers + spec in AST
the generation of ACSL from machine code reveal too fragile as it occurs after several transformations (eg. fusion)
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
generic ACSL spec generation
start generating ACSL spec
some rewriting in C backend pretty-printer
minor rewriting
setup tests for dune
fix almost all warnings
migration draft on dune
moved from Num to Zarith. IMpacted main.ml ad uses of Z3 in zustre_cex and seal-extract
- Primitive Tiny backend- Renamed Mpfr to lustrec_mpfr- Introduced dependency in Zarith. Trying to move away from Num
[MPFR] add more functions and better treatment of print output variables in main.c
- 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
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
- tag_true and tag_false moved to lustre_types- real constants are hidden in Real.ml{i} module
[emf] added the names of the cocospec properties in the output json
Better treatment of arrays in EMF backend. Be careful it may have changed the way enum types are declared
EMF backend issue
Ada: Start cleaning Ada to prepare for why beckend
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...
Ada: First support for transition predicate generation.
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
rev machines in emf
JSON EMF
Merge branch 'ada' into lustrec-seal
Better JSON for EMF backend
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.
Better EMF output, solved some invalid JSON produced
Cleaning C backend - removing unused functiionsPreparing for coming ACSL
Merging branches, disabling the specification print in Ada backend. Should be re-enabled at some point
Merge branch 'salsa' into lustrec-seal
Better production of trace files.By default traces are not produced. Requires the option -t to produce them
Ada: Correct branch exporting to handle boolean match(using an ada if)
Ada: Improve input/output of main ada file
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
Ada: Correct the subcalls to reset for node with polymorphic type(like arrow)
Ada: Correct state print for variable assignement
Ada: Add a pp_with for general with ada statement
Ada: - Replace MStep and Mbranch output by Null to have compilable Ada. - Correct pp_value to print state access when the variable is memory
Ada: Removed useless function
ada: pretty print assignment statement for state
Ada: Start exporting spec
Merge branch 'ada' of https://cavale.enseeiht.fr/git/lustrec into ada
Ada: pretty printing functions for values and assignments in adb
Ada: Correct some errors on the type checking due to polymorphic type.
Ada: Removed from adb the print of clear and init.
Merge branch 'lustrec-seal' of https://cavale.enseeiht.fr/git/lustrec into ada
Ada: Change some loggging feature
Ada: Add new function to print package name from node spec to be called by adb backend.
Ada: Add support for arrows as an independent generic package, instantiated in each package using it. It required a lot of refactoring.
Ada: typo
fix conflicts
Ada: pretty printing of reset function
Ada: Remove generation of init and clear and some refactoring around prototype.
Ada Change private to limited private for State type package.
Ada: first pretty printing functions for adb
Ada: Temporary change
Ada: Add local variable declaration for step
Ada: Last correction was incorrect
Ada: Correct a bad copy-paste
Ada: Add the generation of the wrapper file : the main ada file and the project. It is calledonly if the main node option is given to lustrec. This feature implied some refactoring. Alsoadded some OCaml Doc to undocummented functions.
Ada: Add to the machine state all its subinstance states. Improve also identifier cleaning
Ada: Changed type name for states and normalized variable name to match ada requirements.