CristalCaveGem » LustreC

more compact assign clauses for state variables, and remove useless memory pack predicates and assertions

more agressive optim propagation in spec in order to remove unecessarry existential variables that were eliminated (helps the solvers)

fix bug in handling state variables in nested expressions

add basic support to protect against some ACSL keywords

print (*mem) instead of *mem to avoid ambiguities with accesses

fix handling of state variables in spec expressions

fix bug where singleton tuples were generated

fix offline tests

add offline tests and fix a bug in generated spec where optimization was not performed

fix tests procedure

a working version for automata with 'last' case of enums as default case

working version for stateful contracts

proper generation of stateful contracts

proper handling of stateless nodes and automata

proper inductive case and no code generated for contracts

working version with additional asserts to make the axiom work

a version that almost work for the k-inuctive two_counters example

no need to reschedule in order to "clock-protect" the unitialized state variables in ACSL !

first draft with translated cocospec

first version working with stateless contracts

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 be
public 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 functiions
Preparing for coming ACSL

Merging branches, disabling the specification print in Ada backend. Should be re-enabled at some point

Merge branch 'lustrec-seal' into ada

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 list
to the pp_file and all subfunction in adb generation we pass a list of typed instance which
contains 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.