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
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
Missing file c_backend_lusic
Cleaning output:- no more classic display for ocamlc- compilation warnings removed
Merge branch 'unstable' into merge_mauve_unstable
Merge branch 'testgen' into merging_unstable_testgen
Missing files
Merge branch 'unstable' into merging_pluginsNon regression results were similar to master branch
Printing reals in Horn backend
Cosmetic changes
More informative error message in case of untyped value
Deprecated function changed for compatibility with ocaml 4.04
This is the first merge that does compile. Not tested yet.
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
adding c++ backend
fix tracebility
Working on EMF backend to express cocospec infos as Simulink blocks
[Horn] Updated traceability of Horn backend to deal with fby (arrow machines)
Revert some ocaml code to ocaml 4.01 compatibility
Merge branch 'github_master' into integ_github_jan10Intregrate all modifs by Teme et al
Merge branch 'master' of https://cavale.enseeiht.fr/git/lustrec
Changed the generated C file to produce input and output csv files (named inXX and outXX)
fixed sfunction detetction
adding math.smt2
Solved some issues with commited code (like it doesn't compile). The code was written by Teme's student and- did not rely on existing typing.ml function- used strange fprintf code
Code was refactored but old stuff kept in comment just in case. Will have to be cleaned at some point.
adjusting travis
Merge branch 'master' into master
adding sfunction support
making library statically link to horn backend
adding -I options to lustrec
updating to onera version 30f766a:2016-12-04
Arrays
adding onera automata version
Ongoing work on c backend for makefile. Does not compile yet
moving C files name declaration in backend. Preparation for additional cmake target
...
new branch for merging mpfr and horn
full merge of salsa/mpfr and master
fixed assert compilation in case of stateless program
Updated to onera_git commit version 9421e24
Resolved conflict when merging salsa with horn_encoding. The current branch is the most updated.
Merge branch 'salsa' into merge_salsa_horn_2Postponed conflicts to be solvedConflicts: src/_tags src/backends/Horn/horn_backend.ml src/machine_code.ml src/main_lustre_compiler.ml src/myocamlbuild.ml.in src/optimize_machine.ml
Clean old and resolved TODO
fixed a z3 bug for => within Horn clauses
Introduced the opposite of Reset call: NoReset. This simplify the general compilation process and makes the code more symmetric, hence simpler and clearer code.
solved bug: missing parenthesis in enum typedef
Refined the dependencies in the generated makefile
Merge branch 'master' into horn_enum_types
Conflicts: src/backends/Horn/horn_backend.ml
Solved bug with C backend
Added by default -O0
travis
Plugin based framework
major branche merging salsa/mpfr with trunk
bug correction in typing: tuple types were computed but not recorded
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@485 041b043f-8d7c-46b2-b46e-ef0dd855326e
Refactoring of the horn backend with Reset/Step instead of Init/Step.Teme, please perform a string non regression test wrt the previous version, to make sure we have the same model checking results.
remove duplication
bug corrected: in some cases, local const vars were assigned twice
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@483 041b043f-8d7c-46b2-b46e-ef0dd855326e
numerous bugs corrected:- bug in expansion of array accesses with constant arrays- bug in printing complex array indexes (not C compliant)- bug wrt C99 typing policy for constant arrays- bug in signaling wrong useless static input
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@482 041b043f-8d7c-46b2-b46e-ef0dd855326e
fixed a printing bug in horn backend
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@481 041b043f-8d7c-46b2-b46e-ef0dd855326e
changes to horn
bug:double def fr init rules
revereted to previous commit
Two fresh branches :)to manage enum and arrays in the horn backend.
Bug fixed (454), more on travis
small logging change
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@455 041b043f-8d7c-46b2-b46e-ef0dd855326e
first commit
do not use lusi for horn, and some logging for horn
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@451 041b043f-8d7c-46b2-b46e-ef0dd855326e
some tiny mistakes corrected...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@445 041b043f-8d7c-46b2-b46e-ef0dd855326e