Refactor error printing.
[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.
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.
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
Missing file
_Bool are unsigned integer. The cast as a _Bool is delayed until the end of the function
Merge branch 'unstable' into seahorn_a6df3a6df3 is the initial commit of branch seahorn
add tan function in math.lusi
[Horn] Workaround to prevent the use of declared keywords as node name
Better dist-clean
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".
Solved dependency in Makefile
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
Cleaning test folder. Now generated with ctest/cmake
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
Missing files
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
Cosmetic changes
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
another issue with an old merge: missing nums dep
adding dealloc
Merge branch 'master' into mauve
added deallocation for dynamic memory allocation scheme
adding & in shell
mauve generator with annotations
mauve generator: first shot