CristalCaveGem » LustreC

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

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

fixed matlab output

Changed the matlab function backend

Working on EMF backend to express cocospec infos as Simulink blocks