Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

# Date Author Comment
92ff8f1b 02/01/2017 12:21 AM Teme Kahsai

fix tracebility

d7e04983 01/13/2017 01:17 PM Pierre-Loïc Garoche

[Horn] Updated traceability of Horn backend to deal with fby (arrow machines)

042dc586 01/11/2017 10:02 AM Pierre-Loïc Garoche

Revert some ocaml code to ocaml 4.01 compatibility

dcafc99b 01/11/2017 12:28 AM Pierre-Loïc Garoche

Merge branch 'github_master' into integ_github_jan10
Intregrate all modifs by Teme et al

d128bbd4 01/06/2017 08:04 PM Teme Kahsai

fixed sfunction detetction

9f77bff7 01/06/2017 08:11 AM Teme Kahsai

adding math.smt2

44ce4da8 01/04/2017 12:30 AM Pierre-Loïc Garoche

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.

e057dd08 12/30/2016 10:47 PM Teme Kahsai

adjusting travis

7ad4ff7c 12/30/2016 09:29 PM Teme Kahsai

Merge branch 'master' into master

1b57e111 12/30/2016 09:20 PM Teme Kahsai

adding sfunction support

2dd3d358 12/29/2016 07:18 AM Teme Kahsai

making library statically link to horn backend

822f31e1 12/08/2016 05:55 PM Teme Kahsai

updating to onera version 30f766a:2016-12-04

84902260 10/12/2016 11:44 PM jbraine

Arrays

85a6f473 09/30/2016 06:41 PM Teme Kahsai

adding onera automata version

f3d244c1 08/09/2016 10:01 PM Xavier Thirioux

...

45f0f48d 08/09/2016 09:31 PM Xavier Thirioux

...

fea041c5 08/09/2016 09:25 PM Xavier Thirioux

new branch for merging mpfr and horn

04a63d25 08/06/2016 10:29 AM Xavier Thirioux

full merge of salsa/mpfr and master

3cdd2147 06/02/2016 01:45 AM Teme Kahsai

fixed assert compilation in case of stateless program

bad9b6b2 02/23/2016 10:49 PM Teme Kahsai

Updated to onera_git commit version 9421e24

7ec8e203 12/09/2015 12:40 AM Teme Kahsai

travis

89bc26df 11/16/2015 05:23 PM Teme Kahsai

remove duplication

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

4347ae0c 10/13/2015 10:29 PM Teme Kahsai

changes to horn

9cb34634 10/09/2015 07:19 PM Teme Kahsai

revereted to previous commit

e41592cf 05/05/2015 09:38 PM Teme Kahsai

Bug fixed (454), more on travis

cdf01754 05/05/2015 07:30 PM Teme Kahsai

small logging change

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

e2068500 05/05/2015 01:54 AM Teme Kahsai

first commit

8deaa2dd 05/05/2015 01:17 AM Teme Kahsai

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

c89faaa4 03/24/2015 09:54 PM Teme Kahsai

synch with svn

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

3a87efb8 03/24/2015 09:54 PM Teme Kahsai

fixing double printing of horn rules

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

228ebb2c 03/17/2015 08:30 AM Pierre-Loïc Garoche

Print the types

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

922ed789 03/16/2015 08:31 PM Teme Kahsai

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

b701409d 03/16/2015 08:31 PM Teme Kahsai

sync horn backend

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

193a5ca6 03/16/2015 08:31 PM Teme Kahsai

sync horn backend

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

99d9ac94 03/16/2015 08:30 PM Teme Kahsai

fixing double printing of horn rules

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

c7c6ef4c 03/16/2015 08:30 PM Teme Kahsai

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

3ca6d126 03/05/2015 11:48 PM Pierre-Loïc Garoche

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

7d9df109 03/03/2015 09:10 PM Teme Kahsai

added invariants

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

8d4fddd8 03/03/2015 09:10 PM Teme Kahsai

including invariants

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

5cf953ec 03/03/2015 09:10 PM Teme Kahsai

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

a2d97a3e 07/09/2014 09:57 AM Pierre-Loïc Garoche

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