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

[E-ACSL] fixed warning messages

parent 3e0535e4
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 18 additions and 12 deletions
src/plugins/e-acsl/pre_analysis.ml
+ 4
− 2
View file @ 511ab9e7
......@@ -201,8 +201,10 @@ module rec Transfer
(* Options.feedback "REGISTER %a" Cil.d_term t;*)
state_ref := register_term kf !state_ref t;
Cil.SkipChildren
| Pallocable _ | Pfreeable _ | Pfresh _ | Pseparated _ ->
Error.not_yet "\\separated"
| Pallocable _ -> Error.not_yet "\\allocable"
| Pfreeable _ -> Error.not_yet "\\freeable"
| Pfresh _ -> Error.not_yet "\\fresh"
| Pseparated _ -> Error.not_yet "\\separated"
| Ptrue | Pfalse | Papp _ | Prel _
| Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _
| Plet _ | Pforall _ | Pexists _ | Pat _ | Psubtype _ ->
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
+ 1
− 1
View file @ 511ab9e7
......@@ -5,7 +5,7 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/localvar.c"
FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
Ignoring annotation.
tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
+ 1
− 1
View file @ 511ab9e7
......@@ -5,7 +5,7 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/localvar.c"
FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
Ignoring annotation.
tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
+ 3
− 2
View file @ 511ab9e7
......@@ -5,8 +5,9 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/valid.c"
FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
Ignoring annotation.
tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+ 3
− 2
View file @ 511ab9e7
......@@ -5,8 +5,9 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/valid.c"
FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
Ignoring annotation.
tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
+ 3
− 2
View file @ 511ab9e7
......@@ -5,8 +5,9 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/valid_alias.c"
FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
+ 3
− 2
View file @ 511ab9e7
......@@ -5,8 +5,9 @@
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/valid_alias.c"
FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
......
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