reformatting
work on new reset functions generation
work on spec generation almost done
fix almost all warnings
migration draft on dune
- tag_true and tag_false moved to lustre_types- real constants are hidden in Real.ml{i} module
Better EMF output, solved some invalid JSON produced
Added include directive that directly inject a lustre source file in the prog
Merge branch 'unstable' into lustrec-seal
Merlin files
Pretty serious update:- a bug in regressio ntest Simulink/integrator_ext_IC_matrix_test revealed the following (serious issue): when building the list of instruction (in the machine code) the access to variable were hardcoded to LocalVar or StateVAr depending whether the variables was part of the identified memories....
Removed Contract contruct: imported node should be enough. Solved some warning at compile time
Byte/String bug reappeared
Merge branch 'master' of https://cavale.enseeiht.fr/git/lustrec
Solved bug#57: issues when indirect init of a pre in horn-traces
Merge branch 'vhdl' of https://cavale.enseeiht.fr/git/lustrec into lustrec-seal
strange bug (ill-typed source) wrt Bytes/String conversion
updated division for Horn clauses
Euclidean div/mod treatment in Horn backend
Some progress on zustre2
Zustre backend
Basic library printers moved into backend specific printer files
Further restructuring:- arrow.ml* to define basic builder for arrow (node, name, ...)- machine_code_common similar to corelang but for machine_code (printers, some builders, ...)- machine_code restricted to the translatation from normalized nodes to machines
MLI for normalization and machine_code.Structs defining machines are now in machine_code_types
- Makefile: solved dependency problem when compiling include lusi- Renamed type declarations as lustre_types and machine_code_types
ongoing work on zustre backend
[general] large modification: added machine types, a second typing phase dealing with machine types (eg uint8) typing was transformed as a functor and parametrized by basic types (int/real/bool) it can also be applied multiple times on the same program
Type issue Bytes vs string
[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
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
[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".
Cleaning output:- no more classic display for ocamlc- compilation warnings removed
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
This is the first merge that does compile. Not tested yet.
fix tracebility
[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
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
updating to onera version 30f766a:2016-12-04
Arrays
adding onera automata version
...
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
Merge branch 'master' into horn_enum_types
Conflicts: src/backends/Horn/horn_backend.ml
travis
major branche merging salsa/mpfr with trunk
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
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
synch with svn
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@429 041b043f-8d7c-46b2-b46e-ef0dd855326e
fixing double printing of horn rules
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@428 041b043f-8d7c-46b2-b46e-ef0dd855326e
Print the types
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@425 041b043f-8d7c-46b2-b46e-ef0dd855326e
mapping horn values to lustre values in xml format
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@423 041b043f-8d7c-46b2-b46e-ef0dd855326e
sync horn backend
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@422 041b043f-8d7c-46b2-b46e-ef0dd855326e
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@421 041b043f-8d7c-46b2-b46e-ef0dd855326e