Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / options.ml @ ef8a361a

History | View | Annotate | Download (1.71 KB)

# Date Author Comment
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
59fc6b1c 06/22/2017 05:24 PM Pierre-Loïc Garoche

Default precision for real values printing
f7caf067 06/22/2017 04:18 AM Pierre-Loïc Garoche

EMF backend now relies on machine code representation.
Impact:
- EMF backend has an extra machines argument
- specific option to avoid merge of ite constructs
- set_backend function to improve backend selection

Most code was extracted from seahorn_backend through c0f8
2dae76da 06/21/2017 11:03 PM Pierre-Loïc Garoche

Restored common_option definition. Was removed by a non delicate merge.
b6d37e71 06/21/2017 08:50 PM Pierre-Loïc Garoche

Bug solved: EMF backend was forced
b7258fa5 06/21/2017 08:42 PM Pierre-Loïc Garoche

Merge branch 'unstable' into seahorn_a6df3
a6df3 is the initial commit of branch seahorn
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".
375cbca2 04/27/2017 09:57 PM Pierre-Loïc Garoche

Merge branch 'unstable' into merge_mauve_unstable
09121c1a 04/27/2017 12:19 AM Pierre-Loïc Garoche

Merge branch 'testgen' into merging_unstable_testgen
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
40d33d55 04/05/2017 04:53 PM Xavier Thirioux

first version (doesn't even compile) of mutation and test generation standalone command: lustret
mostly a recovery of an ancient svn repo: mutations
d1b9423d 03/02/2017 06:12 PM David Doose

mauve generator: first shot
52c5ba00 03/01/2017 10:47 AM David Doose

adding c++ backend
a6df3992 01/31/2017 08:22 PM Pierre-Loïc Garoche

Working on EMF backend to express cocospec infos as Simulink blocks
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
1b57e111 12/30/2016 09:20 PM Teme Kahsai

adding sfunction support
fc476249 12/28/2016 01:00 AM Teme Kahsai

adding -I options to lustrec
3b2bd83d 12/08/2016 05:37 PM Teme Kahsai

updating to onera version 30f766a:2016-12-04
41e48ef3 09/01/2016 11:18 AM Eric NOULARD

Add codename to version handling. This should ease making release.
Development codename is "dev"
04a63d25 08/06/2016 10:29 AM Xavier Thirioux

full merge of salsa/mpfr and master
d97c196a 12/08/2015 03:39 PM Xavier Thirioux

Changed mpfr threshold to 2
49d92bf8 11/26/2015 11:29 PM Xavier Thirioux

regression bugs corrected
f6acf47b 11/26/2015 06:17 PM Pierre-Loïc Garoche

Plugin based framework
53206908 11/26/2015 04:45 PM Xavier Thirioux

major branche merging salsa/mpfr with trunk
d50b0dc0 10/07/2015 07:22 PM Teme Kahsai

sync
a53a28cb 08/18/2015 11:51 AM Eric Noulard

Post 1.1 release.
Back to dev version

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@473 041b043f-8d7c-46b2-b46e-ef0dd855326e
9b04601c 08/18/2015 11:51 AM Eric Noulard

Post 1.1 release.
Back to dev version
b2e2b4d8 08/13/2015 04:58 PM Eric Noulard

prepare lustrec 1.1

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@471 041b043f-8d7c-46b2-b46e-ef0dd855326e
3fb19815 08/13/2015 04:58 PM Eric Noulard

prepare lustrec 1.1
e2068500 05/05/2015 01:54 AM Teme Kahsai

first commit
2c083577 05/05/2015 01:29 AM Teme Kahsai

changed name from -horn-queries to -horn-query

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@452 041b043f-8d7c-46b2-b46e-ef0dd855326e
5fe9fe22 05/05/2015 01:29 AM Teme Kahsai

changed name from -horn-queries to -horn-query
ec433d69 04/08/2015 10:03 PM Xavier Thirioux

Major revision due to severe limitations and bugs of inlining capabilities:
- destination dir should now work properly
- lusic files now have a version number, to avoid nasty segfaults
when loading lusic files created by an older compiler version
- inlining should now work with generic nodes and generic array library...
01d48bb0 04/08/2015 10:03 PM Xavier Thirioux

Major revision due to severe limitations and bugs of inlining capabilities:
- destination dir should now work properly
- lusic files now have a version number, to avoid nasty segfaults
when loading lusic files created by an older compiler version
- inlining should now work with generic nodes and generic array library...
7df1a309 04/08/2015 03:54 PM Pierre-Loïc Garoche

horn queries back

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@441 041b043f-8d7c-46b2-b46e-ef0dd855326e
f8b3de19 04/08/2015 03:54 PM Pierre-Loïc Garoche

horn queries back
302eeebe 04/08/2015 08:53 AM Pierre-Loïc Garoche

Post Xia dev

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@439 041b043f-8d7c-46b2-b46e-ef0dd855326e
00b2c9f8 04/08/2015 08:53 AM Pierre-Loïc Garoche

Post Xia dev
2bd3b8cd 04/08/2015 08:50 AM Pierre-Loïc Garoche

Prepare for tagging : Xia version 1.0

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@437 041b043f-8d7c-46b2-b46e-ef0dd855326e
ba2f9fa1 04/08/2015 08:50 AM Pierre-Loïc Garoche

Prepare for tagging : Xia version 1.0
ea1c2906 03/06/2015 11:09 AM Pierre-Loïc Garoche

Changed the option horntraces to a general traces option
This annotation phases would have to be moved in optimization of normalized code

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@415 041b043f-8d7c-46b2-b46e-ef0dd855326e
c065827c 03/06/2015 11:09 AM Pierre-Loïc Garoche

Changed the option horntraces to a general traces option
This annotation phases would have to be moved in optimization of normalized code
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
89a70069 12/09/2014 02:03 PM Xavier Thirioux

added a new option -print_reuse that prints clock disjoint variables and reuse policy.
useful for debugging and carrying correctness proofs to the C code level.
non trivial result only when option -O 3 or above is activated.

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@383 041b043f-8d7c-46b2-b46e-ef0dd855326e
c825868a 12/09/2014 02:03 PM Xavier Thirioux

added a new option -print_reuse that prints clock disjoint variables and reuse policy.
useful for debugging and carrying correctness proofs to the C code level.
non trivial result only when option -O 3 or above is activated.
1e48ef45 12/01/2014 11:32 PM Pierre-Loïc Garoche

- Dealt with compiling lusic from distant lusi files.
- Header now do not allow the generation of function previously declared as C prototype

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@375 041b043f-8d7c-46b2-b46e-ef0dd855326e
5ae8db15 12/01/2014 11:32 PM Pierre-Loïc Garoche

- Dealt with compiling lusic from distant lusi files.
- Header now do not allow the generation of function previously declared as C prototype
9603460e 09/02/2014 05:46 PM Xavier Thirioux

- corrected bug with destination directory (-d option)
- corrected several bugs in inlining
- STILL, BUGS REMAINING in inlined code !!??!!

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@328 041b043f-8d7c-46b2-b46e-ef0dd855326e
3f823d04 09/02/2014 05:46 PM Xavier Thirioux

- corrected bug with destination directory (-d option)
- corrected several bugs in inlining
- STILL, BUGS REMAINING in inlined code !!??!!
ed81df06 07/15/2014 02:15 PM Xavier Thirioux

added some functions, prior to code refactoring

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@322 041b043f-8d7c-46b2-b46e-ef0dd855326e
7dedc5f0 07/15/2014 02:15 PM Xavier Thirioux

added some functions, prior to code refactoring
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
43aa67ec 07/09/2014 12:35 AM 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@311 041b043f-8d7c-46b2-b46e-ef0dd855326e
fcf1fd96 07/09/2014 12:35 AM Teme Kahsai

Fixed horn backend to make query for properties. More work needed for cex
af5af1e8 07/03/2014 10:46 PM Pierre-Loïc Garoche

Merged horn_traces branch

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@303 041b043f-8d7c-46b2-b46e-ef0dd855326e
36454535 07/03/2014 10:46 PM Pierre-Loïc Garoche

Merged horn_traces branch
d4107cf2 06/25/2014 05:37 PM Pierre-Loïc Garoche

Merged trunk updates

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/specification_acsl_new_backend@288 041b043f-8d7c-46b2-b46e-ef0dd855326e
e95470b3 06/25/2014 05:37 PM Pierre-Loïc Garoche

Merged trunk updates
c1adf235 06/24/2014 03:57 PM Pierre-Loïc Garoche

Restructured the main: call to optimization, scheduling performed out of machine_code, etc
Merge Xavier last commits
Unfinished lustre backend

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/simplifier@271 041b043f-8d7c-46b2-b46e-ef0dd855326e
59294251 06/24/2014 03:57 PM Pierre-Loïc Garoche

Restructured the main: call to optimization, scheduling performed out of machine_code, etc
Merge Xavier last commits
Unfinished lustre backend
592f508c 03/01/2014 12:01 AM Pierre-Loïc Garoche

Reenabled the generation of witnesses for inline process.
Systematic use of the build path

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@175 041b043f-8d7c-46b2-b46e-ef0dd855326e
2842f7ca 03/01/2014 12:01 AM Pierre-Loïc Garoche

Reenabled the generation of witnesses for inline process.
Systematic use of the build path
7291cb80 02/28/2014 04:56 PM Xavier Thirioux

- merged test script
- added -d support
- corrected #open parser problem
- corrected interface/implementation (.lusi/.lus) checking
for types (not yet for clocks)

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@171 041b043f-8d7c-46b2-b46e-ef0dd855326e
8b3afe43 02/28/2014 04:56 PM Xavier Thirioux

- merged test script
- added -d support
- corrected #open parser problem
- corrected interface/implementation (.lusi/.lus) checking
for types (not yet for clocks)
0777a7be 02/28/2014 03:28 PM Pierre-Loïc Garoche

Merge back horn backend branch in trunk

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@169 041b043f-8d7c-46b2-b46e-ef0dd855326e
29ad4531 02/28/2014 03:28 PM Pierre-Loïc Garoche

Merge back horn backend branch in trunk
c6f61bd7 02/28/2014 02:05 PM Pierre-Loïc Garoche

Merge trunk modif in branch

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@168 041b043f-8d7c-46b2-b46e-ef0dd855326e
64aa99c4 02/28/2014 02:05 PM Pierre-Loïc Garoche

Merge trunk modif in branch
e2380d4d 02/28/2014 10:33 AM Pierre-Loïc Garoche

Solved some bugs in the lustre printer
Generation of a witness with both the main node and hte inlined main node
Test script modified to check consistency of the inlining process

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/inlining@162 041b043f-8d7c-46b2-b46e-ef0dd855326e
c02d255e 02/28/2014 10:33 AM Pierre-Loïc Garoche

Solved some bugs in the lustre printer
Generation of a witness with both the main node and hte inlined main node
Test script modified to check consistency of the inlining process
3ee1012f 02/19/2014 05:02 PM Pierre-Loïc Garoche

Initial copy of the horn output version. Not really working yet

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@141 041b043f-8d7c-46b2-b46e-ef0dd855326e
f6923c9e 02/19/2014 05:02 PM Pierre-Loïc Garoche

Initial copy of the horn output version. Not really working yet
22fe1c93 10/02/2013 08:13 AM Pierre-Loïc Garoche

Moved files to trunk in lustre_compiler

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@116 041b043f-8d7c-46b2-b46e-ef0dd855326e
0cbf0839 10/02/2013 08:13 AM Pierre-Loïc Garoche

Moved files to trunk in lustre_compiler