CristalCaveGem » LustreC

Improved EMF backend. Working on the whole fmcad suite

Copied Printers.pp_expr functions to Horn backend to escape < and > in XML traces output

- 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

Changed encoding of matlab expression inputs from u(xx) to uxx.

EMF backend now relies on machine code representation.
Impact:
- EMF backend has an extra machines argument
- specific option to avoid merge of ite constructs
- set_backend function to improve backend selection

Most code was extracted from seahorn_backend through c0f8

fixed matlab output

Changed the matlab function backend

Missing file