CristalCaveGem » LustreC

updated division for Horn clauses

Euclidean div/mod treatment in Horn 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

[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_plugins
Non 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_jan10
Intregrate 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_2
Postponed conflicts to be solved
Conflicts:
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

fixed a printing bug in horn backend

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

small logging change

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

do not use lusi for horn, and some logging for horn

synch with svn

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@429 041b043f-8d7c-46b2-b46e-ef0dd855326e

synch with svn

fixing double printing of horn rules

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@428 041b043f-8d7c-46b2-b46e-ef0dd855326e

fixing double printing of horn rules

Print the types

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@425 041b043f-8d7c-46b2-b46e-ef0dd855326e

Print the types

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

mapping horn values to lustre values in xml format

sync horn backend

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@422 041b043f-8d7c-46b2-b46e-ef0dd855326e

sync horn backend

sync horn backend

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@421 041b043f-8d7c-46b2-b46e-ef0dd855326e

sync horn backend

fixing double printing of horn rules

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@419 041b043f-8d7c-46b2-b46e-ef0dd855326e

fixing double printing of horn rules

Fixed conflict with the svn trunk version

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@417 041b043f-8d7c-46b2-b46e-ef0dd855326e

Fixed conflict with the svn trunk version

Reactivated the generation of traceability information
Changed the test-compile to use the horn-traces and the horn-queries option

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@414 041b043f-8d7c-46b2-b46e-ef0dd855326e

Reactivated the generation of traceability information
Changed the test-compile to use the horn-traces and the horn-queries option

added invariants

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@412 041b043f-8d7c-46b2-b46e-ef0dd855326e

added invariants

including invariants

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@411 041b043f-8d7c-46b2-b46e-ef0dd855326e

including invariants

Fixed horn backend to make query for properties. More work needed for cex

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@410 041b043f-8d7c-46b2-b46e-ef0dd855326e

Fixed horn backend to make query for properties. More work needed for cex

Updated the licence info and header for each file.
Moved backends in separate folders

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@313 041b043f-8d7c-46b2-b46e-ef0dd855326e

Updated the licence info and header for each file.
Moved backends in separate folders