rev machines in emf
JSON EMF
Better JSON for EMF backend
Better EMF output, solved some invalid JSON produced
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.
Some progress on EMF bqckend. Refactoring machines code
Merlin files
EMF export of local type definition (for simple types)
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....
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
[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
[EMF] Less verbose
[EMF] adding original name field in the JSON
[EMF] Added the reset signal (the every argument) as input to the JSON struct
Issue with clocked expressions. Now handled throught a local branch, ie. a single action block in Simulink
[EMF] improved feedback on reset calls
[EMF} missing brace
[EMF] missing quotes
[EMF] improved alignement of braces + solved (naother) bug in shortening of ids
[EMF] more hash
Merge branch 'unstable' of https://cavale.enseeiht.fr/git/lustrec into unstable
[EMF] bug solved, some ids were not hashed
ange ID length
blup
[EMF] simplify branches with single case as regular instructions
[EMF] Disable join of guards in EMF backend
[EMF] protect machine names
[EMF] protect more field
[EMF] Protecting print of names to ensure a length < 50. Remove the middle part of the string and inject a hash of it.
Renamed math lib into lustrec_math to avoid conflicting calls to <math.h>
Provides type compatible with Matlab types in EMF backend
[EMF backend] Merging branches
bug fixed: Inputs for branches solved
Proper integer index for enumerated branches
Enumerated datatypes as integer
Refactored EMF backend. Handle now the call to existing math and conv libraries
EMF backend: each branch provides the inputs and outputs
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