CristalCaveGem » LustreC

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

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.

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