Skip to content
Snippets Groups Projects
Commit 77b7b490 authored by Julien Signoles's avatar Julien Signoles
Browse files

remove spurious warnings about reals and fixes oracles

parent 048ce8fd
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 92 additions and 35 deletions
src/plugins/e-acsl/doc/Changelog
+ 1
− 0
View file @ 77b7b490
...@@ -15,6 +15,7 @@ ...@@ -15,6 +15,7 @@
# E-ACSL: the Whole E-ACSL plug-in # E-ACSL: the Whole E-ACSL plug-in
############################################################################### ###############################################################################
- E-ACSL [2014/03/27] Remove spurious warnings when using type `real`.
-* E-ACSL [2014/03/26] Fix bug #1692 about wrong localisation of -* E-ACSL [2014/03/26] Fix bug #1692 about wrong localisation of
some messages. some messages.
- E-ACSL [2014/03/26] Remove a spurious warning when an annotated - E-ACSL [2014/03/26] Remove a spurious warning when an annotated
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
+ 3
− 2
View file @ 77b7b490
...@@ -6,8 +6,9 @@ ...@@ -6,8 +6,9 @@
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h" [kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
[e-acsl] beginning translation. [e-acsl] beginning translation.
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating type `real' by `long double' tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating a real number by a float tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
+ 3
− 2
View file @ 77b7b490
...@@ -6,8 +6,9 @@ ...@@ -6,8 +6,9 @@
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h" [kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
[e-acsl] beginning translation. [e-acsl] beginning translation.
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating type `real' by `long double' tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating a real number by a float tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
+ 13
− 3
View file @ 77b7b490
...@@ -15,10 +15,20 @@ tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `disjoint b ...@@ -15,10 +15,20 @@ tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `disjoint b
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:124:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:124:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
+ 4
− 2
View file @ 77b7b490
...@@ -17,8 +17,10 @@ tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns cl ...@@ -17,8 +17,10 @@ tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns cl
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
+ 5
− 1
View file @ 77b7b490
...@@ -13,7 +13,11 @@ tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `disjoint beha ...@@ -13,7 +13,11 @@ tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `disjoint beha
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:124:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:124:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
+ 5
− 1
View file @ 77b7b490
...@@ -13,7 +13,11 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `disjoint ...@@ -13,7 +13,11 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `disjoint
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:124:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:124:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
+ 5
− 1
View file @ 77b7b490
...@@ -13,7 +13,11 @@ tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `disjoint ...@@ -13,7 +13,11 @@ tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `disjoint
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:124:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:124:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
+ 13
− 3
View file @ 77b7b490
...@@ -15,10 +15,20 @@ tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `disjoint beh ...@@ -15,10 +15,20 @@ tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `disjoint beh
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:124:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:124:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+ 4
− 2
View file @ 77b7b490
...@@ -17,8 +17,10 @@ tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `assigns clau ...@@ -17,8 +17,10 @@ tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `assigns clau
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
+ 13
− 3
View file @ 77b7b490
...@@ -15,10 +15,20 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `disjoi ...@@ -15,10 +15,20 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `disjoi
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:124:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:124:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
+ 4
− 2
View file @ 77b7b490
...@@ -17,8 +17,10 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `assign ...@@ -17,8 +17,10 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `assign
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
+ 13
− 3
View file @ 77b7b490
...@@ -15,10 +15,20 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `disjoint be ...@@ -15,10 +15,20 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `disjoint be
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:124:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:124:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:129:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
+ 4
− 2
View file @ 77b7b490
...@@ -17,8 +17,10 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `assigns cla ...@@ -17,8 +17,10 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `assigns cla
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:141:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
src/plugins/e-acsl/typing.ml
+ 2
− 8
View file @ 77b7b490
...@@ -76,10 +76,7 @@ let typ_of_eacsl_typ = function ...@@ -76,10 +76,7 @@ let typ_of_eacsl_typ = function
| No_integral (Ltype _) -> Error.not_yet "typing of user-defined logic type" | No_integral (Ltype _) -> Error.not_yet "typing of user-defined logic type"
| No_integral (Lvar _) -> Error.not_yet "type variable" | No_integral (Lvar _) -> Error.not_yet "type variable"
| No_integral Linteger -> Mpz.t () | No_integral Linteger -> Mpz.t ()
| No_integral Lreal -> | No_integral Lreal -> TFloat(FLongDouble, [])
Options.warning ~current:true ~once:true
"approximating type `real' by `long double'";
TFloat(FLongDouble, [])
| No_integral (Larrow _) -> Error.not_yet "functional type" | No_integral (Larrow _) -> Error.not_yet "functional type"
let eacsl_typ_of_typ ty = let eacsl_typ_of_typ ty =
...@@ -173,10 +170,7 @@ let generic_typ (which: < f: 'a. 'a * 'a -> 'a >) t = ...@@ -173,10 +170,7 @@ let generic_typ (which: < f: 'a. 'a * 'a -> 'a >) t =
| Ltype _ as ty when Logic_const.is_boolean_type ty -> Mpz.t () | Ltype _ as ty when Logic_const.is_boolean_type ty -> Mpz.t ()
| Ltype _ -> Error.not_yet "typing of user-defined logic type" | Ltype _ -> Error.not_yet "typing of user-defined logic type"
| Lvar _ -> Error.not_yet "type variable" | Lvar _ -> Error.not_yet "type variable"
| Lreal -> | Lreal -> TFloat(FLongDouble, [])
Options.warning ~current:true ~once:true
"approximating type `real' by `long double'";
TFloat(FLongDouble, [])
| Larrow _ -> Error.not_yet "functional type" | Larrow _ -> Error.not_yet "functional type"
in in
which#f (ty, ty) which#f (ty, ty)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment