json-parser: use Logs and Cmdliner librairies
clean _tags.in for YoJSON package
json-parser: remove Const_bool and use Const_tag
parser-json: clean main program + add pp for vars
parser-json: correct parsing of real constants for variables
parser-json: add variables in parsing
parser-json: final version of parser with new types
minor changes in _tags.in
TMerge branch 'unstable' into json-parser
bug correction: each var_decl must be unique and not shared as a global var
[lustresf]: tuple of false values for initial state
A fresh option to print with declared types instead of inferred ones
parser-json: first steps to integrate JSON parser
add files in gitignore
lustresf: Better construction of lustre ast. Still more work to be done.
Even prettier pretty printing. Is it even possible to improve?
Moved stateflow tool in src/toolUpdated the makefile to compile lustresfNot working yet
Missing readme file in the import
Initial import of stateflow_cps_semantics (github)
C backend: solved the issue of long name in generated binaries.
Normalization: force normalization of "every" arguments
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
First working version of algebraic loop resolution. Disabled by default.
[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
[EMF] simplify branches with single case as regular instructions
[EMF] Disable join of guards in EMF backend
Working on algebraic loop diagnostic and resolution
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.
A math library for some functions used in Simulink
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
Addressing node calls in asserts
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
Renamed ISet of Machine_code to VSet: was sets of variable and was conflicting with ISet from Utils which carries strings.
small modifs in EMF format
Branchs output in EMF is only the intersection of each branch defined flows
Full rewrite of EMF backend.
New global option to normalize simple call to std lib functions (+,-,*, comparison ops, etc).This is used in EMF backend.
Ongoin work on EMF backend. Commit to store a working version. More work to do on clocks and resets
Added a feature to alias ite contructs argument. To be used by EMF backend
Bug solved: lusic dependency of mpfr
Bug solved in include dependencies in install target
Improved EMF backend. Working on the whole fmcad suite
Copied Printers.pp_expr functions to Horn backend to escape < and > in XML traces output
Issues with Causality and asserts
const that are not dimension types should not be used to evaluate dimension expression. This happened with const variables denoting real values.
Moved to 1.5 dev
Preparing relaease LustreC 1.4 Xia/Xiang
Print branch in configure.ac
Merge branch 'unstable' into master
More tests in default test target: main focus on C backend
Cleaning debug messages
forcing introduction of new equations for fcn calls in asserts
Solved bug in machine code generation for asserts that contain memories
Cleaned horrible ocaml practice (optional parameters and mli issues)
- 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
Turn an option to off by default: it was triggering scope plugin automatically
Providing means to have specification as dynamic checks.[bug] seems to crash with EMF backend
Updated scope plugin
Default precision for real values printing
io_frontend header with new functions
- Added a precision parameter for io_frontend "real" types- New fonction in plugins: main_loop_body_prefix
Flushing after printing in io_frontend functions
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
Removed duplicate tan definition in math.lusi
add tan function to math.lusi
fixed matlab output
Changed the matlab function backend
Merge branch 'unstable' into seahorn_a6df3
Improved dependencies for install target
Restored common_option definition. Was removed by a non delicate merge.
Bug solved: EMF backend was forced