From bbf3b0a08ed4a78a00e6a0e1aa801a46841e4713 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 7 May 2013 15:24:50 +0000
Subject: [PATCH] [E-ACSL] analysis: fixed soundness bug when calling several
times the same function
---
src/plugins/e-acsl/TODO | 1 -
.../e-acsl/known_bugs/bts1392_ghost_extern.i | 6 -
src/plugins/e-acsl/known_bugs/bts1412.c | 154 ----------------
src/plugins/e-acsl/pre_analysis.ml | 151 +++++++++++-----
.../e-acsl/tests/e-acsl-runtime/call.c | 23 +++
.../e-acsl-runtime/oracle/call.1.err.oracle | 0
.../e-acsl-runtime/oracle/call.1.res.oracle | 58 ++++++
.../e-acsl-runtime/oracle/call.err.oracle | 0
.../e-acsl-runtime/oracle/call.res.oracle | 58 ++++++
.../tests/e-acsl-runtime/oracle/gen_call.c | 171 ++++++++++++++++++
.../tests/e-acsl-runtime/oracle/gen_call2.c | 171 ++++++++++++++++++
.../e-acsl-runtime/oracle/gen_localvar.c | 7 +
.../e-acsl-runtime/oracle/gen_localvar2.c | 7 +
13 files changed, 601 insertions(+), 206 deletions(-)
delete mode 100644 src/plugins/e-acsl/known_bugs/bts1392_ghost_extern.i
delete mode 100644 src/plugins/e-acsl/known_bugs/bts1412.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/call.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index d87df2536ac..8494d38a80e 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -39,7 +39,6 @@
- analysis: optimize it by performing no join over sets anymore
- analysis: fixed incorrectness in presence of recursive functions
- RTE: potential duplication (e.g. with **p)
-- analysis: memoisation of function calls is incorrect
##############
# KNOWN BUGS #
diff --git a/src/plugins/e-acsl/known_bugs/bts1392_ghost_extern.i b/src/plugins/e-acsl/known_bugs/bts1392_ghost_extern.i
deleted file mode 100644
index c44daf35945..00000000000
--- a/src/plugins/e-acsl/known_bugs/bts1392_ghost_extern.i
+++ /dev/null
@@ -1,6 +0,0 @@
-// avec -e-acsl-full-mmodel
-// extern ghost variable
-
-int main(int i, char** j) {
- return 0;
-}
diff --git a/src/plugins/e-acsl/known_bugs/bts1412.c b/src/plugins/e-acsl/known_bugs/bts1412.c
deleted file mode 100644
index b7f30dc8483..00000000000
--- a/src/plugins/e-acsl/known_bugs/bts1412.c
+++ /dev/null
@@ -1,154 +0,0 @@
-
-typedef unsigned size_t;
-extern void* malloc(size_t);
-extern void free(void*);
-#define NULL 0
-#define LEN 5
-
-unsigned long T[LEN];
-
-struct list {
- int element;
- struct list * next;
-};
-
-struct list * merge_sort(struct list *);
-
-
-/*@ behavior null:
- @ assumes l == \null;
- @ ensures \result == \null;
- @ behavior not_null:
- @ ensures \valid(\result);
- @*/
-struct list * merge_sort(struct list * l) {
- if(l == NULL)
- return l;
- if(l->next == NULL)
- return l;
-
- /* SPLIT */
- int cpt = 0;
- struct list * L1 = l, * L2 = l->next, * next, * ret = NULL,
- * tmp = L2->next, * iterL1 = L1, * iterL2 = L2;
- L1->next = L2->next = NULL;
-
- while(tmp != NULL) {
- struct list * new = malloc(sizeof(struct list));
- new->element = tmp->element;
- new->next = NULL;
-
- next = tmp->next;
- if(cpt % 2)
- iterL2 = (iterL2->next = new);
- else
- iterL1 = (iterL1->next = new);
- free(tmp);
- tmp = next;
- cpt++;
- }
-
- /* RECURSION */
- L1 = merge_sort(L1);
- L2 = merge_sort(L2);
-
- /* MERGE */
- if(L1->element < L2->element) {
- ret = L1;
- L1 = L1->next;
- } else {
- ret = L2;
- L2 = L2->next;
- }
- tmp = ret;
-
- while(L1 != NULL || L2 != NULL) {
- if(L1 == NULL) {
- tmp->next = L2;
- break;
- }
- if(L2 == NULL) {
- tmp->next = L1;
- break;
- }
- struct list * new = malloc(sizeof(struct list));
-
- if(L1->element < L2->element) {
- new->element = L1->element;
- new->next = NULL;
- tmp->next = new;
- next = L1->next;
- free(L1);
- L1 = next;
- } else {
- new->element = L2->element;
- new->next = NULL;
- tmp->next = new;
- next = L2->next;
- free(L2);
- L2 = next;
- }
- tmp = new;
- }
-
- return l;
-}
-
-
-/*@ ensures \valid(\result);
- @ ensures \result->element == i;
- @ ensures \result->next == \old(l);
- @*/
-struct list * add(struct list * l, int i) {
- struct list * new;
- new = malloc(sizeof(struct list));
- new->element = i;
- new->next = l;
- return new;
-}
-
-/*@ ensures \result == \null;
- @*/
-struct list * erase(struct list * l) {
- struct list * tmp = l;
- while(tmp != NULL) {
- struct list * next = tmp->next;
- //@ assert \valid(tmp);
- free(tmp);
- tmp = next;
- }
- return tmp;
-}
-
-int main() {
- struct list * L = NULL;
- int i = 0;
-
- //@ assert 0 <= i <= LEN;
- /*@ loop invariant 0 <= i <= LEN;
- @ loop assigns i, T[0..(LEN-1)];
- @ loop variant LEN-i;
- @*/
- for(; i < LEN;) {
- T[i] = i+LEN%32*i;
- i++;
- //@ assert 0 <= i <= LEN;
- }
-
- i = 0;
- //@ assert 0 <= i <= LEN;
- /*@ loop invariant 0 <= i <= LEN;
- @ loop assigns i, L;
- @ loop variant LEN-i;
- @*/
- for(; i < LEN;) {
- L = add(L, T[i]);
- i++;
- //@ assert 0 <= i <= LEN;
- }
- L = merge_sort(L);
- L = erase(L);
-
- return 0;
-}
-
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 68594cbad3b..3fa1ed3f482 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -50,19 +50,21 @@ let get_rte_by_stmt =
(let module L = Datatype.List(Code_annotation) in L.ty))
module Env: sig
- val default_varinfos: Varinfo.Set.t option -> Varinfo.Set.t
+ val default_varinfos: Varinfo.Hptset.t option -> Varinfo.Hptset.t
val apply: (kernel_function -> 'a) -> kernel_function -> 'a
val clear: unit -> unit
- val add: kernel_function -> Varinfo.Set.t option Stmt.Hashtbl.t -> unit
- val find: kernel_function -> Varinfo.Set.t option Stmt.Hashtbl.t
- module StartData: Dataflow.StmtStartData with type data = Varinfo.Set.t option
+ val add: kernel_function -> Varinfo.Hptset.t option Stmt.Hashtbl.t -> unit
+ val add_init: kernel_function -> Varinfo.Hptset.t option -> unit
+ val mem_init: kernel_function -> Varinfo.Hptset.t option -> bool
+ val find: kernel_function -> Varinfo.Hptset.t option Stmt.Hashtbl.t
+ module StartData: Dataflow.StmtStartData with type data = Varinfo.Hptset.t option
val is_consolidated: unit -> bool
- val consolidate: Varinfo.Set.t -> unit
+ val consolidate: Varinfo.Hptset.t -> unit
val consolidated_mem: varinfo -> bool
end = struct
let current_kf = ref (Kernel_function.dummy ())
- let default_varinfos = function None -> Varinfo.Set.empty | Some s -> s
+ let default_varinfos = function None -> Varinfo.Hptset.empty | Some s -> s
let apply f kf =
let old = !current_kf in
@@ -75,8 +77,26 @@ end = struct
let add = Kernel_function.Hashtbl.add tbl
let find = Kernel_function.Hashtbl.find tbl
+ module S = Set.Make(Datatype.Option(Varinfo.Hptset))
+
+ let tbl_init = Kernel_function.Hashtbl.create 7
+ let add_init kf init =
+ let set =
+ try Kernel_function.Hashtbl.find tbl_init kf
+ with Not_found -> S.empty
+ in
+ let set = S.add init set in
+ Kernel_function.Hashtbl.replace tbl_init kf set
+
+ let mem_init kf init =
+ try
+ let set = Kernel_function.Hashtbl.find tbl_init kf in
+ S.mem init set
+ with Not_found ->
+ false
+
module StartData = struct
- type data = Varinfo.Set.t option
+ type data = Varinfo.Hptset.t option
let apply f =
try
let h = Kernel_function.Hashtbl.find tbl !current_kf in
@@ -92,22 +112,25 @@ end = struct
let length () = apply Stmt.Hashtbl.length
end
- let consolidated_set = ref Varinfo.Set.empty
+ (* TODO: instead of this costly consolidation, why do not take the state of
+ the entry point of the function? *)
+
+ let consolidated_set = ref Varinfo.Hptset.empty
let is_consolidated_ref = ref false
let consolidate set =
- let set = Varinfo.Set.fold Varinfo.Set.add set !consolidated_set in
+ let set = Varinfo.Hptset.union set !consolidated_set in
consolidated_set := set
let consolidated_mem v =
is_consolidated_ref := true;
- Varinfo.Set.mem v !consolidated_set
+ Varinfo.Hptset.mem v !consolidated_set
let is_consolidated () = !is_consolidated_ref
let clear () =
Kernel_function.Hashtbl.clear tbl;
- consolidated_set := Varinfo.Set.empty;
+ consolidated_set := Varinfo.Hptset.empty;
is_consolidated_ref := false
end
@@ -117,20 +140,20 @@ let reset () =
Env.clear ()
module rec Transfer
- : Dataflow.BackwardsTransfer with type t = Varinfo.Set.t option
+ : Dataflow.BackwardsTransfer with type t = Varinfo.Hptset.t option
= struct
let name = "E_ACSL.Pre_analysis"
let debug = ref false
- type t = Varinfo.Set.t option
+ type t = Varinfo.Hptset.t option
module StmtStartData = Env.StartData
let pretty fmt state = match state with
| None -> Format.fprintf fmt "None"
- | Some s -> Format.fprintf fmt "%a" Varinfo.Set.pretty s
+ | Some s -> Format.fprintf fmt "%a" Varinfo.Hptset.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
@@ -144,16 +167,18 @@ module rec Transfer
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_))
+ | Return _, Some old, Some new_ ->
+ Some (Some (Varinfo.Hptset.union old new_))
| _, Some old, Some new_ ->
- if Varinfo.Set.equal old new_ then
+ if Varinfo.Hptset.equal old new_ then
None
else
- Some (Some (Varinfo.Set.union old new_))
+ Some (Some (Varinfo.Hptset.union old new_))
(** Take the data from two successors and combine it *)
let combineSuccessors s1 s2 =
- Some (Varinfo.Set.union (Env.default_varinfos s1) (Env.default_varinfos s2))
+ Some
+ (Varinfo.Hptset.union (Env.default_varinfos s1) (Env.default_varinfos s2))
let is_ptr_or_array ty = Cil.isPtrType ty || Cil.isArrayType ty
@@ -166,7 +191,7 @@ module rec Transfer
Options.feedback ~level:4 ~dkey "monitoring %a from annotation of %a."
Printer.pp_varinfo vi
Kernel_function.pretty kf;
- Varinfo.Set.add vi varinfos
+ Varinfo.Hptset.add vi varinfos
in
match thost with
| TVar { lv_origin = None } -> varinfos
@@ -347,7 +372,7 @@ module rec Transfer
let state = Env.default_varinfos state in
let extend_to_expr state lhost e =
let add_vi state vi =
- if is_ptr_or_array_exp e && Varinfo.Set.mem vi state then
+ if is_ptr_or_array_exp e && Varinfo.Hptset.mem vi state then
match base_addr e with
| None -> state
| Some vi_e ->
@@ -355,7 +380,7 @@ module rec Transfer
"monitoring %a from %a."
Printer.pp_varinfo vi_e
Printer.pp_lval (lhost, NoOffset);
- Varinfo.Set.add vi_e state
+ Varinfo.Hptset.add vi_e state
else
state
in
@@ -398,7 +423,8 @@ module rec Transfer
(fun acc p a -> match base_addr a with
| None -> acc
| Some vi ->
- if Varinfo.Set.mem vi state then Varinfo.Set.add p acc
+ if Varinfo.Hptset.mem vi state
+ then Varinfo.Hptset.add p acc
else acc)
state
params
@@ -410,8 +436,8 @@ module rec Transfer
match base_addr_node (Lval lv) with
| None -> init
| Some vi ->
- if Varinfo.Set.mem vi state
- then Varinfo.Set.add (Misc.result_vi kf) init
+ if Varinfo.Hptset.mem vi state
+ then Varinfo.Hptset.add (Misc.result_vi kf) init
else init
in
let state = Compute.get ~init kf in
@@ -421,7 +447,7 @@ module rec Transfer
(fun acc p a -> match base_addr a with
| None -> acc
| Some vi ->
- if Varinfo.Set.mem p state then Varinfo.Set.add vi acc
+ if Varinfo.Hptset.mem p state then Varinfo.Hptset.add vi acc
else acc)
state
params
@@ -435,11 +461,20 @@ module rec Transfer
else
state
in
- let state = match result with
- | None -> state
- | Some (lhost, _) ->
- (* result of this call must be kept; so keep each argument *)
- List.fold_left (fun acc e -> extend_to_expr acc lhost e) state l
+ let state = match result, Kernel_function.is_definition kf with
+ | None, _ | _, false -> state
+ | Some (lhost, _), true ->
+ (* add the result if \result must be kept after calling the kf *)
+ let vi = Misc.result_vi kf in
+ if Varinfo.Hptset.mem vi state then
+ match lhost with
+ | Var vi -> Varinfo.Hptset.add vi state
+ | Mem e ->
+ match base_addr e with
+ | None -> Kernel.fatal "no base address for %a" Printer.pp_exp e
+ | Some vi -> Varinfo.Hptset.add vi state
+ else
+ state
in
Dataflow.Done (Some state)
| _ ->
@@ -451,7 +486,7 @@ instrumentation.";
(List.fold_left
(fun acc e -> match base_addr e with
| None -> acc
- | Some vi -> Varinfo.Set.add vi acc)
+ | Some vi -> Varinfo.Hptset.add vi acc)
state
l)))
| Asm _ -> Error.not_yet "asm"
@@ -474,7 +509,7 @@ instrumentation.";
end
and Compute: sig
- val get: ?init:Varinfo.Set.t -> kernel_function -> Varinfo.Set.t
+ val get: ?init:Varinfo.Hptset.t -> kernel_function -> Varinfo.Hptset.t
end = struct
module D = Dataflow.Backwards(Transfer)
@@ -483,17 +518,37 @@ end = struct
Options.feedback ~dkey ~level:2 "entering in function %a."
Kernel_function.pretty kf;
assert (not (Misc.is_library_loc (Kernel_function.get_location kf)));
- let tbl = Stmt.Hashtbl.create 17 in
+ let tbl, is_init =
+ try Env.find kf, true
+ with Not_found -> Stmt.Hashtbl.create 17, false
+ in
(* Options.feedback "ANALYSING %a" Kernel_function.pretty kf;*)
- Env.add kf tbl;
+ if not is_init then Env.add kf tbl;
(try
let fundec = Kernel_function.get_definition kf in
let stmts, returns = Dataflow.find_stmts fundec in
- List.iter (fun s -> Stmt.Hashtbl.add tbl s None) stmts;
- Extlib.may
- (fun set ->
- List.iter (fun s -> Stmt.Hashtbl.replace tbl s (Some set)) returns)
- init_set;
+ if is_init then
+ Extlib.may
+ (fun set ->
+ List.iter
+ (fun s ->
+ let old =
+ try Extlib.the (Stmt.Hashtbl.find tbl s)
+ with Not_found -> assert false
+ in
+ Stmt.Hashtbl.replace
+ tbl
+ s
+ (Some (Varinfo.Hptset.union set old)))
+ returns)
+ init_set
+ else begin
+ List.iter (fun s -> Stmt.Hashtbl.add tbl s None) stmts;
+ Extlib.may
+ (fun set ->
+ List.iter (fun s -> Stmt.Hashtbl.replace tbl s (Some set)) returns)
+ init_set
+ end;
D.compute returns
with Kernel_function.No_Definition | Kernel_function.No_Statement ->
());
@@ -503,14 +558,19 @@ end = struct
let get ?init kf =
if Misc.is_library_loc (Kernel_function.get_location kf) then
- Varinfo.Set.empty
+ Varinfo.Hptset.empty
else
try
let stmt = Kernel_function.find_first_stmt kf in
(* Options.feedback "GETTING %a" Kernel_function.pretty kf;*)
let tbl =
- try Env.find kf
- with Not_found -> Env.apply (compute init) kf
+ if Env.mem_init kf init then
+ try Env.find kf with Not_found -> assert false
+ else begin
+ (* WARN: potentially incorrect in case of recursive call *)
+ Env.add_init kf init;
+ Env.apply (compute init) kf
+ end
in
try
let set = Stmt.Hashtbl.find tbl stmt in
@@ -518,7 +578,7 @@ end = struct
with Not_found ->
Options.fatal "stmt never analyzed: %a" Printer.pp_stmt stmt
with Kernel_function.No_Statement ->
- Varinfo.Set.empty
+ Varinfo.Hptset.empty
end
@@ -548,7 +608,8 @@ let must_model_vi ?kf ?stmt vi =
(* [JS 2013/05/07] that is unsound to take the env from the given stmt in
presence of aliasing with an address (see tests address.i).
TODO: could be optimized though *)
- consolidated_must_model_vi vi
+ let res = consolidated_must_model_vi vi in
+ res
(* match stmt, kf with
| None, _ -> consolidated_must_model_vi vi
| Some _, None ->
@@ -560,7 +621,7 @@ let must_model_vi ?kf ?stmt vi =
let tbl = Env.find kf in
try
let set = Stmt.Hashtbl.find tbl stmt in
- Varinfo.Set.mem vi (Env.default_varinfos set)
+ Varinfo.Hptset.mem vi (Env.default_varinfos set)
with Not_found ->
(* new statement *)
consolidated_must_model_vi vi
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/call.c b/src/plugins/e-acsl/tests/e-acsl-runtime/call.c
new file mode 100644
index 00000000000..ead459fbf85
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/call.c
@@ -0,0 +1,23 @@
+/* run.config
+ COMMENT: function call
+ STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
+ EXECNOW: LOG gen_call.c BIN gen_call.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/call.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_call.c > /dev/null && ./gcc_test.sh call
+ EXECNOW: LOG gen_call2.c BIN gen_call2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/call.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_call2.c > /dev/null && ./gcc_test.sh call2
+*/
+
+#include <stdlib.h>
+
+extern void *malloc(unsigned int size);
+
+/*@ ensures \valid(\result); */
+int *f(int *x, int *y) {
+ *y = 1;
+ return x;
+}
+
+int main() {
+ int x = 0, *p, *q = malloc(sizeof(int)), *r = malloc(sizeof(int));
+ p = f(&x, q);
+ q = f(&x, r);
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
new file mode 100644
index 00000000000..a3b1305bb08
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
@@ -0,0 +1,58 @@
+[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/e_acsl_gmp_types.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/e_acsl_gmp.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/e_acsl.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_api.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_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/call.c"
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[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 ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __memory_size ∈ [--..--]
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __delete_block
+FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+[value] using specification for function __initialize
+tests/e-acsl-runtime/call.c:12:[value] Function f: postcondition got status valid.
+[value] using specification for function __valid
+[value] using specification for function e_acsl_assert
+share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/call.c:12:[value] Function __e_acsl_f: postcondition got status valid.
+[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
+[value] using specification for function __clean
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values at end of function __e_acsl_malloc:
+ __fc_heap_status ∈ [--..--]
+ __retres ∈ {{ &Frama_C_alloc ; &Frama_C_alloc_0 }}
+[value] Values at end of function f:
+ Frama_C_alloc[bits 0 to 31] ∈ {1}
+ Frama_C_alloc_0[bits 0 to 31] ∈ {1} or UNINITIALIZED
+[value] Values at end of function __e_acsl_f:
+ __retres ∈ {{ &x }}
+ Frama_C_alloc[bits 0 to 31] ∈ {1}
+ Frama_C_alloc_0[bits 0 to 31] ∈ {1} or UNINITIALIZED
+[value] Values at end of function main:
+ __fc_heap_status ∈ [--..--]
+ x ∈ {0}
+ p ∈ {{ &x }}
+ q ∈ {{ &x }}
+ r ∈ {{ &Frama_C_alloc_0 }}
+ __retres ∈ {0}
+ Frama_C_alloc[bits 0 to 31] ∈ {1}
+ Frama_C_alloc_0[bits 0 to 31] ∈ {1}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
new file mode 100644
index 00000000000..a3b1305bb08
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
@@ -0,0 +1,58 @@
+[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/e_acsl_gmp_types.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/e_acsl_gmp.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/e_acsl.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_api.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_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/call.c"
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[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 ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __memory_size ∈ [--..--]
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __delete_block
+FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+[value] using specification for function __initialize
+tests/e-acsl-runtime/call.c:12:[value] Function f: postcondition got status valid.
+[value] using specification for function __valid
+[value] using specification for function e_acsl_assert
+share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/call.c:12:[value] Function __e_acsl_f: postcondition got status valid.
+[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
+[value] using specification for function __clean
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values at end of function __e_acsl_malloc:
+ __fc_heap_status ∈ [--..--]
+ __retres ∈ {{ &Frama_C_alloc ; &Frama_C_alloc_0 }}
+[value] Values at end of function f:
+ Frama_C_alloc[bits 0 to 31] ∈ {1}
+ Frama_C_alloc_0[bits 0 to 31] ∈ {1} or UNINITIALIZED
+[value] Values at end of function __e_acsl_f:
+ __retres ∈ {{ &x }}
+ Frama_C_alloc[bits 0 to 31] ∈ {1}
+ Frama_C_alloc_0[bits 0 to 31] ∈ {1} or UNINITIALIZED
+[value] Values at end of function main:
+ __fc_heap_status ∈ [--..--]
+ x ∈ {0}
+ p ∈ {{ &x }}
+ q ∈ {{ &x }}
+ r ∈ {{ &Frama_C_alloc_0 }}
+ __retres ∈ {0}
+ Frama_C_alloc[bits 0 to 31] ∈ {1}
+ Frama_C_alloc_0[bits 0 to 31] ∈ {1}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
new file mode 100644
index 00000000000..6924634d17c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
@@ -0,0 +1,171 @@
+/* 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;
+/*@
+model __mpz_struct { ℤ n };
+*/
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+int __fc_random_counter __attribute__((__unused__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic
+ dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
+ behavior allocation:
+ assumes is_allocable(size);
+ ensures \fresh{Old, Here}(\result,\old(size));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+
+ behavior no_allocation:
+ assumes ¬is_allocable(size);
+ ensures \result ≡ \null;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+extern void *__malloc(size_t size);
+
+/*@ 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(void *ptr, size_t size);
+
+extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
+extern size_t __memory_size;
+
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
+ behavior allocation:
+ assumes is_allocable(size);
+ ensures \fresh{Old, Here}(\result,\old(size));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+
+ behavior no_allocation:
+ assumes ¬is_allocable(size);
+ ensures \result ≡ \null;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void *__e_acsl_malloc(size_t size)
+{
+ void *__retres;
+ __store_block((void *)(& __retres),4U);
+ __retres = __malloc(size);
+ __delete_block((void *)(& __retres));
+ return __retres;
+}
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+
+*/
+/*@ ensures \valid(\result); */
+int *f(int *x, int *y)
+{
+ __store_block((void *)(& x),4U);
+ __store_block((void *)(& y),4U);
+ __initialize((void *)y,sizeof(int));
+ *y = 1;
+ __delete_block((void *)(& x));
+ __delete_block((void *)(& y));
+ return x;
+}
+
+/*@ ensures \valid(\result); */
+int *__e_acsl_f(int *x, int *y)
+{
+ int *__retres;
+ __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& x),4U);
+ __store_block((void *)(& y),4U);
+ __retres = f(x,y);
+ {
+ int __e_acsl_valid;
+ __e_acsl_valid = __valid((void *)__retres,sizeof(int));
+ e_acsl_assert(__e_acsl_valid,(char *)"Postcondition",(char *)"f",
+ (char *)"\\valid(\\result)",12);
+ __delete_block((void *)(& x));
+ __delete_block((void *)(& y));
+ __delete_block((void *)(& __retres));
+ return __retres;
+ }
+}
+
+int main(void)
+{
+ int __retres;
+ int x;
+ int *p;
+ int *q;
+ int *r;
+ __store_block((void *)(& q),4U);
+ __store_block((void *)(& p),4U);
+ __store_block((void *)(& x),4U);
+ __full_init((void *)(& x));
+ x = 0;
+ __full_init((void *)(& q));
+ q = (int *)__e_acsl_malloc(sizeof(int));
+ r = (int *)__e_acsl_malloc(sizeof(int));
+ __full_init((void *)(& p));
+ p = __e_acsl_f(& x,q);
+ __full_init((void *)(& q));
+ q = __e_acsl_f(& x,r);
+ __retres = 0;
+ __delete_block((void *)(& q));
+ __delete_block((void *)(& p));
+ __delete_block((void *)(& x));
+ __clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
new file mode 100644
index 00000000000..6924634d17c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
@@ -0,0 +1,171 @@
+/* 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;
+/*@
+model __mpz_struct { ℤ n };
+*/
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+int __fc_random_counter __attribute__((__unused__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic
+ dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
+ behavior allocation:
+ assumes is_allocable(size);
+ ensures \fresh{Old, Here}(\result,\old(size));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+
+ behavior no_allocation:
+ assumes ¬is_allocable(size);
+ ensures \result ≡ \null;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+extern void *__malloc(size_t size);
+
+/*@ 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(void *ptr, size_t size);
+
+extern __attribute__((__FC_BUILTIN__)) void __clean(void);
+
+extern size_t __memory_size;
+
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
+ behavior allocation:
+ assumes is_allocable(size);
+ ensures \fresh{Old, Here}(\result,\old(size));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+
+ behavior no_allocation:
+ assumes ¬is_allocable(size);
+ ensures \result ≡ \null;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void *__e_acsl_malloc(size_t size)
+{
+ void *__retres;
+ __store_block((void *)(& __retres),4U);
+ __retres = __malloc(size);
+ __delete_block((void *)(& __retres));
+ return __retres;
+}
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+
+*/
+/*@ ensures \valid(\result); */
+int *f(int *x, int *y)
+{
+ __store_block((void *)(& x),4U);
+ __store_block((void *)(& y),4U);
+ __initialize((void *)y,sizeof(int));
+ *y = 1;
+ __delete_block((void *)(& x));
+ __delete_block((void *)(& y));
+ return x;
+}
+
+/*@ ensures \valid(\result); */
+int *__e_acsl_f(int *x, int *y)
+{
+ int *__retres;
+ __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& x),4U);
+ __store_block((void *)(& y),4U);
+ __retres = f(x,y);
+ {
+ int __e_acsl_valid;
+ __e_acsl_valid = __valid((void *)__retres,sizeof(int));
+ e_acsl_assert(__e_acsl_valid,(char *)"Postcondition",(char *)"f",
+ (char *)"\\valid(\\result)",12);
+ __delete_block((void *)(& x));
+ __delete_block((void *)(& y));
+ __delete_block((void *)(& __retres));
+ return __retres;
+ }
+}
+
+int main(void)
+{
+ int __retres;
+ int x;
+ int *p;
+ int *q;
+ int *r;
+ __store_block((void *)(& q),4U);
+ __store_block((void *)(& p),4U);
+ __store_block((void *)(& x),4U);
+ __full_init((void *)(& x));
+ x = 0;
+ __full_init((void *)(& q));
+ q = (int *)__e_acsl_malloc(sizeof(int));
+ r = (int *)__e_acsl_malloc(sizeof(int));
+ __full_init((void *)(& p));
+ p = __e_acsl_f(& x,q);
+ __full_init((void *)(& q));
+ q = __e_acsl_f(& x,r);
+ __retres = 0;
+ __delete_block((void *)(& q));
+ __delete_block((void *)(& p));
+ __delete_block((void *)(& x));
+ __clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
index 61a4f0a1f7f..4cfbaf98faa 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
@@ -125,6 +125,7 @@ struct list *add(struct list *l, int i)
{
struct list *new;
__store_block((void *)(& new),4U);
+ __store_block((void *)(& l),4U);
__full_init((void *)(& new));
new = (struct list *)__e_acsl_malloc(sizeof(struct list));
/*@ assert \valid(new); */
@@ -146,6 +147,7 @@ struct list *add(struct list *l, int i)
new->element = i;
__initialize((void *)(& new->next),sizeof(struct list *));
new->next = l;
+ __delete_block((void *)(& l));
__delete_block((void *)(& new));
return new;
}
@@ -154,10 +156,15 @@ int main(void)
{
int __retres;
struct list *l;
+ __store_block((void *)(& l),4U);
+ __full_init((void *)(& l));
l = (struct list *)((void *)0);
+ __full_init((void *)(& l));
l = add(l,4);
+ __full_init((void *)(& l));
l = add(l,7);
__retres = 0;
+ __delete_block((void *)(& l));
__clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
index 61a4f0a1f7f..4cfbaf98faa 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
@@ -125,6 +125,7 @@ struct list *add(struct list *l, int i)
{
struct list *new;
__store_block((void *)(& new),4U);
+ __store_block((void *)(& l),4U);
__full_init((void *)(& new));
new = (struct list *)__e_acsl_malloc(sizeof(struct list));
/*@ assert \valid(new); */
@@ -146,6 +147,7 @@ struct list *add(struct list *l, int i)
new->element = i;
__initialize((void *)(& new->next),sizeof(struct list *));
new->next = l;
+ __delete_block((void *)(& l));
__delete_block((void *)(& new));
return new;
}
@@ -154,10 +156,15 @@ int main(void)
{
int __retres;
struct list *l;
+ __store_block((void *)(& l),4U);
+ __full_init((void *)(& l));
l = (struct list *)((void *)0);
+ __full_init((void *)(& l));
l = add(l,4);
+ __full_init((void *)(& l));
l = add(l,7);
__retres = 0;
+ __delete_block((void *)(& l));
__clean();
return __retres;
}
--
GitLab