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
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".
trying to improving pretty printing. Not so perfect for the moment
[bug solved] issues with asserts (invalid eqs scheduling)
added pp_imap function
- Adding new Makefile target for regression test- Version now includes current git branch
Removing silly warning message
Missing file c_backend_lusic
Cleaning output:- no more classic display for ocamlc- compilation warnings removed
Merge branch 'unstable' into merge_mauve_unstable
_tags is generated now
Cleaner configure autoconf script
Merge branch 'testgen' into merging_unstable_testgen
Merge branch 'unstable' into merging_pluginsNon regression results were similar to master branch
Removing generated file
Printing reals in Horn backend
Solved a bug in the compilation of asserts. Now different behavior depending on the backend:functional: keep it as isnon func: introduce a fresh local var v and replace assert(e) by v=e; assert (v);
functional_backend function moved to corelang
More informative error message in case of untyped value
Updated deps: requires ocamlgraph as an ocamlfind package
Deprecated function changed for compatibility with ocaml 4.04
This is the first merge that does compile. Not tested yet.
first version (doesn't even compile) of mutation and test generation standalone command: lustretmostly a recovery of an ancient svn repo: mutations