diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index e88014be4f9ba107cf6e08cecf77bbd531802be6..699745967d929230091a915a67daa2544e1a648b 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -618,7 +618,8 @@ module Value = struct
(** Type for a Value builtin function *)
- type builtin_sig =
+ type builtin_type = unit -> typ * typ list
+ type builtin =
state ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
Value_types.call_result
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index fe390a2c327da09e22208efe9dafb753b104b519..b37707a8ae7b1d07f2a3d5ee08266868707eb9c0 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -177,26 +177,31 @@ module Value : sig
exception Outside_builtin_possibilities
- (** Type for a Value builtin function *)
- type builtin_sig =
- (** Memory state at the beginning of the function *)
- state ->
- (** Args for the function: the expressions corresponding to the formals
- of the functions at the call site, the actual value of those formals,
- and a more precise view of those formals using offsetmaps (for eg.
- structs) *)
- (Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
+ (* Type of a C function interpreted by a builtin:
+ return type and list of argument types. *)
+ type builtin_type = unit -> typ * typ list
+
+ (** Type for an Eva builtin function *)
+ type builtin =
+ (** Memory state at the beginning of the function *)
+ state ->
+ (** Args for the function: the expressions corresponding to the formals
+ of the functions at the call site, the actual value of those formals,
+ and a more precise view of those formals using offsetmaps (for eg.
+ structs) *)
+ (Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
Value_types.call_result
- val register_builtin: (string -> ?replace:string -> builtin_sig -> unit) ref
- (** [!register_builtin name ?replace f] registers an abstract function [f]
- to use everytime a C function named [name] is called in the program.
- If [replace] is supplied and option [-val-builtins-auto] is active,
- calls to [replace] will also be substituted by the builtin.
- See also option [-val-builtin] *)
+ val register_builtin:
+ (string -> ?replace:string -> ?typ:builtin_type -> builtin -> unit) ref
+ (** [!register_builtin name ?replace ?typ f] registers an abstract function
+ [f] to use everytime a C function named [name] of type [typ] is called in
+ the program. If [replace] is supplied and option [-eva-builtins-auto] is
+ active, calls to [replace] will also be substituted by the builtin. See
+ also option [-eva-builtin] *)
- val registered_builtins: (unit -> (string * builtin_sig) list) ref
- (** Returns a list of the pairs (name, builtin_sig) registered via
+ val registered_builtins: (unit -> (string * builtin) list) ref
+ (** Returns a list of the pairs (name, builtin) registered via
[register_builtin].
@since Aluminium-20160501 *)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/vla.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/vla.res.oracle
index f6a8b30c854998a4e78fa503c9c272011acc6c49..5a7dfb6eba881243d1482e0522cafbd61d107b3b 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/vla.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/vla.res.oracle
@@ -3,4 +3,4 @@
[eva:alarm] tests/memory/vla.c:8: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/vla.c:12: Warning:
- function __e_acsl_assert: precondition got status invalid.
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index fb2479c5e3c896d33ad478cb4d07bd459e6354d1..9a326b521900cec8f429f688eb4142702528f68c 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -30,13 +30,25 @@ exception Invalid_nb_of_args of int
if -val-builtins-auto is set. *)
type use_builtin = Always | OnAuto
+(* Table of all registered builtins; filled by [register_builtin] calls. *)
let table = Hashtbl.create 17
-let register_builtin name ?replace f =
- Hashtbl.replace table name (f, None, Always);
+(* Table binding each kernel function to their builtin for a given analysis.
+ Filled at the beginning of each analysis by [prepare_builtins]. *)
+let builtins_table = Hashtbl.create 17
+
+module Info = struct
+ let name = "Eva.Builtins.BuiltinsOverride"
+ let dependencies = [ Db.Value.self ]
+end
+(** Set of functions overridden by a builtin. *)
+module BuiltinsOverride = State_builder.Set_ref (Kernel_function.Set) (Info)
+
+let register_builtin name ?replace ?typ f =
+ Hashtbl.replace table name (f, typ, None, Always);
match replace with
| None -> ()
- | Some fname -> Hashtbl.replace table fname (f, Some name, OnAuto)
+ | Some fname -> Hashtbl.replace table fname (f, typ, Some name, OnAuto)
let () = Db.Value.register_builtin := register_builtin
@@ -45,7 +57,7 @@ let () = Db.Value.register_builtin := register_builtin
let registered_builtins () =
let l =
Hashtbl.fold
- (fun name (f, _, u) acc -> if u = Always then (name, f) :: acc else acc)
+ (fun name (f, _, _, u) acc -> if u = Always then (name, f) :: acc else acc)
table []
in
List.sort (fun (name1, _) (name2, _) -> String.compare name1 name2) l
@@ -54,7 +66,7 @@ let () = Db.Value.registered_builtins := registered_builtins
let builtin_names_and_replacements () =
let stand_alone, replacements =
- Hashtbl.fold (fun name (_, replaced_by, _) (acc1, acc2) ->
+ Hashtbl.fold (fun name (_, _, replaced_by, _) (acc1, acc2) ->
match replaced_by with
| None -> name :: acc1, acc2
| Some rep_by -> acc1, (name, rep_by) :: acc2
@@ -94,13 +106,13 @@ let () =
let mem_builtin name =
try
- let _, _, u = Hashtbl.find table name in
+ let _, _, _, u = Hashtbl.find table name in
u = Always
with Not_found -> false
let () = Db.Value.mem_builtin := mem_builtin
-(* Returns the builtin with its specification, used to evaluate preconditions
+(* Returns the specification of a builtin, used to evaluate preconditions
and to transfer the states of other domains. *)
let find_builtin_specification kf =
let spec = Annotations.funspec kf in
@@ -109,55 +121,85 @@ let find_builtin_specification kf =
TODO: check that the specification is the frama-c libc specification? *)
if spec.spec_behavior <> [] then Some spec else None
-let find_builtin_override kf =
- let name =
- try Value_parameters.BuiltinsOverrides.find kf
- with Not_found -> Kernel_function.get_name kf
+(* Returns [true] if the function [kf] is incompatible with the expected type
+ for a given builtin, which therefore cannot be applied. *)
+let inconsistent_builtin_typ kf = function
+ | None -> false (* No expected type provided with the builtin, no check. *)
+ | Some typ ->
+ let expected_result, expected_args = typ () in
+ match Kernel_function.get_type kf with
+ | TFun (result, args, _, _) ->
+ let args = Cil.argsToList args in
+ Cil.need_cast result expected_result
+ || List.length args <> List.length expected_args
+ || List.exists2 (fun (_, t, _) u -> Cil.need_cast t u) args expected_args
+ | _ -> assert false
+
+(* Warns if the builtin [bname] overrides the function definition [kf]. *)
+let warn_builtin_override kf source bname =
+ let internal =
+ (* TODO: treat this 'internal' *)
+ let file = source.Filepath.pos_path in
+ Filepath.is_relative ~base_name:Config.datadir (file :> string)
in
- try
- let f, _, u = Hashtbl.find table name in
- if u = Always || Value_parameters.BuiltinsAuto.get ()
- then Extlib.opt_map (fun s -> name, f, s) (find_builtin_specification kf)
- else None
- with Not_found -> None
+ if Kernel_function.is_definition kf && not internal
+ then
+ let fname = Kernel_function.get_name kf in
+ Value_parameters.warning ~source ~once:true
+ ~wkey:Value_parameters.wkey_builtins_override
+ "function %s: definition will be overridden by %s"
+ fname (if fname = bname then "its builtin" else "builtin " ^ bname)
-let warn_builtin_override bname kf =
+let prepare_builtin kf builtin_name builtin expected_typ =
let source = fst (Kernel_function.get_location kf) in
- if find_builtin_specification kf = None
+ if inconsistent_builtin_typ kf expected_typ
then
Value_parameters.warning ~source ~once:true
- ~wkey:Value_parameters.wkey_builtins_missing_spec
- "The builtin for function %a will not be used, as its frama-c libc \
- specification is not available."
- Kernel_function.pretty kf
+ ~wkey:Value_parameters.wkey_builtins_override
+ "The builtin %s will not be used for function %a of incompatible type.@ \
+ (got: %a)."
+ builtin_name Kernel_function.pretty kf
+ Printer.pp_typ (Kernel_function.get_type kf)
else
- let internal =
- let pos = fst (Kernel_function.get_location kf) in
- (*TODO: treat this 'internal'*)
- let file = pos.Filepath.pos_path in
- Filepath.is_relative ~base_name:Config.datadir (file :> string)
- in
- if Kernel_function.is_definition kf && not internal
- then
- let fname = Kernel_function.get_name kf in
+ match find_builtin_specification kf with
+ | None ->
Value_parameters.warning ~source ~once:true
- ~wkey:Value_parameters.wkey_builtins_override
- "function %s: definition will be overridden by %s"
- fname (if fname = bname then "its builtin" else "builtin " ^ bname)
+ ~wkey:Value_parameters.wkey_builtins_missing_spec
+ "The builtin for function %a will not be used, as its frama-c libc \
+ specification is not available."
+ Kernel_function.pretty kf
+ | Some spec ->
+ warn_builtin_override kf source builtin_name;
+ BuiltinsOverride.add kf;
+ Hashtbl.replace builtins_table kf (builtin_name, builtin, spec)
-let warn_definitions_overridden_by_builtins () =
- Value_parameters.BuiltinsOverrides.iter
- (fun (kf, name) -> warn_builtin_override (Extlib.the name) kf);
+let prepare_builtins () =
+ BuiltinsOverride.clear ();
+ Hashtbl.clear builtins_table;
let autobuiltins = Value_parameters.BuiltinsAuto.get () in
+ (* Links kernel functions to the registered builtins. *)
Hashtbl.iter
- (fun name (_, _, u) ->
+ (fun name (f, typ, _bname, u) ->
if autobuiltins || u = Always
then
try
let kf = Globals.Functions.find_by_name name in
- warn_builtin_override name kf
+ prepare_builtin kf name f typ
with Not_found -> ())
- table
+ table;
+ (* Overrides builtins attribution according to the -eva-builtin option. *)
+ Value_parameters.BuiltinsOverrides.iter
+ (fun (kf, name) ->
+ let builtin_name = Extlib.the name in
+ let f, typ, _, _ = Hashtbl.find table builtin_name in
+ prepare_builtin kf builtin_name f typ)
+
+let find_builtin_override = Hashtbl.find_opt builtins_table
+
+let is_builtin_overridden =
+ if not (BuiltinsOverride.is_computed ())
+ then prepare_builtins ();
+ BuiltinsOverride.mem
(* -------------------------------------------------------------------------- *)
(* --- Returning a clobbered set --- *)
@@ -182,7 +224,7 @@ let clobbered_set_from_ret state ret =
type call = (Precise_locs.precise_location, Cvalue.V.t) Eval.call
type result = Cvalue.Model.t * Locals_scoping.clobbered_set
-type builtin = Db.Value.builtin_sig
+type builtin = Db.Value.builtin
open Eval
diff --git a/src/plugins/value/domains/cvalue/builtins.mli b/src/plugins/value/domains/cvalue/builtins.mli
index 351bf9a11ddd32c6df1c74fbba77bbe45f1ecf6e..c7f7bc656afcddc491851817663ccc8a529450bf 100644
--- a/src/plugins/value/domains/cvalue/builtins.mli
+++ b/src/plugins/value/domains/cvalue/builtins.mli
@@ -25,28 +25,38 @@
exception Invalid_nb_of_args of int
-(** Register the given OCaml function as a builtin, that will be used
- instead of the Cil C function of the same name *)
-val register_builtin: string -> ?replace:string -> Db.Value.builtin_sig -> unit
+(** [register_builtin name ?replace ?typ f] registers the ocaml function [f]
+ as a builtin to be used instead of the C function of name [name].
+ If [replace] is provided, the builtin is also used instead of the C function
+ of name [replace], unless option -eva-builtin-auto is disabled.
+ If [typ] is provided, consistency between the expected [typ] and the type of
+ the C function is checked before using the builtin. *)
+val register_builtin:
+ string -> ?replace:string ->
+ ?typ:Db.Value.builtin_type -> Db.Value.builtin -> unit
+
+(** Prepares the builtins to be used for an analysis. Must be called at the
+ beginning of each Eva analysis. Warns about builtins of incompatible types,
+ builtins without an available specification and builtins overriding function
+ definitions. *)
+val prepare_builtins: unit -> unit
(** [clobbered_set_from_ret state ret] can be used for functions that return
a pointer to where they have written some data. It returns all the bases
of [ret] whose contents may contain local variables. *)
val clobbered_set_from_ret: Cvalue.Model.t -> Cvalue.V.t -> Base.SetLattice.t
-(** Emits warnings for each function definition that will be overridden by an
- Eva built-in.
- Does not include definitions in the Frama-C stdlib.
- @since Phosphorus-20170501-beta1 *)
-val warn_definitions_overridden_by_builtins: unit -> unit
-
type builtin
type call = (Precise_locs.precise_location, Cvalue.V.t) Eval.call
type result = Cvalue.Model.t * Locals_scoping.clobbered_set
+(** Is a given function replaced by a builtin? *)
+val is_builtin_overridden: Cil_types.kernel_function -> bool
+
(** Returns the cvalue builtin for a function, if any. Also returns the name of
the builtin and the specification of the function; the preconditions must be
- evaluated along with the builtin. *)
+ evaluated along with the builtin.
+ [prepare_builtins] should have been called before using this function. *)
val find_builtin_override:
Cil_types.kernel_function -> (string * builtin * Cil_types.funspec) option
diff --git a/src/plugins/value/domains/cvalue/builtins_float.ml b/src/plugins/value/domains/cvalue/builtins_float.ml
index 458470bfbd5d68f8ad26fab04d9ce4939cdc3369..3c28988d37d153cd207c925d78de5a611e203c4b 100644
--- a/src/plugins/value/domains/cvalue/builtins_float.ml
+++ b/src/plugins/value/domains/cvalue/builtins_float.ml
@@ -70,8 +70,9 @@ let arity2 fk caml_fun state actuals =
let register_arity2 c_name fk f =
let name = "Frama_C_" ^ c_name in
- Builtins.register_builtin name ~replace:c_name (arity2 fk f);
-;;
+ let t = Cil_types.TFloat (fk, []) in
+ let typ () = t, [t; t] in
+ Builtins.register_builtin name ~replace:c_name ~typ (arity2 fk f)
let () =
let open Fval in
@@ -80,9 +81,7 @@ let () =
register_arity2 "pow" Cil_types.FDouble pow;
register_arity2 "powf" Cil_types.FFloat pow;
register_arity2 "fmod" Cil_types.FDouble fmod;
- register_arity2 "fmodf" Cil_types.FFloat fmod;
-;;
-
+ register_arity2 "fmodf" Cil_types.FFloat fmod
let arity1 name fk caml_fun state actuals =
match actuals with
@@ -114,8 +113,9 @@ let arity1 name fk caml_fun state actuals =
let register_arity1 c_name fk f =
let name = "Frama_C_" ^ c_name in
- Builtins.register_builtin name ~replace:c_name (arity1 name fk f);
-;;
+ let t = Cil_types.TFloat (fk, []) in
+ let typ () = t, [t] in
+ Builtins.register_builtin name ~replace:c_name ~typ (arity1 name fk f)
let () =
let open Fval in
@@ -139,5 +139,4 @@ let () =
register_arity1 "floorf" Cil_types.FFloat floor;
register_arity1 "ceilf" Cil_types.FFloat ceil;
register_arity1 "truncf" Cil_types.FFloat trunc;
- register_arity1 "roundf" Cil_types.FFloat fround;
-;;
+ register_arity1 "roundf" Cil_types.FFloat fround
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index f85c0c466ee462a48d0fb8bbd14878a4890e4a62..2efd15c1339cc2ae87388ec5cebc443cd29f3b8f 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -354,8 +354,14 @@ let alloc_fresh ?(prefix="malloc") weak region state actuals =
}
| _ -> raise (Builtins.Invalid_nb_of_args 1)
-let () = Builtins.register_builtin "Frama_C_malloc_fresh" (alloc_fresh Strong Base.Malloc)
-let () = Builtins.register_builtin "Frama_C_malloc_fresh_weak" (alloc_fresh Weak Base.Malloc)
+let () =
+ Builtins.register_builtin "Frama_C_malloc_fresh"
+ (alloc_fresh Strong Base.Malloc)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
+let () =
+ Builtins.register_builtin "Frama_C_malloc_fresh_weak"
+ (alloc_fresh Weak Base.Malloc)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
let alloc_size_ok intended_size =
try
@@ -404,8 +410,14 @@ let calloc_abstract calloc_f state actuals =
let calloc_fresh weak state actuals =
calloc_abstract (alloc_abstract weak Base.Malloc) state actuals
-let () = Builtins.register_builtin "Frama_C_calloc_fresh" (calloc_fresh Strong)
-let () = Builtins.register_builtin "Frama_C_calloc_fresh_weak" (calloc_fresh Weak)
+let () =
+ Builtins.register_builtin "Frama_C_calloc_fresh" (calloc_fresh Strong)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf;
+ Cil.theMachine.Cil.typeOfSizeOf]))
+let () =
+ Builtins.register_builtin "Frama_C_calloc_fresh_weak" (calloc_fresh Weak)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf;
+ Cil.theMachine.Cil.typeOfSizeOf]))
(* Variables that have been returned by a call to an allocation function
at this callstack. The first allocated variable is at the top of the
@@ -476,7 +488,7 @@ let alloc_by_stack_aux region stack prefix sizev state =
(* For each callstack, the first MallocPrecision.get() are precise fresh
distinct locations. The following allocations all return the same
base, first strong, then weak, and which is extended as needed. *)
-let alloc_by_stack ?(prefix="malloc") region ?returns_null : Db.Value.builtin_sig = fun state actuals->
+let alloc_by_stack ?(prefix="malloc") region ?returns_null : Db.Value.builtin = fun state actuals->
let stack = call_stack_no_wrappers () in
let sizev = match actuals with
| [_,size,_] -> size
@@ -493,19 +505,24 @@ let alloc_by_stack ?(prefix="malloc") region ?returns_null : Db.Value.builtin_si
;;
let () = Builtins.register_builtin
~replace:"malloc" "Frama_C_malloc_by_stack" (alloc_by_stack Base.Malloc)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
let () = Builtins.register_builtin
~replace:"__fc_vla_alloc" "Frama_C_vla_alloc_by_stack"
(alloc_by_stack Base.VLA ~returns_null:false)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
let () = Builtins.register_builtin
~replace:"alloca" "Frama_C_alloca"
(alloc_by_stack ~prefix:"alloca" Base.Alloca ~returns_null:false)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
(* Equivalent to [alloc_by_stack], but for [calloc]. *)
-let calloc_by_stack : Db.Value.builtin_sig = fun state actuals ->
+let calloc_by_stack : Db.Value.builtin = fun state actuals ->
calloc_abstract (alloc_by_stack_aux Base.Malloc) state actuals
let () = Builtins.register_builtin
~replace:"calloc" "Frama_C_calloc_by_stack" calloc_by_stack
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf;
+ Cil.theMachine.Cil.typeOfSizeOf]))
(** {1 Free} *)
@@ -614,7 +631,9 @@ let frama_c_free state actuals =
}
| _ -> raise (Builtins.Invalid_nb_of_args 1)
-let () = Builtins.register_builtin ~replace:"free" "Frama_C_free" frama_c_free
+let () =
+ Builtins.register_builtin ~replace:"free" "Frama_C_free" frama_c_free
+ ~typ:(fun () -> (Cil.voidType, [Cil.voidPtrType]))
(* built-in for [__fc_vla_free] function. By construction, VLA should always
be mapped to a single base. *)
@@ -633,6 +652,7 @@ let frama_c_vla_free state actuals =
let () =
Builtins.register_builtin
~replace:"__fc_vla_free" "Frama_C_vla_free" frama_c_vla_free
+ ~typ:(fun () -> (Cil.voidType, [Cil.voidPtrType]))
let free_automatic_bases stack state =
(* free automatic bases that were allocated in the current function *)
@@ -792,9 +812,12 @@ let realloc ~multiple state args = match args with
let () = Builtins.register_builtin
~replace:"realloc" "Frama_C_realloc" (realloc ~multiple:false)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.voidPtrType;
+ Cil.theMachine.Cil.typeOfSizeOf]))
let () = Builtins.register_builtin
"Frama_C_realloc_multiple" (realloc ~multiple:true)
-
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.voidPtrType;
+ Cil.theMachine.Cil.typeOfSizeOf]))
(** {1 Leak detection} *)
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 21a9876322a1e7dfe27fdc0a8c9d0dc8803ce778..d5dabe47293e52f7b3a3cc6a99e7efec0b6474dd 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -76,8 +76,7 @@ let pre_analysis () =
Split_return.pretty_strategies ();
generate_specs ();
Widen.precompute_widen_hints ();
- if Value_parameters.WarnBuiltinOverride.get () then
- Builtins.warn_definitions_overridden_by_builtins ();
+ Builtins.prepare_builtins ();
Value_perf.reset ();
(* We may be resuming Value from a previously crashed analysis. Clear
degeneration states *)
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index 79b128e2dfacbad5e6c453171c1a75a3eb36bd1b..1d9d353bedde408b98f428923a4f70fc8bdc6f4b 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -52,7 +52,7 @@ let pp_p_kind fmt = function
| Assumes -> Format.pp_print_string fmt "assumes"
let post_kind kf =
- if Builtins.find_builtin_override kf <> None
+ if Builtins.is_builtin_overridden kf
then PostBuiltin
else if !Db.Value.use_spec_instead_of_definition kf then
if Kernel_function.is_definition kf
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 24d5ca59ab6a103270a9c0a266cdc8499f7c24f6..fbceb4deb4c00243c9bd0e24800039c304dbd377 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -88,7 +88,7 @@ let is_determinate kf =
warn_indeterminate kf
|| not (Kernel_function.is_definition kf (* Should we keep this? *)
|| (name >= "Frama_C" && name < "Frama_D")
- || Builtins.find_builtin_override kf <> None)
+ || Builtins.is_builtin_overridden kf)
(* Used to disambiguate files for Frama_C_dump_each_file directives. *)
module DumpFileCounters =
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index 6b2e67872412b52392079aef644e5f3242c5f8b9..315b56b05e9e65492b4f40c1c2e49a54632e59f3 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -75,7 +75,7 @@ let mark_unreachable () =
(* Do not mark preconditions as dead if they are not analyzed in
non-dead code. Otherwise, the consolidation does strange things. *)
if not (Value_util.skip_specifications kf) ||
- Builtins.find_builtin_override kf <> None
+ Builtins.is_builtin_overridden kf
then begin
(* Setup all precondition statuses for [kf]: maybe it has
never been called anywhere. *)
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index f8617e5ad4eb5c0b021ed543a5102af398231f72..0181dc864359153a839c4fc499db63b594993b9d 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -137,7 +137,7 @@ let find_deps_term_no_transitivity_state state t =
let use_spec_instead_of_definition kf =
not (Kernel_function.is_definition kf) ||
Ast_info.is_frama_c_builtin (Kernel_function.get_name kf) ||
- Builtins.find_builtin_override kf <> None ||
+ Builtins.is_builtin_overridden kf ||
Kernel_function.Set.mem kf (Value_parameters.UsePrototype.get ()) ||
Value_parameters.LoadFunctionState.mem kf
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index a45ba4188c1cb01f9b82d9905db9aedc45b08956..6213ef4f51156fcaffba7d0fd7c1e0a9306a9f4b 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -1313,26 +1313,6 @@ module NumerorsLogFile =
let default = ""
end)
-let () = Parameter_customize.set_group alarms
-let () = Parameter_customize.is_invisible ()
-module WarnBuiltinOverride =
- True(struct
- let option_name = "-val-warn-builtin-override"
- let help = "[DEPRECATED: use warning category key '" ^
- (wkey_name wkey_builtins_override) ^
- "' to control] Warn when Eva built-ins will override function \
- definitions"
- end)
-let () = add_correctness_dep WarnBuiltinOverride.parameter
-let () = WarnBuiltinOverride.add_update_hook
- (fun _ v ->
- warning "Option %s is deprecated. \
- Use warning category key '%a' instead"
- WarnBuiltinOverride.option_name
- pp_warn_category wkey_builtins_override;
- set_warn_status wkey_builtins_override
- (if v then Log.Wonce else Log.Winactive))
-
(* ------------------------------------------------------------------------- *)
(* --- Interpreter mode --- *)
(* ------------------------------------------------------------------------- *)
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 7ead8310a01f463bd9cd8f75d995a2ecce1af21a..00db23383f500a22b368d1c34a279ef972cd07ee 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -148,7 +148,6 @@ module PrintCallstacks: Parameter_sig.Bool
module AlarmsWarnings: Parameter_sig.Bool
module ReportRedStatuses: Parameter_sig.String
module NumerorsLogFile: Parameter_sig.String
-module WarnBuiltinOverride: Parameter_sig.Bool
module MemExecAll: Parameter_sig.Bool
diff --git a/tests/builtins/malloc-deps.i b/tests/builtins/malloc-deps.c
similarity index 82%
rename from tests/builtins/malloc-deps.i
rename to tests/builtins/malloc-deps.c
index 9c514cf7f03c9190fb7da4c1a475532387800a33..a50b7e99b2fc4190bc771320a65cedfedc6bf7de 100644
--- a/tests/builtins/malloc-deps.i
+++ b/tests/builtins/malloc-deps.c
@@ -1,15 +1,15 @@
/* run.config*
OPT: -eva @EVA_CONFIG@ -deps -calldeps -inout -slevel 5 -eva-msg-key malloc
*/
+#include <stddef.h>
//@ assigns \result \from \nothing;
-void *Frama_C_malloc_fresh(unsigned long n);
+void *Frama_C_malloc_fresh(size_t n);
//@ assigns \result \from \nothing;
-void *Frama_C_malloc_fresh_weak(unsigned long n);
+void *Frama_C_malloc_fresh_weak(size_t n);
//@ assigns \result \from \nothing;
-void *Frama_C_malloc_by_stack(unsigned long n);
+void *Frama_C_malloc_by_stack(size_t n);
volatile int v;
-
void g(int *p, int k) { p[k] = k; }
void main(int i, int j) {
diff --git a/tests/builtins/malloc-optimistic.c b/tests/builtins/malloc-optimistic.c
index bb1e66301f34a10a42e31ff8f1c745c6f25a35b2..1d1afd57f2a6609edad41df6f60d48e36328525c 100644
--- a/tests/builtins/malloc-optimistic.c
+++ b/tests/builtins/malloc-optimistic.c
@@ -1,9 +1,9 @@
/* run.config*
STDOPT: +"-slevel 30 -eva-slevel-merge-after-loop @all -eva-malloc-functions malloc -eva-memexec"
*/
-
+#include <stddef.h>
//@ assigns \result \from \nothing;
-void *malloc(unsigned long size);
+void *malloc(size_t size);
//@ assigns \nothing; frees p;
void free(void *p);
diff --git a/tests/builtins/malloc.c b/tests/builtins/malloc.c
index eb00026fa89a438de9352088d7b868c9dadfd809..c62203fa9ddc252a00f91fa13647a74520e169bf 100644
--- a/tests/builtins/malloc.c
+++ b/tests/builtins/malloc.c
@@ -1,9 +1,9 @@
/* run.config*
OPT: -eva @EVA_CONFIG@ -slevel 10 -eva-mlevel 0
*/
-
-void *Frama_C_malloc_by_stack(unsigned long i);
-void *Frama_C_malloc_fresh(unsigned long i);
+#include <stddef.h>
+void *Frama_C_malloc_by_stack(size_t i);
+void *Frama_C_malloc_fresh(size_t i);
void main(int c) {
int x;
diff --git a/tests/builtins/malloc_memexec.c b/tests/builtins/malloc_memexec.c
index 463f80de13fe6ee4dd098db987ddb42b46659c44..2a0434c008580b6802e46d28c4f5627791898dc9 100644
--- a/tests/builtins/malloc_memexec.c
+++ b/tests/builtins/malloc_memexec.c
@@ -1,12 +1,12 @@
/* run.config*
OPT: -eva @EVA_CONFIG@ -eva-memexec -deps -inout -eva-mlevel 0
*/
-
+#include <stddef.h>
//@ assigns \result;
-void *Frama_C_malloc_fresh(unsigned long n);
+void *Frama_C_malloc_fresh(size_t n);
//@ assigns \result;
-void *Frama_C_malloc_fresh_weak(unsigned long n);
+void *Frama_C_malloc_fresh_weak(size_t n);
void f(int *p, int i) {
diff --git a/tests/builtins/memexec-malloc.c b/tests/builtins/memexec-malloc.c
index 0d3b65f3862bda04111181e35de553fe3a6a68c6..13755b28f84a30df2756040668f35c799571097f 100644
--- a/tests/builtins/memexec-malloc.c
+++ b/tests/builtins/memexec-malloc.c
@@ -1,7 +1,7 @@
/* run.config*
- STDOPT: #"-eva-malloc-functions alloc,Frama_C_malloc_by_stack -eva-mlevel 0"
+ STDOPT: #"-eva-malloc-functions alloc -eva-mlevel 0"
*/
-
+#include <stdlib.h>
#define N 2000
int t[N];
@@ -12,7 +12,7 @@ void f() {
}
int *alloc() {
- return Frama_C_malloc_by_stack(4);
+ return malloc(4);
}
int *k() {
diff --git a/tests/builtins/oracle/malloc-deps.res.oracle b/tests/builtins/oracle/malloc-deps.res.oracle
index f76d408d0cf18ac435f16cdb940ff869ed9f9819..3d9d469a1915936ad60fcfe7f8589d9e44add84b 100644
--- a/tests/builtins/oracle/malloc-deps.res.oracle
+++ b/tests/builtins/oracle/malloc-deps.res.oracle
@@ -1,106 +1,106 @@
-[kernel] Parsing tests/builtins/malloc-deps.i (no preprocessing)
+[kernel] Parsing tests/builtins/malloc-deps.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
v ∈ [--..--]
-[eva] tests/builtins/malloc-deps.i:17: Call to builtin Frama_C_malloc_fresh_weak
-[eva] tests/builtins/malloc-deps.i:17:
+[eva] tests/builtins/malloc-deps.c:17: Call to builtin Frama_C_malloc_fresh_weak
+[eva] tests/builtins/malloc-deps.c:17:
allocating weak variable __malloc_w_main_l17
-[eva] tests/builtins/malloc-deps.i:21: Call to builtin Frama_C_malloc_fresh
-[eva] tests/builtins/malloc-deps.i:21: allocating variable __malloc_main_l21
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva] tests/builtins/malloc-deps.i:28: allocating variable __malloc_main_l28
+[eva] tests/builtins/malloc-deps.c:21: Call to builtin Frama_C_malloc_fresh
+[eva] tests/builtins/malloc-deps.c:21: allocating variable __malloc_main_l21
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva] tests/builtins/malloc-deps.c:28: allocating variable __malloc_main_l28
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
-[eva:alarm] tests/builtins/malloc-deps.i:13: Warning:
+ Called from tests/builtins/malloc-deps.c:29.
+[eva:alarm] tests/builtins/malloc-deps.c:13: Warning:
out of bounds write. assert \valid(p + k);
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc:weak] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc:weak] tests/builtins/malloc-deps.c:28:
marking variable `__malloc_main_l28' as weak
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31) to fit 0..63
-[eva:alarm] tests/builtins/malloc-deps.i:29: Warning:
+[eva:alarm] tests/builtins/malloc-deps.c:29: Warning:
signed overflow. assert l + v ≤ 2147483647;
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31/63) to fit 0..95
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31/95) to fit 0..127
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31/127) to fit 0..159
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31/159) to fit 0..191
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:27: starting to merge loop iterations
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:27: starting to merge loop iterations
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31/191) to fit 0..191/223
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31/223) to fit 0..191/255
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31/255) to fit 0..191/319
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
[eva] Done for function g
-[eva] tests/builtins/malloc-deps.i:28: Call to builtin Frama_C_malloc_by_stack
-[eva:malloc] tests/builtins/malloc-deps.i:28:
+[eva] tests/builtins/malloc-deps.c:28: Call to builtin Frama_C_malloc_by_stack
+[eva:malloc] tests/builtins/malloc-deps.c:28:
resizing variable `__malloc_w_main_l28' (0..31/319) to fit 0..191/319
[eva] computing for function g <- main.
- Called from tests/builtins/malloc-deps.i:29.
+ Called from tests/builtins/malloc-deps.c:29.
[eva] Recording results for g
[from] Computing for function g
[from] Done for function g
@@ -147,13 +147,13 @@
__malloc_w_main_l28[0..9] FROM v (and SELF)
[from] ====== END OF DEPENDENCIES ======
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to Frama_C_malloc_fresh_weak at tests/builtins/malloc-deps.i:17 (by main):
+[from] call to Frama_C_malloc_fresh_weak at tests/builtins/malloc-deps.c:17 (by main):
\result FROM \nothing
-[from] call to Frama_C_malloc_fresh at tests/builtins/malloc-deps.i:21 (by main):
+[from] call to Frama_C_malloc_fresh at tests/builtins/malloc-deps.c:21 (by main):
\result FROM \nothing
-[from] call to Frama_C_malloc_by_stack at tests/builtins/malloc-deps.i:28 (by main):
+[from] call to Frama_C_malloc_by_stack at tests/builtins/malloc-deps.c:28 (by main):
\result FROM \nothing
-[from] call to g at tests/builtins/malloc-deps.i:29 (by main):
+[from] call to g at tests/builtins/malloc-deps.c:29 (by main):
__malloc_w_main_l28[0..9] FROM p; k (and SELF)
[from] entry point:
__malloc_w_main_l17[0] FROM i; j (and SELF)
diff --git a/tests/builtins/oracle/memexec-malloc.res.oracle b/tests/builtins/oracle/memexec-malloc.res.oracle
index 7a3b162c3f6f516fddaf55512b9e08062052ed16..a6ebfd55f71791bbc1d1b5c62ee7a91c0b493901 100644
--- a/tests/builtins/oracle/memexec-malloc.res.oracle
+++ b/tests/builtins/oracle/memexec-malloc.res.oracle
@@ -1,8 +1,4 @@
[kernel] Parsing tests/builtins/memexec-malloc.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/builtins/memexec-malloc.c:15: Warning:
- Calling undeclared function Frama_C_malloc_by_stack. Old style K&R code?
-[kernel:annot:missing-spec] tests/builtins/memexec-malloc.c:22: Warning:
- Neither code nor specification for function Frama_C_malloc_by_stack, generating default assigns from the prototype
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -24,15 +20,13 @@
[eva] tests/builtins/memexec-malloc.c:29: Reusing old results for call to f
[eva] computing for function alloc <- main.
Called from tests/builtins/memexec-malloc.c:31.
-[eva] tests/builtins/memexec-malloc.c:15:
- Call to builtin Frama_C_malloc_by_stack
+[eva] tests/builtins/memexec-malloc.c:15: Call to builtin malloc
[eva] tests/builtins/memexec-malloc.c:15: allocating variable __malloc_main_l31
[eva] Recording results for alloc
[eva] Done for function alloc
[eva] computing for function alloc <- main.
Called from tests/builtins/memexec-malloc.c:32.
-[eva] tests/builtins/memexec-malloc.c:15:
- Call to builtin Frama_C_malloc_by_stack
+[eva] tests/builtins/memexec-malloc.c:15: Call to builtin malloc
[eva] tests/builtins/memexec-malloc.c:15: allocating variable __malloc_main_l32
[eva] Recording results for alloc
[eva] Done for function alloc
@@ -40,8 +34,7 @@
Called from tests/builtins/memexec-malloc.c:34.
[eva] computing for function alloc <- k <- main.
Called from tests/builtins/memexec-malloc.c:19.
-[eva] tests/builtins/memexec-malloc.c:15:
- Call to builtin Frama_C_malloc_by_stack
+[eva] tests/builtins/memexec-malloc.c:15: Call to builtin malloc
[eva] tests/builtins/memexec-malloc.c:15: allocating variable __malloc_k_l19
[eva] Recording results for alloc
[eva] Done for function alloc
@@ -51,8 +44,7 @@
Called from tests/builtins/memexec-malloc.c:35.
[eva] computing for function alloc <- k <- main.
Called from tests/builtins/memexec-malloc.c:19.
-[eva] tests/builtins/memexec-malloc.c:15:
- Call to builtin Frama_C_malloc_by_stack
+[eva] tests/builtins/memexec-malloc.c:15: Call to builtin malloc
[eva] tests/builtins/memexec-malloc.c:15: allocating variable __malloc_k_l19_0
[eva] Recording results for alloc
[eva] Done for function alloc
@@ -61,57 +53,60 @@
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function alloc:
- __retres ∈
- {{ &__malloc_main_l31 ; &__malloc_main_l32 ; &__malloc_k_l19 ;
- &__malloc_k_l19_0 }}
[eva:final-states] Values at end of function f:
t[0..1999] ∈ [0..1999]
i ∈ {2000}
+[eva:final-states] Values at end of function alloc:
+ __fc_heap_status ∈ [--..--]
[eva:final-states] Values at end of function k:
-
+ __fc_heap_status ∈ [--..--]
[eva:final-states] Values at end of function main:
+ __fc_heap_status ∈ [--..--]
t[0..1999] ∈ [0..1999]
p1 ∈ {{ &__malloc_main_l31 }}
p2 ∈ {{ &__malloc_main_l32 }}
p3 ∈ {{ &__malloc_k_l19 }}
p4 ∈ {{ &__malloc_k_l19_0 }}
-[from] Computing for function alloc
-[from] Computing for function Frama_C_malloc_by_stack <-alloc
-[from] Done for function Frama_C_malloc_by_stack
-[from] Done for function alloc
[from] Computing for function f
[from] Done for function f
+[from] Computing for function alloc
+[from] Computing for function malloc <-alloc
+[from] Done for function malloc
+[from] Done for function alloc
[from] Computing for function k
[from] Done for function k
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_malloc_by_stack:
- \result FROM x_0
-[from] Function alloc:
- \result FROM \nothing
[from] Function f:
t[0..1999] FROM \nothing (and SELF)
+[from] Function malloc:
+ __fc_heap_status FROM __fc_heap_status; size (and SELF)
+ \result FROM __fc_heap_status; size
+[from] Function alloc:
+ __fc_heap_status FROM __fc_heap_status (and SELF)
+ \result FROM __fc_heap_status
[from] Function k:
- \result FROM \nothing
+ __fc_heap_status FROM __fc_heap_status (and SELF)
+ \result FROM __fc_heap_status
[from] Function main:
+ __fc_heap_status FROM __fc_heap_status (and SELF)
t[0..1999] FROM \nothing (and SELF)
[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function alloc:
- tmp; __retres
-[inout] Inputs for function alloc:
- \nothing
[inout] Out (internal) for function f:
t[0..1999]; i
[inout] Inputs for function f:
\nothing
+[inout] Out (internal) for function alloc:
+ __fc_heap_status; tmp
+[inout] Inputs for function alloc:
+ __fc_heap_status
[inout] Out (internal) for function k:
- tmp
+ __fc_heap_status; tmp
[inout] Inputs for function k:
- \nothing
+ __fc_heap_status
[inout] Out (internal) for function main:
- t[0..1999]; p1; p2; p3; p4
+ __fc_heap_status; t[0..1999]; p1; p2; p3; p4
[inout] Inputs for function main:
- t[1..2]
+ __fc_heap_status; t[1..2]