Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / options.ml @ 5fccce23

History | View | Annotate | Download (1.93 KB)

# Date Author Comment
3cd040e3 05/17/2018 02:42 PM Pierre-Loïc Garoche

Issues with typing pp_basic_lib_fun

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

Basic library printers moved into backend specific printer files

8b87d0a5 12/14/2017 08:57 PM Pierre-Loïc Garoche

Forcing mpfr status when -real mpfr asked. Default precision is 100 bits.

74ca6b61 09/22/2017 05:38 PM Pierre-Loïc Garoche

A fresh option to print with declared types instead of inferred ones

264a4844 07/20/2017 10:20 PM Pierre-Loïc Garoche

First working version of algebraic loop resolution. Disabled by default.

e7cc5186 07/18/2017 12:03 AM Pierre-Loïc Garoche

Refactor error printing.

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