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

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

- 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

- tag_true and tag_false moved to lustre_types
- real constants are hidden in Real.ml{i} module

Cleaning C backend - removing unused functiions
Preparing for coming ACSL

Merge branch 'salsa' into lustrec-seal

Better production of trace files.
By default traces are not produced. Requires the option -t to produce them

Unevaluation of types and clocks dimension has been already performed before producing the lusic.

- Dep type with a tuple has been replaced by a record type
- Modules now is more integrated and performed the building of the type/clock env.
previously some computation were performed twice by different functions. Some of these functions have been moved from compiler_common to modules

Merge branch 'unstable' into lustrec-seal

math fun lib support in MPFR

Merlin files

Pretty serious update:
- a bug in regressio ntest Simulink/integrator_ext_IC_matrix_test revealed the following (serious issue):
when building the list of instruction (in the machine code) the access to variable were hardcoded to LocalVar or StateVAr depending whether the variables was part of the identified memories....

Removed Contract contruct: imported node should be enough. Solved some warning at compile time

Merge branch 'vhdl' of https://cavale.enseeiht.fr/git/lustrec into lustrec-seal

updated division for Horn clauses

corrected euclidean division in C code

Merge branch 'unstable' into lustrec-seal

introduced euclidean/C-like division in C code generation

Issues with typing pp_basic_lib_fun

Tuning the pretty printing of Salsa plugin

Zustre backend

Basic library printers moved into backend specific printer files

Further restructuring:
- arrow.ml* to define basic builder for arrow (node, name, ...)
- machine_code_common similar to corelang but for machine_code (printers, some builders, ...)
- machine_code restricted to the translatation from normalized nodes to machines

MLI for normalization and machine_code.
Structs defining machines are now in machine_code_types

- Makefile: solved dependency problem when compiling include lusi
- Renamed type declarations as lustre_types and machine_code_types

Recursive resolution of dependencies

[general] large modification: added machine types, a second typing phase dealing with machine types (eg uint8)
typing was transformed as a functor and parametrized by basic types (int/real/bool)
it can also be applied multiple times on the same program

[main] enum typedef in C use the original lustre filename as identifier. This commit cleans the filename to remove dots.

Solving a warning with ocaml 4.04 and uppercase_ascii. Provides backward compatibility for 4.02

C backend: solved the issue of long name in generated binaries.

first solution to address very large identifiers in node names, logs, and generated binaries

Refactor error printing.

- Added a field lustre_eq to machine instruction in order to record the originating lustre equation
- EMF backend now impose the optimization level to be set to 0 in order to avoid equation elimination that would render traceability difficult
- Options.ml has been split into Options.ml / Options_management.ml. Options.ml only contains references and no functions

- Addtional encapsulation of machine_code instr in a struct to enable future extension of type with more metadata.
- Improved EMF backend with META information

- Added a precision parameter for io_frontend "real" types
- New fonction in plugins: main_loop_body_prefix

Improved include folders behaviors:
- allow multiple -I dir, will be used in order (first one declared
is first used)

- when declaring a global library #open <foo>, foo is first checked
in local folders, than in global one (install path). This
does not apply to local libraries opened with #open "foo".

trying to improving pretty printing. Not so perfect for the moment

Missing file c_backend_lusic

Cleaning output:
- no more classic display for ocamlc
- compilation warnings removed

Merge branch 'unstable' into merge_mauve_unstable

Merge branch 'testgen' into merging_unstable_testgen

Merge branch 'unstable' into merging_plugins
Non regression results were similar to master branch

More informative error message in case of untyped value

Deprecated function changed for compatibility with ocaml 4.04

adding dealloc

Merge branch 'master' into mauve

added deallocation for dynamic memory allocation scheme

adding & in shell

mauve generator with annotations

mauve generator: first shot

adding c++ backend

Revert some ocaml code to ocaml 4.01 compatibility