Cocospec: parsing, normalizing and processing machines for contracts.
Merge branch 'salsa' into lustrec-seal
Reformating plugin signatures. Better report management
New -salsa-disable option
Merge branch 'unstable' into salsa
Merge branch 'unstable' into lustrec-seal
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....
More work on Salsa plugin
[salsa] more debug messages
[salsa] introducing sliced temporal variables
Tuning the pretty printing of Salsa plugin
Homogenizing the API for salsa and its use within the plugin
Some tentative improvement of Salsa plugin. Not satisfying yet
NumMartel functions
Merging unstable into salsa
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
- Normalization parameters (alias and unfold_array) are now provided as parameter- program type renamed as program_t- Initiating the lustrev tool with dependencies to z3 and seal.
Ongoing work on salsa: introduce slicing of expr
Updated Salsa plugin to latest version of Salsa.Some issues wrt machine type features.Work in progress
[salsa] cleaning verbose logs
- Addtional encapsulation of machine_code instr in a struct to enable future extension of type with more metadata.- Improved EMF backend with META information
Cleaning output:- no more classic display for ocamlc- compilation warnings removed
Modified Salsa plugin to apply the algorithm until no more progress can be made
More debug print
on joue avec l'affiche des floats
- Print the range before/after the transformation of the expression- Use %e to print floating point error
Plugin based framework
major branche merging salsa/mpfr with trunk