diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index a1e78558beae129f7a85f2585ae7f97bfeb01764..2616dfe348ecf0cccffe24ea501655179a83052c 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -143,9 +143,6 @@ let get_orig_name kf =
let name = Kernel_function.get_name kf in
strip_prefix e_acsl_gen_prefix name
-let is_alloc_name fn =
- fn = "malloc" || fn = "free" || fn = "realloc" || fn = "calloc"
-
let mk_api_name fname =
e_acsl_api_prefix ^ fname
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index 10a2a111be7c8d3101a0eb0db7705ca7a8fde82d..25aae974b69f88db507a7f3bff88e48eb9e8bdfa 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -101,10 +101,6 @@ pointer and integer parts. *)
(** {2 Handling prefixes of generated library functions and variables} *)
(* ************************************************************************** *)
-val is_alloc_name: string -> bool
-(** @return true if a given string matches the name of a
- memory-allocation function recognized by E-ACSL. *)
-
val mk_api_name: string -> string
(** @return given some base name append it with a prefix used
by functions and variables in the public API of E-ACSL runtime library.
diff --git a/src/plugins/e-acsl/mmodel_analysis.ml b/src/plugins/e-acsl/mmodel_analysis.ml
index 5ef4a927fdb6bdae42cb6902c235c14f22e052be..9e7c308a9af4b092b6a49dc97cc98afdb27b692f 100644
--- a/src/plugins/e-acsl/mmodel_analysis.ml
+++ b/src/plugins/e-acsl/mmodel_analysis.ml
@@ -31,15 +31,15 @@ open Cil_datatype
let dkey = Options.dkey_analysis
module Env: sig
val has_heap_allocations: unit -> bool
- val check_heap_allocations: string -> unit
+ val check_heap_allocations: kernel_function -> unit
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.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:
+ 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.Hptset.t -> unit
@@ -49,11 +49,13 @@ end = struct
let heap_allocation_ref = ref false
let has_heap_allocations () = !heap_allocation_ref
- let check_heap_allocations fn =
- heap_allocation_ref := !heap_allocation_ref || Misc.is_alloc_name fn
+ let check_heap_allocations kf =
+ (* a function with no definition potentially allocates memory *)
+ heap_allocation_ref :=
+ !heap_allocation_ref || not (Kernel_function.is_definition kf)
let current_kf = ref None
- let default_varinfos = function None -> Varinfo.Hptset.empty | Some s -> s
+ let default_varinfos = function None -> Varinfo.Hptset.empty | Some s -> s
let apply f kf =
let old = !current_kf in
@@ -69,7 +71,7 @@ end = struct
module S = Set.Make(Datatype.Option(Varinfo.Hptset))
let tbl_init = Kernel_function.Hashtbl.create 7
- let add_init kf init =
+ let add_init kf init =
let set =
try Kernel_function.Hashtbl.find tbl_init kf
with Not_found -> S.empty
@@ -77,21 +79,21 @@ end = struct
let set = S.add init set in
Kernel_function.Hashtbl.replace tbl_init kf set
- let mem_init kf init =
- try
+ let mem_init kf init =
+ try
let set = Kernel_function.Hashtbl.find tbl_init kf in
S.mem init set
- with Not_found ->
+ with Not_found ->
false
module StartData = struct
type data = Varinfo.Hptset.t option
- let apply f =
+ let apply f =
try
let kf = Extlib.opt_conv (Kernel_function.dummy()) !current_kf in
let h = Kernel_function.Hashtbl.find tbl kf in
f h
- with Not_found ->
+ with Not_found ->
assert false
let clear () = apply Stmt.Hashtbl.clear
let mem k = apply Stmt.Hashtbl.mem k
@@ -108,11 +110,11 @@ end = struct
let consolidated_set = ref Varinfo.Hptset.empty
let is_consolidated_ref = ref false
- let consolidate set =
+ let consolidate set =
let set = Varinfo.Hptset.union set !consolidated_set in
consolidated_set := set
- let consolidated_mem v =
+ let consolidated_mem v =
is_consolidated_ref := true;
Varinfo.Hptset.mem v !consolidated_set
@@ -121,7 +123,7 @@ end = struct
let is_empty () =
try
Kernel_function.Hashtbl.iter
- (fun _ h ->
+ (fun _ h ->
Stmt.Hashtbl.iter
(fun _ set -> match set with
| None -> ()
@@ -132,7 +134,7 @@ end = struct
with Exit ->
false
- let clear () =
+ let clear () =
Kernel_function.Hashtbl.clear tbl;
consolidated_set := Varinfo.Hptset.empty;
is_consolidated_ref := false;
@@ -140,7 +142,7 @@ end = struct
end
-let reset () =
+let reset () =
Options.feedback ~dkey ~level:2 "clearing environment.";
Env.clear ()
@@ -172,17 +174,17 @@ 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_ ->
+ | Return _, Some old, Some new_ ->
Some (Some (Varinfo.Hptset.union old new_))
- | _, Some old, Some new_ ->
+ | _, Some old, Some new_ ->
if Varinfo.Hptset.equal old new_ then
None
else
Some (Some (Varinfo.Hptset.union old new_))
(** Take the data from two successors and combine it *)
- let combineSuccessors s1 s2 =
- Some
+ let combineSuccessors s1 s2 =
+ Some
(Varinfo.Hptset.union (Env.default_varinfos s1) (Env.default_varinfos s2))
let is_ptr_or_array ty = Cil.isPointerType ty || Cil.isArrayType ty
@@ -192,43 +194,43 @@ module rec Transfer
is_ptr_or_array ty
let rec base_addr_node = function
- | Lval lv | AddrOf lv | StartOf lv ->
+ | Lval lv | AddrOf lv | StartOf lv ->
(match lv with
| Var vi, _ -> Some vi
| Mem e, _ -> base_addr e)
- | BinOp((PlusPI | IndexPI | MinusPI), e1, e2, _) ->
+ | BinOp((PlusPI | IndexPI | MinusPI), e1, e2, _) ->
if is_ptr_or_array_exp e1 then base_addr e1
else begin
assert (is_ptr_or_array_exp e2);
base_addr e2
end
| Info(e, _) | CastE(_, e) -> base_addr e
- | BinOp((MinusPP | PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt
+ | BinOp((MinusPP | PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt
| Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr),
_, _, _)
- | UnOp _ | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _
- | AlignOfE _ ->
+ | UnOp _ | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _
+ | AlignOfE _ ->
None
and base_addr e = base_addr_node e.enode
let extend_to_expr always state lhost e =
let add_vi state vi =
- if is_ptr_or_array_exp e && (always || Varinfo.Hptset.mem vi state) then
+ if is_ptr_or_array_exp e && (always || Varinfo.Hptset.mem vi state) then
match base_addr e with
| None -> state
- | Some vi_e ->
+ | Some vi_e ->
Options.feedback ~level:4 ~dkey
"monitoring %a from %a."
Printer.pp_varinfo vi_e
Printer.pp_lval (lhost, NoOffset);
Varinfo.Hptset.add vi_e state
- else
+ else
state
in
match lhost with
| Var vi -> add_vi state vi
- | Mem e ->
+ | Mem e ->
match base_addr e with
| None -> state
| Some vi -> add_vi state vi
@@ -241,10 +243,10 @@ module rec Transfer
true
else
state, false
- | AddrOf(lhost, _) ->
+ | AddrOf(lhost, _) ->
extend_to_expr true state lhost (Cil.new_exp ~loc:e.eloc (Lval lv)),
true
- | BinOp((PlusPI | IndexPI | MinusPI), e1, e2, _) ->
+ | BinOp((PlusPI | IndexPI | MinusPI), e1, e2, _) ->
if is_ptr_or_array_exp e1 then extend_from_addr state lv e1
else begin
assert (is_ptr_or_array_exp e2);
@@ -258,10 +260,10 @@ module rec Transfer
let state, always = extend_from_addr state lv e in
extend_to_expr always state lhost e
- let rec register_term_lval kf varinfos (thost, _) =
+ let rec register_term_lval kf varinfos (thost, _) =
let add_vi kf vi =
- Options.feedback ~level:4 ~dkey "monitoring %a from annotation of %a."
- Printer.pp_varinfo vi
+ Options.feedback ~level:4 ~dkey "monitoring %a from annotation of %a."
+ Printer.pp_varinfo vi
Kernel_function.pretty kf;
Varinfo.Hptset.add vi varinfos
in
@@ -272,7 +274,7 @@ module rec Transfer
| TMem t -> register_term kf varinfos t
and register_term kf varinfos term = match term.term_node with
- | TLval tlv | TAddrOf tlv | TStartOf tlv ->
+ | TLval tlv | TAddrOf tlv | TStartOf tlv ->
register_term_lval kf varinfos tlv
| TCastE(_, t) | Tat(t, _) | Tlet(_, t) ->
register_term kf varinfos t
@@ -282,7 +284,7 @@ module rec Transfer
| TBinOp((PlusPI | IndexPI | MinusPI), t1, t2) ->
(match t1.term_type with
| Ctype ty when is_ptr_or_array ty -> register_term kf varinfos t1
- | _ ->
+ | _ ->
match t2.term_type with
| Ctype ty when is_ptr_or_array ty -> register_term kf varinfos t2
| _ -> assert false)
@@ -319,22 +321,22 @@ module rec Transfer
| Pseparated _ -> Error.not_yet "\\separated"
| Pdangling _ -> Error.not_yet "\\dangling"
| Ptrue | Pfalse | Papp _ | Prel _
- | Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _
+ | 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.DoChildren
- | TConst _ | TSizeOf _ | TSizeOfStr _ | TAlignOf _ | Tnull | Ttype _
- | Tempty_set ->
+ | TConst _ | TSizeOf _ | TSizeOfStr _ | TAlignOf _ | Tnull | Ttype _
+ | Tempty_set ->
(* no left-value inside inside: skip for efficiency *)
Cil.SkipChildren
| TUnOp _ | TBinOp _ | Ttypeof _ | TSizeOfE _
| TLval _ | TAlignOfE _ | TCastE _ | TAddrOf _
| TStartOf _ | Tapp _ | Tlambda _ | TDataCons _ | Tif _ | Tat _
| TCoerce _ | TCoerceE _ | TUpdate _ | Tunion _ | Tinter _
- | Tcomprehension _ | Trange _ | Tlet _ | TLogic_coerce _ ->
+ | Tcomprehension _ | Trange _ | Tlet _ | TLogic_coerce _ ->
(* potential sub-term inside *)
Cil.DoChildren
method !vlogic_label _ = Cil.SkipChildren
@@ -343,11 +345,11 @@ module rec Transfer
(* potential RTE *)
state_ref := register_term kf !state_ref t;
Cil.DoChildren
- | TVar _ | TResult _ ->
+ | TVar _ | TResult _ ->
Cil.SkipChildren
end
-let register_predicate kf pred state =
+let register_predicate kf pred state =
let state_ref = ref state in
Error.handle
(fun () ->
@@ -356,11 +358,11 @@ let register_predicate kf pred state =
();
!state_ref
- let register_code_annot kf a state =
+ let register_code_annot kf a state =
let state_ref = ref state in
Error.handle
(fun () ->
- ignore
+ ignore
(Visitor.visitFramacCodeAnnotation (register_object kf state_ref) a))
();
!state_ref
@@ -371,7 +373,7 @@ let register_predicate kf pred state =
List.fold_left (fun state (_, init) -> do_init vi init state) state l
let register_initializers state =
- let do_one vi init state = match init.init with
+ let do_one vi init state = match init.init with
| None -> state
| Some init -> do_init vi init state
in
@@ -387,37 +389,37 @@ let register_predicate kf pred state =
let doStmt stmt =
let _, kf = Kernel_function.find_from_sid stmt.sid in
let is_first =
- try Stmt.equal stmt (Kernel_function.find_first_stmt kf)
+ try Stmt.equal stmt (Kernel_function.find_first_stmt kf)
with Kernel_function.No_Statement -> assert false
in
let is_last =
- try Stmt.equal stmt (Kernel_function.find_return kf)
+ try Stmt.equal stmt (Kernel_function.find_return kf)
with Kernel_function.No_Statement -> assert false
in
- Dataflow.Post
+ Dataflow.Post
(fun state ->
let state = Env.default_varinfos state in
- let state =
- if (is_first || is_last) && Misc.is_generated_kf kf then
+ let state =
+ if (is_first || is_last) && Misc.is_generated_kf kf then
Annotations.fold_behaviors
- (fun _ bhv s ->
+ (fun _ bhv s ->
let handle_annot test f s =
- if test then
+ if test then
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
+ handle_annot
+ is_last
(fun f -> Annotations.fold_ensures (fun e (_, p) -> f e p)) s)
kf
state
else
state
in
- let state =
+ let state =
Annotations.fold_code_annot
(fun _ -> register_code_annot kf) stmt state
in
@@ -426,14 +428,14 @@ let register_predicate kf pred state =
let rtes = Rte.stmt kf stmt in
List.fold_left
(fun state a -> register_code_annot kf a state) state rtes
- else
+ else
state
in
let state =
(* take initializers into account *)
if is_first then
let main, lib = Globals.entry_point () in
- if Kernel_function.equal kf main && not lib then
+ if Kernel_function.equal kf main && not lib then
register_initializers state
else
state
@@ -443,82 +445,82 @@ let register_predicate kf pred state =
Some state)
let do_call res f args state =
- Env.check_heap_allocations f.vname;
let kf = Globals.Functions.get f in
- let params = Globals.Functions.get_params kf in
- let state =
- if Kernel_function.is_definition kf then
- try
- (* compute the initial state of the called function *)
- let init =
- List.fold_left2
- (fun acc p a -> match base_addr a with
- | None -> acc
- | Some vi ->
- if Varinfo.Hptset.mem vi state
- then Varinfo.Hptset.add p acc
- else acc)
- state
- params
+ Env.check_heap_allocations kf;
+ let params = Globals.Functions.get_params kf in
+ let state =
+ if Kernel_function.is_definition kf then
+ try
+ (* compute the initial state of the called function *)
+ let init =
+ List.fold_left2
+ (fun acc p a -> match base_addr a with
+ | None -> acc
+ | Some vi ->
+ if Varinfo.Hptset.mem vi state
+ then Varinfo.Hptset.add p acc
+ else acc)
+ state
+ params
args
- in
+ in
let init = match res with
- | None -> init
- | Some lv ->
- match base_addr_node (Lval lv) with
- | None -> init
- | Some vi ->
+ | None -> init
+ | Some lv ->
+ match base_addr_node (Lval lv) with
+ | None -> init
+ | Some vi ->
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
- (* compute the resulting state by keeping arguments whenever the
- corresponding formals must be kept *)
- List.fold_left2
- (fun acc p a -> match base_addr a with
- | None -> acc
- | Some vi ->
- if Varinfo.Hptset.mem p state then Varinfo.Hptset.add vi acc
- else acc)
- state
- params
+ then Varinfo.Hptset.add (Misc.result_vi kf) init
+ else init
+ in
+ let state = Compute.get ~init kf in
+ (* compute the resulting state by keeping arguments whenever the
+ corresponding formals must be kept *)
+ List.fold_left2
+ (fun acc p a -> match base_addr a with
+ | None -> acc
+ | Some vi ->
+ if Varinfo.Hptset.mem p state then Varinfo.Hptset.add vi acc
+ else acc)
+ state
+ params
args
with Invalid_argument _ ->
- Options.warning ~current:true
+ Options.warning ~current:true
"ignoring effect of variadic function %a"
- Kernel_function.pretty
- kf;
- state
- else
- state
- in
+ Kernel_function.pretty
+ kf;
+ state
+ else
+ state
+ in
let state = match res, 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
+ | 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
+ match lhost with
+ | Var vi -> Varinfo.Hptset.add vi state
| Mem e ->
- match base_addr e with
- | None -> state
- | Some vi -> Varinfo.Hptset.add vi state
- else
- state
- in
- Dataflow.Done (Some state)
+ match base_addr e with
+ | None -> state
+ | Some vi -> Varinfo.Hptset.add vi state
+ else
+ state
+ in
+ Dataflow.Done (Some state)
(** The (backwards) transfer function for an instruction. 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 doInstr _stmt instr state =
+ let doInstr _stmt instr state =
let state = Env.default_varinfos state in
match instr with
- | Set(lv, e, _) ->
+ | Set(lv, e, _) ->
let state = handle_assignment state lv e in
Dataflow.Done (Some state)
| Local_init(v,AssignInit i,_) ->
@@ -535,13 +537,13 @@ let register_predicate kf pred state =
Options.warning ~current:true
"function pointers may introduce too limited instrumentation.";
(* imprecise function call: keep each argument *)
- Dataflow.Done
+ Dataflow.Done
(Some
(List.fold_left
(fun acc e -> match base_addr e with
| None -> acc
| Some vi -> Varinfo.Hptset.add vi acc)
- state
+ state
l)))
| Asm _ -> Error.not_yet "asm"
| Skip _ | Code_annot _ -> Dataflow.Default
@@ -556,20 +558,20 @@ let register_predicate kf pred state =
Stmts_graph.stmt_can_reach kf], where [kf] is the kernel_function
being analyzed; [let stmt_can_reach _ _ = true] is also correct,
albeit less efficient *)
- let stmt_can_reach stmt =
+ let stmt_can_reach stmt =
let _, kf = Kernel_function.find_from_sid stmt.sid in
Stmts_graph.stmt_can_reach kf stmt
end
-and Compute: sig
- val get: ?init:Varinfo.Hptset.t -> kernel_function -> Varinfo.Hptset.t
+and Compute: sig
+ val get: ?init:Varinfo.Hptset.t -> kernel_function -> Varinfo.Hptset.t
end = struct
module D = Dataflow.Backwards(Transfer)
- let compute init_set kf =
- Options.feedback ~dkey ~level:2 "entering in function %a."
+ let compute init_set kf =
+ 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, is_init =
@@ -581,16 +583,16 @@ end = struct
(try
let fundec = Kernel_function.get_definition kf in
let stmts, returns = Dataflow.find_stmts fundec in
- if is_init then
+ if is_init then
Extlib.may
- (fun set ->
- List.iter
- (fun s ->
- let old =
- try Extlib.the (Stmt.Hashtbl.find tbl s)
+ (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
+ Stmt.Hashtbl.replace
tbl
s
(Some (Varinfo.Hptset.union set old)))
@@ -599,14 +601,14 @@ end = struct
else begin
List.iter (fun s -> Stmt.Hashtbl.add tbl s None) stmts;
Extlib.may
- (fun set ->
+ (fun set ->
List.iter (fun s -> Stmt.Hashtbl.replace tbl s (Some set)) returns)
init_set
end;
D.compute stmts
- with Kernel_function.No_Definition | Kernel_function.No_Statement ->
+ with Kernel_function.No_Definition | Kernel_function.No_Statement ->
());
- Options.feedback ~dkey ~level:2 "function %a done."
+ Options.feedback ~dkey ~level:2 "function %a done."
Kernel_function.pretty kf;
tbl
@@ -617,22 +619,22 @@ end = struct
try
let stmt = Kernel_function.find_first_stmt kf in
(* Options.feedback "GETTING %a" Kernel_function.pretty kf;*)
- let tbl =
+ let tbl =
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
+ Env.apply (compute init) kf
end
in
try
let set = Stmt.Hashtbl.find tbl stmt in
Env.default_varinfos set
with Not_found ->
- Options.fatal "[pre_analysis] stmt never analyzed: %a"
+ Options.fatal "[pre_analysis] stmt never analyzed: %a"
Printer.pp_stmt stmt
- with Kernel_function.No_Statement ->
+ with Kernel_function.No_Statement ->
Varinfo.Hptset.empty
end
@@ -671,17 +673,17 @@ let must_model_vi ?kf ?stmt vi =
| Some _, None ->
assert false
| Some stmt, Some kf ->
- if not (Env.is_consolidated ()) then
+ if not (Env.is_consolidated ()) then
ignore (consolidated_must_model_vi vi);
try
let tbl = Env.find kf in
try
let set = Stmt.Hashtbl.find tbl stmt in
Varinfo.Hptset.mem vi (Env.default_varinfos set)
- with Not_found ->
+ with Not_found ->
(* new statement *)
consolidated_must_model_vi vi
- with Not_found ->
+ with Not_found ->
(* [kf] is dead code *)
false
*)
@@ -692,15 +694,15 @@ let rec must_model_lval ?kf ?stmt = function
and must_model_exp ?kf ?stmt e = match e.enode with
| Lval lv | AddrOf lv | StartOf lv -> must_model_lval ?kf ?stmt lv
| BinOp((PlusPI | IndexPI | MinusPI), e1, _, _) -> must_model_exp ?kf ?stmt e1
- | BinOp(MinusPP, e1, e2, _) ->
+ | BinOp(MinusPP, e1, e2, _) ->
must_model_exp ?kf ?stmt e1 || must_model_exp ?kf ?stmt e2
| Info(e, _) | CastE(_, e) -> must_model_exp ?kf ?stmt e
- | BinOp((PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt
+ | BinOp((PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt
| Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr),
_, _, _)
| Const _ -> (* possible in case of static address *) false
- | UnOp _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _
- | AlignOfE _ ->
+ | UnOp _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _
+ | AlignOfE _ ->
Options.fatal "[pre_analysis] unexpected expression %a" Exp.pretty e
let must_model_vi ?kf ?stmt vi =
@@ -709,7 +711,7 @@ let must_model_vi ?kf ?stmt vi =
(Options.Full_mmodel.get ()
|| Error.generic_handle (must_model_vi ?kf ?stmt) false vi)
-let must_model_lval ?kf ?stmt lv =
+let must_model_lval ?kf ?stmt lv =
Options.Full_mmodel.get ()
|| Error.generic_handle (must_model_lval ?kf ?stmt) false lv
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
index 5c42f259ca2aeaebdb89e8e95f11408b8254a9d1..daeefeb20f4eccda8f32f813078993ed0f36feff 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
@@ -223,11 +223,14 @@ static const uint64_t static_readonly_masks [] = {
DVASSERT(((uintptr_t)_addr) % HEAP_SEGMENT == 0, \
"Heap base address %a is unaligned", _addr)
+#define DVALIDATE_MEMORY_INIT \
+ DVASSERT(mem_layout.initialized != 0, "Un-initialized shadow layout", NULL)
+
/* Debug function making sure that the order of program segments is as expected
* and that the program and the shadow segments used do not overlap. */
static void validate_memory_layout() {
/* Check that the struct holding memory layout is marked as initialized. */
- DVASSERT(mem_layout.initialized != 0, "Un-initialized shadow layout", NULL);
+ DVALIDATE_MEMORY_INIT;
/* Make sure the order of program segments is as expected, i.e.,
* top to bottom: stack -> tls -> heap -> global */
@@ -375,6 +378,7 @@ static void validate_memory_layout() {
#else
/*! \cond exclude from doxygen */
+# define DVALIDATE_MEMORY_INIT
# define DVALIDATE_SHADOW_LAYOUT
# define DVALIDATE_HEAP_ACCESS
# define DVALIDATE_STATIC_ACCESS
@@ -769,7 +773,9 @@ static size_t heap_allocation_size = 0;
* correspond to `unusable space`.
* \b WARNING: Current implementation assumes that the size of a heap segment
* does not exceed 64 bytes. */
-static void set_heap_segment(void *ptr, size_t size, size_t alloc_size, size_t init) {
+static void set_heap_segment(void *ptr, size_t size, size_t alloc_size,
+ size_t init, const char *function) {
+ DVALIDATE_MEMORY_INIT;
/* Ensure the shadowed block in on the tracked heap portion */
DVALIDATE_IS_ON_HEAP(((uintptr_t)ptr) - HEAP_SEGMENT, size);
DVALIDATE_ALIGNMENT(ptr); /* Make sure alignment is right */
@@ -820,7 +826,7 @@ static void* shadow_malloc(size_t size) {
(char*)native_aligned_alloc(HEAP_SEGMENT, alloc_size) : NULL;
if (res)
- set_heap_segment(res, size, alloc_size, 0);
+ set_heap_segment(res, size, alloc_size, 0, "malloc");
return res;
}
@@ -841,7 +847,7 @@ static void* shadow_calloc(size_t nmemb, size_t size) {
if (res) {
memset(res, 0, size);
- set_heap_segment(res, size, alloc_size, 1);
+ set_heap_segment(res, size, alloc_size, 1, "calloc");
}
return res;
@@ -856,7 +862,8 @@ static void* shadow_calloc(size_t nmemb, size_t size) {
*
* NOTE: ::unset_heap_segment assumes that `ptr` is a base address of an
* allocated heap memory block, i.e., `freeable(ptr)` evaluates to true. */
-static void unset_heap_segment(void *ptr, int init) {
+static void unset_heap_segment(void *ptr, int init, const char *function) {
+ DVALIDATE_MEMORY_INIT;
DVALIDATE_FREEABLE(((uintptr_t)ptr));
/* Base address of shadow block */
uintptr_t *base_shadow = (uintptr_t*)HEAP_SHADOW(ptr);
@@ -878,7 +885,7 @@ static void unset_heap_segment(void *ptr, int init) {
static void shadow_free(void *ptr) {
if (ptr != NULL) { /* NULL is a valid behaviour */
if (freeable(ptr)) {
- unset_heap_segment(ptr, 1);
+ unset_heap_segment(ptr, 1, "free");
native_free(ptr);
} else {
vabort("Not a start of block (%a) in free\n", ptr);
@@ -910,10 +917,10 @@ static void* shadow_realloc(void *ptr, size_t size) {
size_t old_alloc_size = ALLOC_SIZE(old_size);
/* Nullify old representation */
- unset_heap_segment(ptr, 0);
+ unset_heap_segment(ptr, 0, "realloc");
/* Set up new block shadow */
- set_heap_segment(res, size, alloc_size, 0);
+ set_heap_segment(res, size, alloc_size, 0, "realloc");
/* Move init shadow */
unsigned char* old_init_shadow = (unsigned char*)HEAP_INIT_SHADOW(ptr);
@@ -959,7 +966,7 @@ static void *shadow_aligned_alloc(size_t alignment, size_t size) {
char *res = native_aligned_alloc(alignment, size);
if (res)
- set_heap_segment(res, size, ALLOC_SIZE(size), 0);
+ set_heap_segment(res, size, ALLOC_SIZE(size), 0, "aligned_alloc");
return (void*)res;
}
@@ -980,7 +987,7 @@ static int shadow_posix_memalign(void **memptr, size_t alignment, size_t size) {
int res = native_posix_memalign(memptr, alignment, size);
if (!res) {
- set_heap_segment(*memptr, size, ALLOC_SIZE(size), 0);
+ set_heap_segment(*memptr, size, ALLOC_SIZE(size), 0, "posix_memalign");
}
return res;
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
index 2e7d6aa1674c2c8b302a45b86a119bd8eb24085b..435d9f52ff4a1f29b9acc6872f535a40264c7bd4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
@@ -1,16 +1,30 @@
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
+char *__gen_e_acsl_literal_string;
+void __e_acsl_globals_init(void)
+{
+ __gen_e_acsl_literal_string = "X=%d, t[0]=%d, t[1]=%d\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
+ sizeof("X=%d, t[0]=%d, t[1]=%d\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
+ return;
+}
+
int main(void)
{
int __retres;
int t[2];
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_globals_init();
int x = 0;
int i = 1;
t[0] = 1;
t[1] = 2;
- printf("X=%d, t[0]=%d, t[1]=%d\n",x,t[0],t[i]);
+ printf(__gen_e_acsl_literal_string,x,t[0],t[i]);
__retres = 0;
+ __e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/runtime/hidden_malloc.c b/src/plugins/e-acsl/tests/runtime/hidden_malloc.c
new file mode 100644
index 0000000000000000000000000000000000000000..a33c036ea74cbcf53c637f434e6cb2af885841de
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/hidden_malloc.c
@@ -0,0 +1,13 @@
+/* run.config
+ COMMENT: Malloc executed by a library function
+*/
+
+#include <limits.h>
+#include <stdlib.h>
+
+int main(int argc, const char **argv) {
+ /* If the second argument of `realpath` is NULL it uses malloc.
+ Make sure that memory layout has been initialized. */
+ char *cwd = realpath(".", NULL);
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_hidden_malloc.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_hidden_malloc.c
new file mode 100644
index 0000000000000000000000000000000000000000..3a2240a660f8f3d640002528d1807a02651615c7
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_hidden_malloc.c
@@ -0,0 +1,33 @@
+/* Generated by Frama-C */
+#include "stdlib.h"
+char *__gen_e_acsl_literal_string;
+/*@ assigns \result, *((char *)x_1 + (0 ..));
+ assigns \result \from *(x_0 + (0 ..)), *((char *)x_1 + (0 ..));
+ assigns *((char *)x_1 + (0 ..))
+ \from *(x_0 + (0 ..)), *((char *)x_1 + (0 ..));
+ */
+extern int ( /* missing proto */ realpath)(char const *x_0, void *x_1);
+
+void __e_acsl_globals_init(void)
+{
+ __gen_e_acsl_literal_string = ".";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("."));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
+ return;
+}
+
+int main(int argc, char const **argv)
+{
+ int __retres;
+ int tmp;
+ __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
+ __e_acsl_globals_init();
+ tmp = realpath(__gen_e_acsl_literal_string,(void *)0);
+ char *cwd = (char *)tmp;
+ __retres = 0;
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..537cc4f4abfd448619f4698b21c6de8791f80b19
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.res.oracle
@@ -0,0 +1,6 @@
+tests/runtime/hidden_malloc.c:11:[kernel] warning: Calling undeclared function realpath. Old style K&R code?
+[e-acsl] beginning translation.
+tests/runtime/hidden_malloc.c:11:[kernel] warning: Neither code nor specification for function realpath, generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
+tests/runtime/hidden_malloc.c:11:[value] warning: Completely invalid destination for assigns clause *((char *)x_1 + (0 ..)).
+ Ignoring.