EMF backend: each branch provides the inputs and outputs
Merge branch 'unstable' of https://cavale.enseeiht.fr/git/lustrec into unstable
small modifs in EMF format
Branchs output in EMF is only the intersection of each branch defined flows
Full rewrite of EMF backend.
Ongoin work on EMF backend. Commit to store a working version. More work to do on clocks and resets
Improved EMF backend. Working on the whole fmcad suite
- 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
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
Working on EMF backend to express cocospec infos as Simulink blocks