json-parser: add string_of_XXX functions for assertions
json-parser: test exception for variables
json-parser: switch arguments for assert_equal (expected/actual)
json-parser: use JSON_parse_error exception
json-parser: more tests with single variables
json-parser: change variables names in tests
json-parser: add test for boolean variable true
json-parser: refactor first test
json-parser: first unit test for JSON parser (variables)
json-parser: prepare tests in Makefiles and _tags.in
json-parser: clean packages and _tags.in
json-parser: replace assert with exceptions
json-parser: clean files names and directories
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
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
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.
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
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.
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
- 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
Restored common_option definition. Was removed by a non delicate merge.
Bug solved: EMF backend was forced
Merge branch 'unstable' into seahorn_a6df3a6df3 is the initial commit of branch seahorn
[Horn] Workaround to prevent the use of declared keywords as node name
Solved printing bug in Horn backend
Improved include folders behaviors:- allow multiple -I dir, will be used in order (first one declared is first used)
- when declaring a global library #open <foo>, foo is first checked in local folders, than in global one (install path). This does not apply to local libraries opened with #open "foo".