CristalCaveGem » LustreC

Ada: pretty printing functions for values and assignments in adb

Ada: typo

fix conflicts

Ada: pretty printing of reset function

Ada: Remove generation of init and clear and some refactoring around
prototype.

Merge branch 'ada' of https://cavale.enseeiht.fr/git/lustrec into ada

Ada Change private to limited private for State type package.

Ada: first pretty printing functions for adb

Ada: Temporary change

Ada: Add local variable declaration for step

Ada: Last correction was incorrect

Ada: Correct a bad copy-paste

Ada: Add the generation of the wrapper file : the main ada file and the project. It is called
only if the main node option is given to lustrec. This feature implied some refactoring. Also
added some OCaml Doc to undocummented functions.

Ada: Add to the machine state all its subinstance states. Improve also identifier cleaning

Ada: Changed type name for states and normalized variable name to match ada requirements.

Ada: Add prototype of the four procedure in the adb generation

Ada: Add the state variable in the ads, type definition and as parameter of all procedure

Ada: Move some functions from ada_backend_ads.ml to ada_backend_common.ml

Ada: Remove useless comment

3 main modifications :
- Create a new file : ada_backend_common.ml which contains all the function common to adb and ads.
- Add comment to function
- Generate the procedure prototype in the ads

Basic structure for Ada backend

Ada: skeletons for Ada compiler

math fun lib support in MPFR

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....

Removed Contract contruct: imported node should be enough. Solved some warning at compile time

Byte/String bug reappeared

Merge branch 'master' of https://cavale.enseeiht.fr/git/lustrec

Solved bug#57: issues when indirect init of a pre in horn-traces

strange bug (ill-typed source) wrt Bytes/String conversion

updated division for Horn clauses

corrected euclidean division in C code

Merge branch 'euclidean' of https://cavale.enseeiht.fr/git/lustrec into euclidean

introduced euclidean/C-like division in C code generation

Euclidean div/mod treatment in Horn backend

Issues with typing pp_basic_lib_fun

Tuning the pretty printing of Salsa plugin

Basic library printers moved into backend specific printer files

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

Recursive resolution of dependencies

[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

Type issue Bytes vs string

[main] enum typedef in C use the original lustre filename as identifier. This commit cleans the filename to remove dots.

[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

Solving a warning with ocaml 4.04 and uppercase_ascii. Provides backward compatibility for 4.02

Issue with clocked expressions. Now handled throught a local branch, ie. a single action block in Simulink

C backend: solved the issue of long name in generated binaries.

first solution to address very large identifiers in node names, logs, and generated binaries

[EMF] improved feedback on reset calls

Merge branch 'dynamic_inlining' into unstable

[EMF} missing brace

[EMF] missing quotes

Merge branch 'unstable' into dynamic_inlining

[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

Refactor error printing.

[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>

[HORN] handled asserts in stateless node step rule definition

[HORN] Protect names of stateless nodes with a _fun suffix. This was conflicting with existing names in Z3, ie. "abs".
[HORN] Better treatment of stateless nodes collecting semantics
Fixes issue #13 on github: https://github.com/coco-team/lustrec/issues/13

Provides type compatible with Matlab types in EMF backend

[EMF backend] Merging branches

Refactored some code: optimization of machine

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

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

fixed matlab output

Changed the matlab function backend

Merge branch 'unstable' into seahorn_a6df3
a6df3 is the initial commit of branch seahorn

[Horn] Workaround to prevent the use of declared keywords as node name