From 22d1eb761c17ca8757d8bde755c55b85454790a9 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 5 Dec 2012 16:41:30 +0000
Subject: [PATCH] [E-ACSL] clause 'assumes' now checked during pre_analysis
[E-ACSL] fixed bug in Pre_analysis with pointer arithmetics in logic [E-ACSL]
does not check some possible cases during pre analysis Thx to two first
items, fully fixed bug #1324
---
src/plugins/e-acsl/TODO | 1 +
src/plugins/e-acsl/pre_analysis.ml | 125 ++++----
src/plugins/e-acsl/pre_analysis.mli | 2 +-
.../e-acsl/tests/e-acsl-runtime/bts1324.i | 27 ++
.../oracle/bts1324.1.err.oracle | 0
.../oracle/bts1324.1.res.oracle | 81 +++++
.../e-acsl-runtime/oracle/bts1324.err.oracle | 0
.../e-acsl-runtime/oracle/bts1324.res.oracle | 90 ++++++
.../tests/e-acsl-runtime/oracle/gen_bts1324.c | 168 ++++++++++
.../e-acsl-runtime/oracle/gen_bts13242.c | 293 ++++++++++++++++++
.../oracle/gen_valid_in_contract.c | 16 +
.../oracle/gen_valid_in_contract2.c | 16 +
.../oracle/valid_in_contract.1.res.oracle | 3 +
.../oracle/valid_in_contract.res.oracle | 3 +
14 files changed, 766 insertions(+), 59 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/bts1324.i
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index eab34b88127..709190c30d4 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -17,6 +17,7 @@
- variable GMP potentiellement initialisé mais non utilisé en présence de \at
(voir test result.i, cas -e-acsl-gmp-only)
- générer les delete des globals dans une fonction séparée, comme pour les init.
+- do not analyse library function in pre-analysis
##############
# KNOWN BUGS #
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 58e1b4a21c4..1636d2d2966 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -112,7 +112,9 @@ module rec Transfer
module StmtStartData = Env.StartData
- let pretty _fmt _state = assert false
+ let pretty fmt state = match state with
+ | None -> Format.fprintf fmt "None"
+ | Some s -> Format.fprintf fmt "%a" Varinfo.Set.pretty s
(** The data at function exit. Used for statements with no successors.
This is usually bottom, since we'll also use doStmt on Return
@@ -123,10 +125,11 @@ module rec Transfer
the one we have just computed. Return None if the combination is the same
as the old data, otherwise return the combination. In the latter case, the
predecessors of the statement are put on the working list. *)
- let combineStmtStartData _stmt ~old state = match old, state with
- | _, None -> assert false
- | None, Some _ -> Some state (* [old] already included in [state] *)
- | Some old, Some new_ ->
+ let combineStmtStartData stmt ~old state = match stmt.skind, old, state with
+ | _, _, None -> assert false
+ | _, None, Some _ -> Some state (* [old] already included in [state] *)
+ | Return _, Some old, Some new_ -> Some (Some (Varinfo.Set.union old new_))
+ | _, Some old, Some new_ ->
if Varinfo.Set.equal old new_ then
None
else
@@ -137,7 +140,7 @@ module rec Transfer
Some (Varinfo.Set.union (Env.default_varinfos s1) (Env.default_varinfos s2))
let rec register_term_lval kf varinfos (thost, _) = match thost with
- | TVar { lv_origin = None } -> Error.not_yet "logic variable"
+ | TVar { lv_origin = None } -> varinfos
| TVar { lv_origin = Some vi } ->
Varinfo.Set.add vi varinfos
| TResult _ -> Varinfo.Set.add (Misc.result_vi kf) varinfos
@@ -154,7 +157,7 @@ module rec Transfer
| TBinOp(_, t1, t2) | Tif(_, t1, t2) ->
let s = register_term kf varinfos t1 in
register_term kf s t2
- | Tapp(_, _, l) -> List.fold_left (register_term kf) varinfos l
+ | Tapp(_, _, _) -> Error.not_yet "function application"
| TDataCons _ -> Error.not_yet "data constructor"
| Tbase_addr _ -> Error.not_yet "\\base_addr"
| Toffset _ -> Error.not_yet "\\offset"
@@ -170,12 +173,62 @@ module rec Transfer
| Tcomprehension _ -> Error.not_yet "set comprehension"
| Trange _ -> Error.not_yet "\\range"
+ let register_object kf state_ref = object
+ inherit Visitor.frama_c_inplace
+ method vpredicate = function
+ | Pvalid(_, t) | Pvalid_read(_, t) | Pinitialized(_, t)
+ | Pallocable(_, t) | Pfreeable(_, t) | Pfresh(_, _, t, _) ->
+ (* Options.feedback "REGISTER %a" Cil.d_term t;*)
+ state_ref := register_term kf !state_ref t;
+ Cil.SkipChildren
+ | Pseparated _ -> Error.not_yet "\\separated"
+ | Ptrue | Pfalse | Papp _ | Prel _
+ | Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _
+ | Plet _ | Pforall _ | Pexists _ | Pat _ | Psubtype _ ->
+ Cil.DoChildren
+ method vterm term = match term.term_node with
+ | Tbase_addr(_, t) | Toffset(_, t) | Tblock_length(_, t)
+ | TBinOp((PlusPI | IndexPI | MinusPI), t, _) ->
+ state_ref := register_term kf !state_ref t;
+ Cil.SkipChildren
+ | TBinOp(MinusPP, t1, t2) ->
+ let state = register_term kf !state_ref t1 in
+ state_ref := register_term kf state t2;
+ Cil.SkipChildren
+ | TConst _ | TSizeOf _ | TSizeOfStr _ | TAlignOf _ | Tnull
+ | Ttype _ | Tempty_set | TSizeOfE _ | TUnOp _ | TBinOp _ | Ttypeof _ ->
+ (* no left-value inside inside: skip for efficiency *)
+ Cil.SkipChildren
+ | TLval _ | TAlignOfE _ | TCastE _ | TAddrOf _
+ | TStartOf _ | Tapp _ | Tlambda _ | TDataCons _ | Tif _ | Tat _
+ | TCoerce _ | TCoerceE _ | TUpdate _ | Tunion _ | Tinter _
+ | Tcomprehension _ | Trange _ | Tlet _ | TLogic_coerce _ ->
+ (* potential sub-term inside *)
+ Cil.DoChildren
+ method vlogic_label _ = Cil.SkipChildren
+ method vterm_lhost = function
+ | TMem t ->
+ state_ref := register_term kf !state_ref t;
+ Cil.SkipChildren
+ | TVar _ | TResult _ ->
+ Cil.SkipChildren
+ end
+
+ let register_predicate kf pred state =
+ let state_ref = ref state in
+ ignore (Visitor.visitFramacIdPredicate (register_object kf state_ref) pred);
+ !state_ref
+
+ let register_code_annot kf a state =
+ let state_ref = ref state in
+ ignore (Visitor.visitFramacCodeAnnotation (register_object kf state_ref) a);
+ !state_ref
+
(** The (backwards) transfer function for a branch. The [(Cil.CurrentLoc.get
())] is set before calling this. If it returns None, then we have some
default handling. Otherwise, the returned data is the data before the
branch (not considering the exception handlers) *)
let doStmt stmt =
-(* Options.feedback "ANALYSING %a" Cil.d_stmt stmt;*)
let _, kf = Kernel_function.find_from_sid stmt.sid in
let is_first =
try Stmt.equal stmt (Kernel_function.find_first_stmt kf)
@@ -185,52 +238,6 @@ module rec Transfer
try Stmt.equal stmt (Kernel_function.find_return kf)
with Kernel_function.No_Statement -> assert false
in
- let register state_ref = object
- inherit Visitor.frama_c_inplace
- method vpredicate = function
- | Pvalid(_, t) | Pvalid_read(_, t) | Pinitialized(_, t)
- | Pallocable(_, t) | Pfreeable(_, t) | Pfresh(_, _, t, _) ->
-(* Options.feedback "REGISTER %a" Cil.d_term t;*)
- state_ref := register_term kf !state_ref t;
- Cil.SkipChildren
- | Pseparated _ -> Error.not_yet "\\separated"
- | Ptrue | Pfalse | Papp _ | Prel _
- | Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _
- | Plet _ | Pforall _ | Pexists _ | Pat _ | Psubtype _ ->
- Cil.DoChildren
- method vterm term = match term.term_node with
- | Tbase_addr(_, t) | Toffset(_, t) | Tblock_length(_, t) ->
- state_ref := register_term kf !state_ref t;
- Cil.SkipChildren
- | TConst _ | TSizeOf _ | TSizeOfStr _ | TAlignOf _ | Tnull
- | Ttype _ | Tempty_set ->
- (* no sub-term inside: skip for efficiency *)
- Cil.SkipChildren
- | TLval _ | TSizeOfE _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TCastE _
- | TAddrOf _
- | TStartOf _ | Tapp _ | Tlambda _ | TDataCons _ | Tif _ | Tat _
- | TCoerce _ | TCoerceE _ | TUpdate _ | Ttypeof _ | Tunion _ | Tinter _
- | Tcomprehension _ | Trange _ | Tlet _ | TLogic_coerce _ ->
- (* potential sub-term inside *)
- Cil.DoChildren
- method vlogic_label _ = Cil.SkipChildren
- method vterm_lhost = function
- | TMem t ->
- state_ref := register_term kf !state_ref t;
- Cil.SkipChildren
- | TVar _ | TResult _ ->
- Cil.SkipChildren
- end in
- let register_predicate pred state =
- let state_ref = ref state in
- ignore (Visitor.visitFramacIdPredicate (register state_ref) pred);
- !state_ref
- in
- let register_code_annot a state =
- let state_ref = ref state in
- ignore (Visitor.visitFramacCodeAnnotation (register state_ref) a);
- !state_ref
- in
Dataflow.Post
(fun state ->
let state = Env.default_varinfos state in
@@ -240,11 +247,12 @@ module rec Transfer
(fun _ bhv s ->
let handle_annot test f s =
if test then
- f (fun _ p s -> register_predicate p s) kf bhv.b_name s
+ f (fun _ p s -> register_predicate kf p s) kf bhv.b_name s
else
s
in
let s = handle_annot is_first Annotations.fold_requires s in
+ let s = handle_annot is_first Annotations.fold_assumes s in
handle_annot
is_last
(fun f -> Annotations.fold_ensures (fun e (_, p) -> f e p)) s)
@@ -254,7 +262,8 @@ module rec Transfer
state
in
let state =
- Annotations.fold_code_annot (fun _ -> register_code_annot) stmt state
+ Annotations.fold_code_annot
+ (fun _ -> register_code_annot kf) stmt state
in
Some state)
@@ -484,8 +493,8 @@ let must_model_vi ?kf ?stmt vi =
let must_model_lval ?kf ?stmt lv =
Error.generic_handle (must_model_lval ?kf ?stmt) false lv
-let old_must_model_vi bhv ?kf vi =
- must_model_vi ?kf (Cil.get_original_varinfo bhv vi)
+let old_must_model_vi bhv ?kf ?stmt vi =
+ must_model_vi ?kf ?stmt (Cil.get_original_varinfo bhv vi)
(*
Local Variables:
diff --git a/src/plugins/e-acsl/pre_analysis.mli b/src/plugins/e-acsl/pre_analysis.mli
index f8e614d8c84..bdd2d6b1cb1 100644
--- a/src/plugins/e-acsl/pre_analysis.mli
+++ b/src/plugins/e-acsl/pre_analysis.mli
@@ -29,7 +29,7 @@ val must_model_vi: ?kf:kernel_function -> ?stmt:stmt -> varinfo -> bool
val must_model_lval: ?kf:kernel_function -> ?stmt:stmt -> lval -> bool
val old_must_model_vi:
- Cil.visitor_behavior -> ?kf:kernel_function -> varinfo -> bool
+ Cil.visitor_behavior -> ?kf:kernel_function -> ?stmt:stmt -> varinfo -> bool
(*
Local Variables:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1324.i b/src/plugins/e-acsl/tests/e-acsl-runtime/bts1324.i
new file mode 100644
index 00000000000..05456f90c43
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/bts1324.i
@@ -0,0 +1,27 @@
+/* run.config
+ COMMENT: fixed bug with typing of universal quantification
+ EXECNOW: LOG gen_bts1324.c BIN gen_bts1324.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1324.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1324.c > /dev/null && ./gcc_test.sh bts1324
+ EXECNOW: LOG gen_bts13242.c BIN gen_bts13242.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1324.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts13242.c > /dev/null && ./gcc_test.sh bts13242
+*/
+
+/*@ behavior yes:
+ @ assumes \forall int i; 0 < i < n ==> t[i-1] <= t[i];
+ @ ensures \result == 1;
+ @*/
+int sorted(int * t, int n) {
+ int b = 1;
+ if(n <= 1)
+ return 1;
+ for(b = 1; b < n; b++) {
+ if(t[b-1] > t[b])
+ return 0;
+ }
+ return 1;
+}
+
+int main(void) {
+ int t[7] = { 1, 4, 4, 5, 5, 5, 7 };
+ int n = sorted(t, 7);
+ /*@ assert n == 1; */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
new file mode 100644
index 00000000000..a47699ae928
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
@@ -0,0 +1,81 @@
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+tests/e-acsl-runtime/bts1324.i:8:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
+tests/e-acsl-runtime/bts1324.i:8:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {2147483647}
+ __fc_heap_status ∈ [--..--]
+ __fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
+ S___fc_stdout[0].__fc_stdio_fpos ∈ [--..--]
+ [0].__fc_stdio_buffer ∈
+ {{ NULL ; &S___fc_stdio_buffer_0_S___fc_stdout }}
+ [0]{.__fc_stdio_error; .__fc_stdio_eof; } ∈ [--..--]
+ [0].[bits 80 to 95] ∈ UNINITIALIZED
+ {[0].__fc_stdio_id; [1].__fc_stdio_fpos; } ∈ [--..--]
+ [1].__fc_stdio_buffer ∈
+ {{ NULL ; &S___fc_stdio_buffer_1_S___fc_stdout }}
+ [1]{.__fc_stdio_error; .__fc_stdio_eof; } ∈ [--..--]
+ [1].[bits 80 to 95] ∈ UNINITIALIZED
+ [1].__fc_stdio_id ∈ [--..--]
+ S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
+[value] using specification for function __store_block
+[value] using specification for function __initialize
+[value] using specification for function __full_init
+[value] using specification for function __gmpz_init
+./share/e-acsl/e_acsl_gmp.h:36:[value] Function __gmpz_init: precondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:37:[value] Function __gmpz_init: postcondition got status valid.
+[value] using specification for function __gmpz_init_set_si
+./share/e-acsl/e_acsl_gmp.h:61:[value] Function __gmpz_init_set_si: precondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:63:[value] Function __gmpz_init_set_si: postcondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: postcondition got status unknown.
+[value] using specification for function __gmpz_add
+./share/e-acsl/e_acsl_gmp.h:131:[value] Function __gmpz_add: precondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:132:[value] Function __gmpz_add: precondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:133:[value] Function __gmpz_add: precondition got status valid.
+[value] using specification for function __gmpz_set
+./share/e-acsl/e_acsl_gmp.h:82:[value] Function __gmpz_set: precondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:83:[value] Function __gmpz_set: precondition got status valid.
+[value] using specification for function __gmpz_clear
+./share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
+:0:[value] entering loop for the first time
+[value] using specification for function __gmpz_cmp
+./share/e-acsl/e_acsl_gmp.h:115:[value] Function __gmpz_cmp: precondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:116:[value] Function __gmpz_cmp: precondition got status valid.
+[value] using specification for function __gmpz_sub
+./share/e-acsl/e_acsl_gmp.h:138:[value] Function __gmpz_sub: precondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:139:[value] Function __gmpz_sub: precondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:140:[value] Function __gmpz_sub: precondition got status valid.
+[value] using specification for function __gmpz_get_ui
+./share/e-acsl/e_acsl_gmp.h:185:[value] Function __gmpz_get_ui: precondition got status valid.
+tests/e-acsl-runtime/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_2);
+tests/e-acsl-runtime/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_i_2);
+tests/e-acsl-runtime/bts1324.i:15:[value] entering loop for the first time
+./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function __delete_block
+tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid.
+tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid, but it is unknown if the behavior is active.
+tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
+[value] using specification for function __clean
+[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values at end of function e_acsl_assert:
+[value] Values at end of function sorted:
+ b ∈ [7..15]
+ __retres ∈ {1}
+[value] Values at end of function main:
+ t[0] ∈ {1}
+ [1..2] ∈ {4}
+ [3..5] ∈ {5}
+ [6] ∈ {7}
+ n ∈ {1}
+ __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
new file mode 100644
index 00000000000..5a4cb632cc2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
@@ -0,0 +1,90 @@
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl -IFRAMAC_SHARE/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {2147483647}
+ __fc_heap_status ∈ [--..--]
+ __fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
+ S___fc_stdout[0].__fc_stdio_fpos ∈ [--..--]
+ [0].__fc_stdio_buffer ∈
+ {{ NULL ; &S___fc_stdio_buffer_0_S___fc_stdout }}
+ [0]{.__fc_stdio_error; .__fc_stdio_eof; } ∈ [--..--]
+ [0].[bits 80 to 95] ∈ UNINITIALIZED
+ {[0].__fc_stdio_id; [1].__fc_stdio_fpos; } ∈ [--..--]
+ [1].__fc_stdio_buffer ∈
+ {{ NULL ; &S___fc_stdio_buffer_1_S___fc_stdout }}
+ [1]{.__fc_stdio_error; .__fc_stdio_eof; } ∈ [--..--]
+ [1].[bits 80 to 95] ∈ UNINITIALIZED
+ [1].__fc_stdio_id ∈ [--..--]
+ S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
+ S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
+[value] using specification for function __store_block
+[value] using specification for function __initialize
+[value] using specification for function __full_init
+:0:[value] entering loop for the first time
+[value] using specification for function __valid_read
+./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function printf
+[value] using specification for function exit
+FRAMAC_SHARE/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
+tests/e-acsl-runtime/bts1324.i:15:[value] entering loop for the first time
+./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __delete_block
+tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid.
+tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid, but it is unknown if the behavior is active.
+tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
+[value] using specification for function __clean
+[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values at end of function e_acsl_assert:
+ S___fc_stdout[0].__fc_stdio_fpos ∈ [--..--]
+ [0].__fc_stdio_buffer ∈
+ {{ NULL ; &S___fc_stdio_buffer_0_S___fc_stdout }}
+ [0]{.__fc_stdio_error; .__fc_stdio_eof; } ∈ [--..--]
+ [0].[bits 80 to 95] ∈ UNINITIALIZED
+ {[0].__fc_stdio_id; [1].__fc_stdio_fpos; } ∈ [--..--]
+ [1].__fc_stdio_buffer ∈
+ {{ NULL ; &S___fc_stdio_buffer_1_S___fc_stdout }}
+ [1]{.__fc_stdio_error; .__fc_stdio_eof; } ∈ [--..--]
+ [1].[bits 80 to 95] ∈ UNINITIALIZED
+ [1].__fc_stdio_id ∈ [--..--]
+[value] Values at end of function sorted:
+ b ∈ [7..15]
+ __retres ∈ {1}
+ S___fc_stdout[0].__fc_stdio_fpos ∈ [--..--]
+ [0].__fc_stdio_buffer ∈
+ {{ NULL ; &S___fc_stdio_buffer_0_S___fc_stdout }}
+ [0]{.__fc_stdio_error; .__fc_stdio_eof; } ∈ [--..--]
+ [0].[bits 80 to 95] ∈ UNINITIALIZED
+ {[0].__fc_stdio_id; [1].__fc_stdio_fpos; } ∈ [--..--]
+ [1].__fc_stdio_buffer ∈
+ {{ NULL ; &S___fc_stdio_buffer_1_S___fc_stdout }}
+ [1]{.__fc_stdio_error; .__fc_stdio_eof; } ∈ [--..--]
+ [1].[bits 80 to 95] ∈ UNINITIALIZED
+ [1].__fc_stdio_id ∈ [--..--]
+[value] Values at end of function main:
+ t[0] ∈ {1}
+ [1..2] ∈ {4}
+ [3..5] ∈ {5}
+ [6] ∈ {7}
+ n ∈ {1}
+ __retres ∈ {0}
+ S___fc_stdout[0].__fc_stdio_fpos ∈ [--..--]
+ [0].__fc_stdio_buffer ∈
+ {{ NULL ; &S___fc_stdio_buffer_0_S___fc_stdout }}
+ [0]{.__fc_stdio_error; .__fc_stdio_eof; } ∈ [--..--]
+ [0].[bits 80 to 95] ∈ UNINITIALIZED
+ {[0].__fc_stdio_id; [1].__fc_stdio_fpos; } ∈ [--..--]
+ [1].__fc_stdio_buffer ∈
+ {{ NULL ; &S___fc_stdio_buffer_1_S___fc_stdout }}
+ [1]{.__fc_stdio_error; .__fc_stdio_eof; } ∈ [--..--]
+ [1].[bits 80 to 95] ∈ UNINITIALIZED
+ [1].__fc_stdio_id ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
new file mode 100644
index 00000000000..9eb0a8dd321
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
@@ -0,0 +1,168 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+struct __fc_pos_t {
+ unsigned long __fc_stdio_position ;
+};
+typedef struct __fc_pos_t fpos_t;
+struct __fc_FILE {
+ fpos_t __fc_stdio_fpos ;
+ char *__fc_stdio_buffer ;
+ char __fc_stdio_error ;
+ char __fc_stdio_eof ;
+ long __fc_stdio_id ;
+};
+typedef struct __fc_FILE FILE;
+/*@
+model __mpz_struct { ℤ n };
+*/
+int __fc_random_counter __attribute__((__unused__));
+unsigned long const __fc_rand_max = (unsigned long)2147483647;
+extern int __fc_heap_status;
+/*@
+axiomatic
+ dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ ensures \false;
+ assigns \nothing; */
+extern void exit(int status);
+extern FILE *__fc_stdout;
+/*@ assigns *__fc_stdout;
+ assigns *__fc_stdout \from *(format+(..)); */
+extern int printf(char const *format , ...);
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
+{
+ if (! predicate) {
+ printf("%s failed at line %d.\nThe failing predicate is:\n%s.\n",kind,
+ line,pred_txt);
+ exit(1);
+ }
+ return;
+}
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
+ size_t size);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
+ size_t size);
+extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+/*@ behavior yes:
+ assumes ∀ long long i; 0 < i ∧ i < n ⇒ *(t+(i-1)) ≤ *(t+i);
+ ensures \result ≡ 1;
+
+
+*/
+int sorted(int *t, int n)
+{
+ int __e_acsl_at;
+ int __retres;
+ int b;
+ __store_block((void *)(& t),4U);
+ __full_init((void *)(& t));
+ {
+ int __e_acsl_forall;
+ long long __e_acsl_i;
+ __e_acsl_forall = 1;
+ __e_acsl_i = (long long)(0 + 1);
+ while (1) {
+ if (__e_acsl_i < n) { ; }
+ else { break; }
+ {
+ int __e_acsl_valid_read;
+ int __e_acsl_valid_read_2;
+ __e_acsl_valid_read = __valid_read((void *)(t + __e_acsl_i),
+ sizeof(int));
+ e_acsl_assert(__e_acsl_valid_read,(char *)"Postcondition",
+ (char *)"mem_access: \\valid_read(t+__e_acsl_i)",0);
+ __e_acsl_valid_read_2 = __valid_read((void *)(t + (__e_acsl_i - (long long)1)),
+ sizeof(int));
+ e_acsl_assert(__e_acsl_valid_read_2,(char *)"Postcondition",
+ (char *)"mem_access: \\valid_read(t+(long long)(__e_acsl_i-(long long)1))",
+ 0);
+ if (*(t + (__e_acsl_i - (long long)1)) <= *(t + __e_acsl_i)) { ; }
+ else {
+ __e_acsl_forall = 0;
+ goto e_acsl_end_loop1; }
+ }
+
+ __e_acsl_i ++;
+ }
+ e_acsl_end_loop1: /* internal */ ;
+ __e_acsl_at = __e_acsl_forall;
+ }
+
+ b = 1;
+ if (n <= 1) {
+ __retres = 1;
+ goto return_label; }
+ b = 1;
+ while (b < n) {
+ if (*(t + (b - 1)) > *(t + b)) {
+ __retres = 0;
+ goto return_label; }
+ b ++;
+ }
+ __retres = 1;
+ return_label: /* internal */
+ { int __e_acsl_implies;
+ if (! __e_acsl_at) { __e_acsl_implies = 1; }
+ else { __e_acsl_implies = __retres == 1; }
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
+ (char *)"\\old(\\forall long long i; 0 < i && i < n ==> *(t+(i-1)) <= *(t+i)) ==>\n\\result == 1",
+ 9);
+ __delete_block((void *)(& t));
+ return (__retres);
+ }
+
+}
+
+int main(void)
+{
+ int __retres;
+ int t[7];
+ int n;
+ __store_block((void *)(t),28U);
+ __initialize((void *)(t),sizeof(int));
+ t[0] = 1;
+ __initialize((void *)(& t[1]),sizeof(int));
+ t[1] = 4;
+ __initialize((void *)(& t[2]),sizeof(int));
+ t[2] = 4;
+ __initialize((void *)(& t[3]),sizeof(int));
+ t[3] = 5;
+ __initialize((void *)(& t[4]),sizeof(int));
+ t[4] = 5;
+ __initialize((void *)(& t[5]),sizeof(int));
+ t[5] = 5;
+ __initialize((void *)(& t[6]),sizeof(int));
+ t[6] = 7;
+ n = sorted(t,7);
+ /*@ assert n ≡ 1; */
+ e_acsl_assert(n == 1,(char *)"Assertion",(char *)"n == 1",25);
+ __retres = 0;
+ __delete_block((void *)(t));
+ __clean();
+ return (__retres);
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
new file mode 100644
index 00000000000..1c9055649ca
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
@@ -0,0 +1,293 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+struct __fc_pos_t {
+ unsigned long __fc_stdio_position ;
+};
+typedef struct __fc_pos_t fpos_t;
+struct __fc_FILE {
+ fpos_t __fc_stdio_fpos ;
+ char *__fc_stdio_buffer ;
+ char __fc_stdio_error ;
+ char __fc_stdio_eof ;
+ long __fc_stdio_id ;
+};
+typedef struct __fc_FILE FILE;
+/*@
+model __mpz_struct { ℤ n };
+*/
+/*@ requires ¬\initialized(z);
+ ensures \valid(\old(z));
+ allocates \old(z);
+
+ assigns *z;
+
+*/
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
+/*@ requires ¬\initialized(z);
+ ensures \valid(\old(z));
+
+ ensures \initialized(\old(z));
+ allocates \old(z);
+
+ assigns *z;
+ assigns *z \from n;
+
+*/
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
+ long n);
+/*@ requires \valid(z_orig);
+ requires \valid(z);
+ assigns *z;
+ assigns *z \from *z_orig;
+
+*/
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_set(__mpz_struct * /*[1]*/ z,
+ __mpz_struct const * /*[1]*/ z_orig);
+/*@ requires \valid(x);
+ assigns *x; */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+ assigns *z1 \from *z2, *z3;
+
+*/
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2,
+ __mpz_struct const * /*[1]*/ z3);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+ assigns *z1 \from *z2, *z3;
+
+*/
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2,
+ __mpz_struct const * /*[1]*/ z3);
+/*@ requires \valid(z);
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
+int __fc_random_counter __attribute__((__unused__));
+unsigned long const __fc_rand_max = (unsigned long)2147483647;
+extern int __fc_heap_status;
+/*@
+axiomatic
+ dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ ensures \false;
+ assigns \nothing; */
+extern void exit(int status);
+extern FILE *__fc_stdout;
+/*@ assigns *__fc_stdout;
+ assigns *__fc_stdout \from *(format+(..)); */
+extern int printf(char const *format , ...);
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
+{
+ if (! predicate) {
+ printf("%s failed at line %d.\nThe failing predicate is:\n%s.\n",kind,
+ line,pred_txt);
+ exit(1);
+ }
+ return;
+}
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
+ size_t size);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+/*@ behavior yes:
+ assumes ∀ ℤ i; 0 < i ∧ i < n ⇒ *(t+(i-1)) ≤ *(t+i);
+ ensures \result ≡ 1;
+
+
+*/
+int sorted(int *t, int n)
+{
+ int __e_acsl_at;
+ int __retres;
+ int b;
+ __store_block((void *)(& t),4U);
+ __full_init((void *)(& t));
+ {
+ int __e_acsl_forall;
+ mpz_t __e_acsl_i;
+ __e_acsl_forall = 1;
+ __gmpz_init(__e_acsl_i);
+ {
+ mpz_t __e_acsl_5;
+ mpz_t __e_acsl_6;
+ mpz_t __e_acsl_add;
+ __gmpz_init_set_si(__e_acsl_5,(long)0);
+ __gmpz_init_set_si(__e_acsl_6,1L);
+ __gmpz_init(__e_acsl_add);
+ __gmpz_add(__e_acsl_add,(__mpz_struct const *)(__e_acsl_5),
+ (__mpz_struct const *)(__e_acsl_6));
+ __gmpz_set(__e_acsl_i,(__mpz_struct const *)(__e_acsl_add));
+ __gmpz_clear(__e_acsl_5);
+ __gmpz_clear(__e_acsl_6);
+ __gmpz_clear(__e_acsl_add);
+ }
+
+ while (1) {
+ {
+ mpz_t __e_acsl_n;
+ int __e_acsl_lt;
+ __gmpz_init_set_si(__e_acsl_n,(long)n);
+ __e_acsl_lt = __gmpz_cmp((__mpz_struct const *)(__e_acsl_i),
+ (__mpz_struct const *)(__e_acsl_n));
+ if (__e_acsl_lt < 0) { ; } else { break; }
+ __gmpz_clear(__e_acsl_n);
+ }
+
+ {
+ mpz_t __e_acsl;
+ mpz_t __e_acsl_sub;
+ unsigned long __e_acsl_2;
+ mpz_t __e_acsl_3;
+ unsigned long __e_acsl_i_2;
+ mpz_t __e_acsl_4;
+ int __e_acsl_le;
+ __gmpz_init_set_si(__e_acsl,(long)1);
+ __gmpz_init(__e_acsl_sub);
+ __gmpz_sub(__e_acsl_sub,(__mpz_struct const *)(__e_acsl_i),
+ (__mpz_struct const *)(__e_acsl));
+ __e_acsl_2 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_sub));
+ __gmpz_init_set_si(__e_acsl_3,(long)*(t + __e_acsl_2));
+ __e_acsl_i_2 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_i));
+ __gmpz_init_set_si(__e_acsl_4,(long)*(t + __e_acsl_i_2));
+ __e_acsl_le = __gmpz_cmp((__mpz_struct const *)(__e_acsl_3),
+ (__mpz_struct const *)(__e_acsl_4));
+ __gmpz_clear(__e_acsl);
+ __gmpz_clear(__e_acsl_sub);
+ __gmpz_clear(__e_acsl_3);
+ __gmpz_clear(__e_acsl_4);
+ if (__e_acsl_le <= 0) { ; }
+ else {
+ __e_acsl_forall = 0;
+ goto e_acsl_end_loop1; }
+ }
+
+ {
+ mpz_t __e_acsl_7;
+ mpz_t __e_acsl_add_2;
+ __gmpz_init_set_si(__e_acsl_7,1L);
+ __gmpz_init(__e_acsl_add_2);
+ __gmpz_add(__e_acsl_add_2,(__mpz_struct const *)(__e_acsl_i),
+ (__mpz_struct const *)(__e_acsl_7));
+ __gmpz_set(__e_acsl_i,(__mpz_struct const *)(__e_acsl_add_2));
+ __gmpz_clear(__e_acsl_7);
+ __gmpz_clear(__e_acsl_add_2);
+ }
+
+ }
+ e_acsl_end_loop1: /* internal */ ;
+ __e_acsl_at = __e_acsl_forall;
+ __gmpz_clear(__e_acsl_i);
+ }
+
+ b = 1;
+ if (n <= 1) {
+ __retres = 1;
+ goto return_label; }
+ b = 1;
+ while (b < n) {
+ if (*(t + (b - 1)) > *(t + b)) {
+ __retres = 0;
+ goto return_label; }
+ b ++;
+ }
+ __retres = 1;
+ return_label: /* internal */
+ {
+ int __e_acsl_implies;
+ if (! __e_acsl_at) { __e_acsl_implies = 1; }
+ else {
+ mpz_t __e_acsl_result;
+ mpz_t __e_acsl_8;
+ int __e_acsl_eq;
+ __gmpz_init_set_si(__e_acsl_result,(long)__retres);
+ __gmpz_init_set_si(__e_acsl_8,(long)1);
+ __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_result),
+ (__mpz_struct const *)(__e_acsl_8));
+ __e_acsl_implies = __e_acsl_eq == 0;
+ __gmpz_clear(__e_acsl_result);
+ __gmpz_clear(__e_acsl_8);
+ }
+ e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
+ (char *)"\\old(\\forall integer i; 0 < i && i < n ==> *(t+(i-1)) <= *(t+i)) ==>\n\\result == 1",
+ 9);
+ __delete_block((void *)(& t));
+ return (__retres);
+ }
+
+}
+
+int main(void)
+{
+ int __retres;
+ int t[7];
+ int n;
+ __store_block((void *)(t),28U);
+ __initialize((void *)(t),sizeof(int));
+ t[0] = 1;
+ __initialize((void *)(& t[1]),sizeof(int));
+ t[1] = 4;
+ __initialize((void *)(& t[2]),sizeof(int));
+ t[2] = 4;
+ __initialize((void *)(& t[3]),sizeof(int));
+ t[3] = 5;
+ __initialize((void *)(& t[4]),sizeof(int));
+ t[4] = 5;
+ __initialize((void *)(& t[5]),sizeof(int));
+ t[5] = 5;
+ __initialize((void *)(& t[6]),sizeof(int));
+ t[6] = 7;
+ n = sorted(t,7);
+ /*@ assert n ≡ 1; */
+ {
+ mpz_t __e_acsl_n;
+ mpz_t __e_acsl;
+ int __e_acsl_eq;
+ __gmpz_init_set_si(__e_acsl_n,(long)n);
+ __gmpz_init_set_si(__e_acsl,(long)1);
+ __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_n),
+ (__mpz_struct const *)(__e_acsl));
+ e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"n == 1",25);
+ __gmpz_clear(__e_acsl_n);
+ __gmpz_clear(__e_acsl);
+ }
+
+ __retres = 0;
+ __delete_block((void *)(t));
+ __clean();
+ return (__retres);
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
index ebd76810a39..cb8c6c4bcd2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
@@ -56,6 +56,13 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
@@ -85,6 +92,10 @@ struct list *f(struct list *l)
struct list *__e_acsl_at_2;
int __e_acsl_at;
struct list *__retres;
+ __store_block((void *)(& l),4U);
+ __full_init((void *)(& l));
+ __store_block((void *)(& __e_acsl_at_4),4U);
+ __full_init((void *)(& __e_acsl_at_4));
__e_acsl_at_4 = l;
{
int __e_acsl_valid;
@@ -106,7 +117,11 @@ struct list *f(struct list *l)
__e_acsl_at_3 = __e_acsl_and_2;
}
+ __store_block((void *)(& __e_acsl_at_2),4U);
+ __full_init((void *)(& __e_acsl_at_2));
__e_acsl_at_2 = l;
+ __store_block((void *)(& __e_acsl_at),4U);
+ __full_init((void *)(& __e_acsl_at));
__e_acsl_at = l == (void *)0;
if (l == (void *)0) {
__retres = l;
@@ -128,6 +143,7 @@ struct list *f(struct list *l)
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
(char *)"\\old(!\\valid(l) && !\\valid(l->next)) ==>\n\\result == \\old(l)",
22);
+ __delete_block((void *)(& l));
return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
index ebd76810a39..cb8c6c4bcd2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
@@ -56,6 +56,13 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
@@ -85,6 +92,10 @@ struct list *f(struct list *l)
struct list *__e_acsl_at_2;
int __e_acsl_at;
struct list *__retres;
+ __store_block((void *)(& l),4U);
+ __full_init((void *)(& l));
+ __store_block((void *)(& __e_acsl_at_4),4U);
+ __full_init((void *)(& __e_acsl_at_4));
__e_acsl_at_4 = l;
{
int __e_acsl_valid;
@@ -106,7 +117,11 @@ struct list *f(struct list *l)
__e_acsl_at_3 = __e_acsl_and_2;
}
+ __store_block((void *)(& __e_acsl_at_2),4U);
+ __full_init((void *)(& __e_acsl_at_2));
__e_acsl_at_2 = l;
+ __store_block((void *)(& __e_acsl_at),4U);
+ __full_init((void *)(& __e_acsl_at));
__e_acsl_at = l == (void *)0;
if (l == (void *)0) {
__retres = l;
@@ -128,6 +143,7 @@ struct list *f(struct list *l)
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
(char *)"\\old(!\\valid(l) && !\\valid(l->next)) ==>\n\\result == \\old(l)",
22);
+ __delete_block((void *)(& l));
return (__retres);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
index 54c1424c327..88196cccf58 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
@@ -26,6 +26,8 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
+[value] using specification for function __store_block
+[value] using specification for function __full_init
[value] using specification for function __valid
[value] using specification for function __initialized
./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
@@ -34,6 +36,7 @@ tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read
tests/e-acsl-runtime/valid_in_contract.c:21:[value] Non-termination in evaluation of function call expression argument
(void *)l->next
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __delete_block
tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid.
tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid.
tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid, but it is unknown if the behavior is active.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
index 54c1424c327..88196cccf58 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
@@ -26,6 +26,8 @@
[1].__fc_stdio_id ∈ [--..--]
S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
+[value] using specification for function __store_block
+[value] using specification for function __full_init
[value] using specification for function __valid
[value] using specification for function __initialized
./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function __initialized: postcondition got status unknown.
@@ -34,6 +36,7 @@ tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read
tests/e-acsl-runtime/valid_in_contract.c:21:[value] Non-termination in evaluation of function call expression argument
(void *)l->next
./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __delete_block
tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid.
tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid.
tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid, but it is unknown if the behavior is active.
--
GitLab