Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn @ ae7d913d

# Date Author Comment
ae7d913d 11/16/2018 04:18 AM Pierre-Loïc Garoche

Merlin files

c35de73b 11/15/2018 03:18 AM Pierre-Loïc Garoche

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....

0d54d8a8 11/13/2018 02:01 AM Pierre-Loïc Garoche

Removed Contract contruct: imported node should be enough. Solved some warning at compile time

83dc064f 07/13/2018 08:05 PM Pierre-Loïc Garoche

Byte/String bug reappeared

f9d0c175 07/13/2018 07:52 PM Pierre-Loïc Garoche

Merge branch 'master' of https://cavale.enseeiht.fr/git/lustrec

2d2144c0 07/13/2018 05:18 PM Pierre-Loïc Garoche

Solved bug#57: issues when indirect init of a pre in horn-traces

bec3cf3d 05/31/2018 04:35 PM Xavier Thirioux

strange bug (ill-typed source) wrt Bytes/String conversion

1d0fd52b 05/18/2018 12:28 AM Xavier Thirioux

updated division for Horn clauses

fa91d4d0 05/17/2018 03:14 PM Pierre-Loïc Garoche

Euclidean div/mod treatment in Horn backend

ea8f51ae 03/30/2018 11:23 PM Pierre-Loïc Garoche

Basic library printers moved into backend specific printer files

2863281f 03/30/2018 11:14 PM Pierre-Loïc Garoche

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

089f94be 03/30/2018 10:43 PM Pierre-Loïc Garoche

MLI for normalization and machine_code.
Structs defining machines are now in machine_code_types

8446bf03 03/30/2018 05:54 PM Pierre-Loïc Garoche

- Makefile: solved dependency problem when compiling include lusi
- Renamed type declarations as lustre_types and machine_code_types

66359a5e 01/31/2018 07:27 AM Pierre-Loïc Garoche

[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

185ddf4d 01/30/2018 03:01 PM Pierre-Loïc Garoche

Type issue Bytes vs string

212d6eff 07/13/2017 06:40 PM Pierre-Loïc Garoche

[HORN] handled asserts in stateless node step rule definition

07ceae4c 07/13/2017 05:47 PM Pierre-Loïc Garoche

[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

397d5ae3 06/27/2017 06:36 PM Pierre-Loïc Garoche

Copied Printers.pp_expr functions to Horn backend to escape < and > in XML traces output

1bff14ac 06/23/2017 06:13 PM Pierre-Loïc Garoche

- 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

3ca27bc7 06/23/2017 04:07 AM Pierre-Loïc Garoche

- Addtional encapsulation of machine_code instr in a struct to enable future extension of type with more metadata.
- Improved EMF backend with META information

a6974c82 05/17/2017 12:21 PM Pierre-Loïc Garoche

[Horn] Workaround to prevent the use of declared keywords as node name

5d08c49e 05/17/2017 10:13 AM Pierre-Loïc Garoche

Solved printing bug in Horn backend

990210f3 05/16/2017 04:57 PM Pierre-Loïc Garoche

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".

2fdbc781 04/27/2017 10:42 PM Pierre-Loïc Garoche

Cleaning output:
- no more classic display for ocamlc
- compilation warnings removed

09121c1a 04/27/2017 12:19 AM Pierre-Loïc Garoche

Merge branch 'testgen' into merging_unstable_testgen

d2d9d4cb 04/26/2017 11:25 PM Pierre-Loïc Garoche

Missing files

85da3a4b 04/26/2017 11:23 PM Pierre-Loïc Garoche

Merge branch 'unstable' into merging_plugins
Non regression results were similar to master branch

a97d3e02 04/25/2017 10:57 PM Pierre-Loïc Garoche

Printing reals in Horn backend

4e809854 04/25/2017 09:41 AM Pierre-Loïc Garoche

Cosmetic changes

bde99c3f 04/06/2017 04:27 PM Xavier Thirioux

This is the first merge that does compile. Not tested yet.

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

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

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

travis

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.

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

6c4902ae 11/06/2015 06:09 PM Teme Kahsai

fixed a printing bug in horn backend

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

changes to horn

50f7d587 10/09/2015 07:23 PM Pierre-Loïc Garoche

bug:double def fr init rules

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

revereted to previous commit

7c95dcab 10/08/2015 07:11 PM Pierre-Loïc Garoche

Two fresh branches :)
to manage enum and arrays in the horn backend.

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

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

small logging change

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

9c4624e4 05/05/2015 01:17 AM Teme Kahsai

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

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

933ee7a3 03/24/2015 09:54 PM Teme Kahsai

synch with svn

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

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

fixing double printing of horn rules

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

9d01f989 03/17/2015 08:30 AM Pierre-Loïc Garoche

Print the types

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

720f159a 03/16/2015 08:31 PM Teme Kahsai

mapping horn values to lustre values in xml format

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

96d33ff2 03/16/2015 08:31 PM Teme Kahsai

sync horn backend

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

97d3f81a 03/16/2015 08:31 PM Teme Kahsai

sync horn backend

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

24a55d0d 03/16/2015 08:30 PM Teme Kahsai

fixing double printing of horn rules

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

62f65f02 03/16/2015 08:30 PM Teme Kahsai

Fixed conflict with the svn trunk version

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

e9c64a30 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

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

f133f964 03/03/2015 09:10 PM Teme Kahsai

added invariants

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

ea94d58f 03/03/2015 09:10 PM Teme Kahsai

including invariants

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

3c862628 03/03/2015 09:10 PM Teme Kahsai

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

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

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

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