Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn @ ca88e660

Name Size Revision Age Author Comment
horn_backend.ml 18.3 KB ca88e660 almost 5 years Pierre-Loïc Garoche Resolved conflict when merging salsa with horn_...
horn_backend_collecting_sem.ml 6.93 KB ca88e660 almost 5 years Pierre-Loïc Garoche Resolved conflict when merging salsa with horn_...
horn_backend_common.ml 4.03 KB 0dee2bc1 almost 5 years Pierre-Loïc Garoche Refactoring of the horn backend with Reset/Step...
horn_backend_printers.ml 13.7 KB ca88e660 almost 5 years Pierre-Loïc Garoche Resolved conflict when merging salsa with horn_...
horn_backend_traces.ml 6.25 KB 0dee2bc1 almost 5 years Pierre-Loïc Garoche Refactoring of the horn backend with Reset/Step...

Latest revisions

# Date Author Comment
ca88e660 01/08/2016 05:37 PM Pierre-Loïc Garoche

Resolved conflict when merging salsa with horn_encoding. The current branch is the most updated.

f0bff3e5 01/08/2016 01:41 PM Pierre-Loïc Garoche

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

a7e70823 01/07/2016 10:55 PM Pierre-Loïc Garoche

Clean old and resolved TODO

8d0c1f8e 01/07/2016 06:44 PM Pierre-Loïc Garoche

fixed a z3 bug for => within Horn clauses

cf9cc6f9 01/07/2016 04:43 PM Pierre-Loïc Garoche

Introduced the opposite of Reset call: NoReset. This simplify the general compilation process and makes the code more symmetric, hence simpler and clearer code.

2ed9b6f2 01/07/2016 04:41 PM Pierre-Loïc Garoche

solved bug: missing parenthesis in enum typedef

5df5dd85 12/16/2015 03:18 PM Pierre-Loïc Garoche

Merge branch 'master' into horn_enum_types

Conflicts:
src/backends/Horn/horn_backend.ml

53206908 11/26/2015 04:45 PM Xavier Thirioux

major branche merging salsa/mpfr with trunk

0dee2bc1 11/20/2015 06:41 PM Pierre-Loïc Garoche

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.

2580acfd 11/06/2015 06:09 PM Teme Kahsai

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

View revisions

Also available in: Atom