diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 6eb4e0d120f666ee9cd726cf8afee6eff7c3485e..42c8dc20d699ac66a11821ad523bbf99e539a6ed 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -448,7 +448,7 @@ module Value = struct
module Call_Type_Value_Callbacks =
Hook.Build(struct
- type t = [`Builtin of Value_types.call_result | `Spec of funspec
+ type t = [`Builtin of Value_types.call_froms | `Spec of funspec
| `Def | `Memexec]
* state * (kernel_function * kinstr) list end)
;;
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 51a0b971add1479d07077ffe433626b167bf4c08..c8e280821cab3503ed58edc031b1fbdd553f4f9a 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -466,7 +466,7 @@ module Value : sig
@since Aluminium-20160501 *)
module Call_Type_Value_Callbacks:
Hook.Iter_hook with type param =
- [`Builtin of Value_types.call_result | `Spec of funspec | `Def | `Memexec]
+ [`Builtin of Value_types.call_froms | `Spec of funspec | `Def | `Memexec]
* state * callstack
diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
index c1e43ded459a6475ef5b00f4854620914fd5201a..bc84db8cf547e30944ddfa988e14dac5c7301afd 100644
--- a/src/plugins/aorai/aorai_eva_analysis.enabled.ml
+++ b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
@@ -41,7 +41,8 @@ let show_val fmt (expr, v, _) =
let show_aorai_state = "Frama_C_show_aorai_state"
-let _builtin_show_aorai_state state args =
+(*
+let builtin_show_aorai_state state args =
if not (Aorai_option.Deterministic.get()) then begin
Aorai_option.warning
~current:true "%s can only display info for deterministic automata"
@@ -62,6 +63,7 @@ let _builtin_show_aorai_state state args =
c_from = None;
c_cacheable = Value_types.Cacheable;
}
+*)
let () =
Cil_builtins.add_custom_builtin
diff --git a/src/plugins/from/callwise.ml b/src/plugins/from/callwise.ml
index 71038fdbbc65415215314d7133d10747a5dcd439..56cc98f3463583d5cd6bb977be9a75efa180f63f 100644
--- a/src/plugins/from/callwise.ml
+++ b/src/plugins/from/callwise.ml
@@ -90,9 +90,9 @@ let call_for_individual_froms (call_type, value_initial_state, call_stack) =
call_froms_stack :=
{ current_function; value_initial_state; table_for_calls } ::
!call_froms_stack
- | `Builtin { Value_types.c_from = Some (result,_) } ->
+ | `Builtin (Some (result,_)) ->
register_from result
- | `Builtin { Value_types.c_from = None } ->
+ | `Builtin None ->
let behaviors =
!Db.Value.valid_behaviors current_function value_initial_state
in
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 0a9e939486499af8718a176957bb3b8705e2997e..099219289d994a6117b4369936f3ef5502c252bc 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -606,7 +606,7 @@ module Callwise = struct
merge_call_in_local_table call_site table inout
in
match call_type with
- | `Builtin {Value_types.c_from = Some (froms,sure_out) } ->
+ | `Builtin (Some (froms,sure_out)) ->
let in_, out_ = extract_inout_from_froms froms in
let inout = {
over_inputs_if_termination = in_;
@@ -624,7 +624,7 @@ module Callwise = struct
| `Spec spec ->
let inout =compute_using_given_spec_state state spec current_function in
merge_inout inout
- | `Builtin { Value_types.c_from = None } ->
+ | `Builtin None ->
let inout = compute_using_prototype_state state current_function in
merge_inout inout
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index 4767c0a69f5de34be850afaff5f549a182cac1dd..b113962503679425d00905677711e8449f2283ca 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -27,11 +27,22 @@ exception Invalid_nb_of_args of int
exception Outside_builtin_possibilities
type builtin_type = unit -> typ * typ list
+type cacheable = Eval.cacheable
+
+type call_result = {
+ c_values:
+ (Cvalue.V_Offsetmap.t option
+ * Cvalue.Model.t)
+ list;
+ c_clobbered: Base.SetLattice.t;
+ c_cacheable: cacheable;
+ c_from: (Function_Froms.froms * Locations.Zone.t) option
+}
type builtin =
Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
- Value_types.call_result
+ call_result
(* 'Always' means the builtin will always be used to replace a function
with its name. 'OnAuto' means that the function will be replaced only
@@ -254,10 +265,8 @@ let apply_builtin builtin call state =
let name = Kernel_function.get_name call.kf in
let actuals = offsetmap_of_formals state call.arguments call.rest in
let res = compute_builtin name builtin state actuals in
- let call_stack = Value_util.call_stack () in
- Db.Value.Call_Type_Value_Callbacks.apply (`Builtin res, state, call_stack);
let clob = Locals_scoping.bottom () in
- Locals_scoping.remember_bases_with_locals clob res.Value_types.c_clobbered;
+ Locals_scoping.remember_bases_with_locals clob res.c_clobbered;
let process_one_return acc (ret, post_state) =
if Cvalue.Model.is_reachable post_state then
let state =
@@ -271,8 +280,8 @@ let apply_builtin builtin call state =
else
acc
in
- let list = List.fold_left process_one_return [] res.Value_types.c_values in
- list, res.Value_types.c_cacheable
+ let list = List.fold_left process_one_return [] res.c_values in
+ list, res.c_cacheable
(*
Local Variables:
diff --git a/src/plugins/value/domains/cvalue/builtins.mli b/src/plugins/value/domains/cvalue/builtins.mli
index 0a84df5cd32691fb6a555b2a1c317b6a4606bbd9..ec4920b758ba050744c3b426e57880d41e5ae7f1 100644
--- a/src/plugins/value/domains/cvalue/builtins.mli
+++ b/src/plugins/value/domains/cvalue/builtins.mli
@@ -27,11 +27,22 @@ exception Invalid_nb_of_args of int
exception Outside_builtin_possibilities
type builtin_type = unit -> Cil_types.typ * Cil_types.typ list
+type cacheable = Eval.cacheable
+
+type call_result = {
+ c_values:
+ (Cvalue.V_Offsetmap.t option
+ * Cvalue.Model.t)
+ list;
+ c_clobbered: Base.SetLattice.t;
+ c_cacheable: cacheable;
+ c_from: (Function_Froms.froms * Locations.Zone.t) option
+}
type builtin =
Cvalue.Model.t ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
- Value_types.call_result
+ call_result
(** [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].
@@ -69,7 +80,7 @@ val find_builtin_override:
(* Applies a cvalue builtin for the given call, in the given cvalue state. *)
val apply_builtin:
- builtin -> call -> Cvalue.Model.t -> result list * Value_types.cacheable
+ builtin -> call -> Cvalue.Model.t -> result list * cacheable
(*
diff --git a/src/plugins/value/domains/cvalue/builtins_float.ml b/src/plugins/value/domains/cvalue/builtins_float.ml
index 3981a1f063c0076ad8cb69fa80ea45d0473fb675..888c25c53f0aa3d18015e800f522f819e3f4c6f4 100644
--- a/src/plugins/value/domains/cvalue/builtins_float.ml
+++ b/src/plugins/value/domains/cvalue/builtins_float.ml
@@ -59,12 +59,12 @@ let arity2 fk caml_fun state actuals =
with Cvalue.V.Not_based_on_null ->
Cvalue.V.topify_arith_origin (V.join arg1 arg2)
in
- { Value_types.c_values =
+ { Builtins.c_values =
if V.is_bottom r then []
else [wrap_fk r fk, state ];
c_clobbered = Base.SetLattice.bottom;
c_from = None;
- c_cacheable = Value_types.Cacheable; }
+ c_cacheable = Eval.Cacheable; }
end
| _ -> raise (Builtins.Invalid_nb_of_args 2)
@@ -102,12 +102,12 @@ let arity1 name fk caml_fun state actuals =
Cvalue.V.topify_arith_origin arg
end
in
- { Value_types.c_values =
+ { Builtins.c_values =
if V.is_bottom r then []
else [wrap_fk r fk, state ];
c_clobbered = Base.SetLattice.bottom;
c_from = None;
- c_cacheable = Value_types.Cacheable; }
+ c_cacheable = Eval.Cacheable; }
end
| _ -> raise (Builtins.Invalid_nb_of_args 1)
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index 2868e1b1bfbd2f7dcd28441d173cb8f87412f716..363f33aa4c002b98681339461d04c783f4896f52 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -493,9 +493,9 @@ let register_malloc ?replace name ?returns_null prefix region =
let new_state = add_uninitialized state new_base max_alloc in
let ret = V.inject new_base Ival.zero in
let c_values = wrap_fallible_alloc ?returns_null ret state new_state in
- { Value_types.c_values = c_values ;
+ { Builtins.c_values = c_values ;
c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Value_types.NoCacheCallers;
+ c_cacheable = Eval.NoCacheCallers;
c_from = None; }
in
let name = "Frama_C_" ^ name in
@@ -547,9 +547,9 @@ let calloc_builtin state args =
let ret = V.inject base Ival.zero in
wrap_fallible_alloc ?returns_null ret state new_state
in
- { Value_types.c_values;
+ { Builtins.c_values;
c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Value_types.NoCacheCallers;
+ c_cacheable = Eval.NoCacheCallers;
c_from = None; }
let () =
@@ -653,17 +653,17 @@ let frama_c_free state actuals =
| [ _, arg, _ ] ->
let bases_to_remove, card_to_remove, _null = resolve_bases_to_free arg in
if card_to_remove = 0 then
- { Value_types.c_values = [];
+ { Builtins.c_values = [];
c_clobbered = Base.SetLattice.bottom;
c_from = None;
- c_cacheable = Value_types.Cacheable; }
+ c_cacheable = Eval.Cacheable; }
else
let strong = card_to_remove <= 1 in
let state, changed = free_aux state ~strong bases_to_remove in
- { Value_types.c_values = [None, state];
+ { Builtins.c_values = [None, state];
c_clobbered = Base.SetLattice.bottom;
c_from = Some changed;
- c_cacheable = Value_types.Cacheable;
+ c_cacheable = Eval.Cacheable;
}
| _ -> raise (Builtins.Invalid_nb_of_args 1)
@@ -678,10 +678,10 @@ let frama_c_vla_free state actuals =
| [ _, arg, _] ->
let bases_to_remove, _card_to_remove, _null = resolve_bases_to_free arg in
let state, changed = free_aux state ~strong:true bases_to_remove in
- { Value_types.c_values = [None, state];
+ { Builtins.c_values = [None, state];
c_clobbered = Base.SetLattice.bottom;
c_from = Some changed;
- c_cacheable = Value_types.Cacheable;
+ c_cacheable = Eval.Cacheable;
}
| _ -> raise (Builtins.Invalid_nb_of_args 1)
@@ -843,14 +843,14 @@ let realloc_builtin state args =
(* free old bases. *)
let new_state, changed = free_aux new_state ~strong bases in
let c_values = wrap_fallible_alloc ret state new_state in
- { Value_types.c_values;
+ { Builtins.c_values;
c_clobbered = Builtins.clobbered_set_from_ret new_state ret;
- c_cacheable = Value_types.NoCacheCallers;
+ c_cacheable = Eval.NoCacheCallers;
c_from = Some changed; }
else (* Invalid call. *)
- { Value_types.c_values = [] ;
+ { Builtins.c_values = [] ;
c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Value_types.NoCacheCallers;
+ c_cacheable = Eval.NoCacheCallers;
c_from = None; }
let () =
@@ -892,9 +892,9 @@ let check_leaked_malloced_bases state _ =
Value_util.warning_once_current "memory leak detected for %a"
Base.pretty base)
alloced_bases;
- { Value_types.c_values = [None,state] ;
+ { Builtins.c_values = [None,state] ;
c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Value_types.NoCacheCallers;
+ c_cacheable = Eval.NoCacheCallers;
c_from = None;
}
diff --git a/src/plugins/value/domains/cvalue/builtins_memory.ml b/src/plugins/value/domains/cvalue/builtins_memory.ml
index b3a237f7d07205c16d9243002a4a9eb59ddacd72..037cca4f7cf39cf720ef9df89a47904ad716a9a9 100644
--- a/src/plugins/value/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/value/domains/cvalue/builtins_memory.ml
@@ -48,11 +48,11 @@ let frama_C_is_base_aligned state actuals =
si)
x
();
- { Value_types.c_values =
+ { Builtins.c_values =
[ Eval_op.wrap_int Cvalue.V.singleton_one, state];
c_clobbered = Base.SetLattice.bottom;
c_from = None;
- c_cacheable = Value_types.Cacheable;
+ c_cacheable = Eval.Cacheable;
}
| None -> raise Found_misaligned_base
end
@@ -62,10 +62,10 @@ let frama_C_is_base_aligned state actuals =
| Found_misaligned_base
| Not_found (* from project_ival *)
| Abstract_interp.Error_Top (* from fold_i *) ->
- { Value_types.c_values = [Eval_op.wrap_int Cvalue.V.zero_or_one, state];
+ { Builtins.c_values = [Eval_op.wrap_int Cvalue.V.zero_or_one, state];
c_clobbered = Base.SetLattice.bottom;
c_from = None;
- c_cacheable = Value_types.Cacheable;
+ c_cacheable = Eval.Cacheable;
}
let () = register_builtin "Frama_C_is_base_aligned" frama_C_is_base_aligned
@@ -89,10 +89,10 @@ let frama_c_offset state actuals =
guaranteed to be an address";
Cvalue.V.top_int
in
- { Value_types.c_values = [Eval_op.wrap_size_t value, state];
+ { Builtins.c_values = [Eval_op.wrap_size_t value, state];
c_clobbered = Base.SetLattice.bottom;
c_from = None;
- c_cacheable = Value_types.Cacheable;
+ c_cacheable = Eval.Cacheable;
}
| _ -> raise (Builtins.Invalid_nb_of_args 1)
@@ -300,15 +300,15 @@ let frama_c_memcpy state actuals =
if Model.is_reachable new_state then
(* Copy at least partially succeeded (with perhaps an
alarm for some of the sizes *)
- { Value_types.c_values = [Eval_op.wrap_ptr dst_bytes, new_state];
+ { Builtins.c_values = [Eval_op.wrap_ptr dst_bytes, new_state];
c_clobbered = Builtins.clobbered_set_from_ret new_state dst_bytes;
c_from = Some(c_from, sure_zone);
- c_cacheable = Value_types.Cacheable }
+ c_cacheable = Eval.Cacheable }
else
- { Value_types.c_values = [ None, Cvalue.Model.bottom];
+ { Builtins.c_values = [ None, Cvalue.Model.bottom];
c_clobbered = Base.SetLattice.bottom;
c_from = Some(c_from, sure_zone);
- c_cacheable = Value_types.Cacheable }
+ c_cacheable = Eval.Cacheable }
in
match actuals with
| [dst; src; size] -> compute dst src size
@@ -385,10 +385,10 @@ let frama_c_memset_imprecise state dst v size =
let deps_return = deps_nth_arg 0 in
{ deps_table; deps_return }
in
- { Value_types.c_values = [Eval_op.wrap_ptr dst, new_state'];
+ { Builtins.c_values = [Eval_op.wrap_ptr dst, new_state'];
c_clobbered = Base.SetLattice.bottom;
c_from = Some(c_from,sure_zone);
- c_cacheable = Value_types.Cacheable;
+ c_cacheable = Eval.Cacheable;
}
(* let () = register_builtin "Frama_C_memset" frama_c_memset_imprecise *)
@@ -603,10 +603,10 @@ let frama_c_memset_precise state dst v (exp_size, size) =
Cvalue.Model.paste_offsetmap
~from:offsm ~dst_loc ~size:size_bits ~exact:true state
in
- { Value_types.c_values = [Eval_op.wrap_ptr dst, state'];
+ { Builtins.c_values = [Eval_op.wrap_ptr dst, state'];
c_clobbered = Base.SetLattice.bottom;
c_from = Some (c_from,dst_zone);
- c_cacheable = Value_types.Cacheable;
+ c_cacheable = Eval.Cacheable;
}
with
| Bit_utils.NoMatchingOffset -> raise (ImpreciseMemset SizeMismatch)
@@ -654,10 +654,10 @@ let frama_c_interval_split state actuals =
r := (Eval_op.wrap_int (Cvalue.V.inject_int !i), state) :: !r;
i := Int.succ !i;
done;
- { Value_types.c_values = !r;
+ { Builtins.c_values = !r;
c_clobbered = Base.SetLattice.bottom;
c_from = None;
- c_cacheable = Value_types.Cacheable;
+ c_cacheable = Eval.Cacheable;
}
| _ -> raise (Builtins.Invalid_nb_of_args 2)
end
@@ -682,10 +682,10 @@ let frama_c_ungarble state actuals =
with V.Not_based_on_null ->
V.inject_ival Ival.top
in
- { Value_types.c_values = [ Eval_op.wrap_int v, state ];
+ { Builtins.c_values = [ Eval_op.wrap_int v, state ];
c_clobbered = Base.SetLattice.bottom;
c_from = None;
- c_cacheable = Value_types.Cacheable;
+ c_cacheable = Eval.Cacheable;
}
| _ -> raise (Builtins.Invalid_nb_of_args 1)
end
diff --git a/src/plugins/value/domains/cvalue/builtins_misc.ml b/src/plugins/value/domains/cvalue/builtins_misc.ml
index 8617ae7119a1c2a89067005bbdc5ff6549b1c511..678df158bcf88aaaf7a18b6ed2129865bf6009d0 100644
--- a/src/plugins/value/domains/cvalue/builtins_misc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_misc.ml
@@ -45,10 +45,10 @@ let frama_C_assert state actuals =
state
end
in
- { Value_types.c_values = [ None, state ] ;
+ { Builtins.c_values = [ None, state ] ;
c_clobbered = Base.SetLattice.bottom;
c_from = None;
- c_cacheable = Value_types.NoCache;
+ c_cacheable = Eval.NoCache;
}
end
| _ -> raise (Builtins.Invalid_nb_of_args 1)
diff --git a/src/plugins/value/domains/cvalue/builtins_print_c.ml b/src/plugins/value/domains/cvalue/builtins_print_c.ml
index 1ac0850f13ad7937f856416fc5ea43ade0a44e74..0a9ed1a950e885de947d868f3612ed0d45b60f08 100644
--- a/src/plugins/value/domains/cvalue/builtins_print_c.ml
+++ b/src/plugins/value/domains/cvalue/builtins_print_c.ml
@@ -325,10 +325,10 @@ let pretty_state_as_c_assignments fmt state =
let frama_c_dump_assert state _actuals =
Value_parameters.result ~current:true "Frama_C_dump_assert_each called:@\n(%a)@\nEnd of Frama_C_dump_assert_each output"
pretty_state_as_c_assert state;
- { Value_types.c_values = [None, state];
+ { Builtins.c_values = [None, state];
c_clobbered = Base.SetLattice.bottom;
c_from = None;
- c_cacheable = Value_types.NoCache;
+ c_cacheable = Eval.NoCache;
}
let () = Builtins.register_builtin "Frama_C_dump_assert_each" frama_c_dump_assert
@@ -336,10 +336,10 @@ let () = Builtins.register_builtin "Frama_C_dump_assert_each" frama_c_dump_asser
let frama_c_dump_assignments state _actuals =
Value_parameters.result ~current:true "Frama_C_dump_assignment_each called:@\n%a@\nEnd of Frama_C_dump_assignment_each output"
pretty_state_as_c_assignments state;
- { Value_types.c_values = [None, state];
+ { Builtins.c_values = [None, state];
c_clobbered = Base.SetLattice.bottom;
c_from = None;
- c_cacheable = Value_types.NoCache;
+ c_cacheable = Eval.NoCache;
}
let () =
diff --git a/src/plugins/value/domains/cvalue/builtins_split.ml b/src/plugins/value/domains/cvalue/builtins_split.ml
index 57da04a6ea298c8d9f7b723ae37ed9abc5441169..026c9c1aba582fe12526c38cdc4321dfb9a30454 100644
--- a/src/plugins/value/domains/cvalue/builtins_split.ml
+++ b/src/plugins/value/domains/cvalue/builtins_split.ml
@@ -36,9 +36,9 @@ let frama_c_cardinal state actuals =
| None -> Cvalue.V.inject_int Integer.minus_one
| Some i -> Cvalue.V.inject_int i
in
- { Value_types.c_values = [Eval_op.wrap_long_long nb, state];
+ { Builtins.c_values = [Eval_op.wrap_long_long nb, state];
c_clobbered = Base.SetLattice.empty;
- c_cacheable = Value_types.Cacheable;
+ c_cacheable = Eval.Cacheable;
c_from = None;
}
end
@@ -60,9 +60,9 @@ let frama_c_min_max f state actuals =
| Some i -> Cvalue.V.inject_int i
with V.Not_based_on_null -> Cvalue.V.top_int
in
- { Value_types.c_values = [Eval_op.wrap_long_long nb, state];
+ { Builtins.c_values = [Eval_op.wrap_long_long nb, state];
c_clobbered = Base.SetLattice.empty;
- c_cacheable = Value_types.Cacheable;
+ c_cacheable = Eval.Cacheable;
c_from = None;
}
end
@@ -198,26 +198,26 @@ let aux_split f state actuals =
let states = f ~warn:true lv state max_card in
(* Add empty return *)
let states = List.map (fun state -> None, state) states in
- { Value_types.c_values = states;
+ { Builtins.c_values = states;
c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Value_types.Cacheable;
+ c_cacheable = Eval.Cacheable;
c_from = None;
}
with V.Not_based_on_null | Ival.Not_Singleton_Int ->
Value_parameters.warning ~current:true ~once:true
"Cannot use non-constant split level %a" V.pretty card;
- { Value_types.c_values = [(None, state)];
+ { Builtins.c_values = [(None, state)];
c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Value_types.Cacheable;
+ c_cacheable = Eval.Cacheable;
c_from = None;
}
end
| _ ->
Value_parameters.warning ~current:true ~once:true
"Cannot interpret split directive. Ignoring";
- { Value_types.c_values = [(None, state)];
+ { Builtins.c_values = [(None, state)];
c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Value_types.Cacheable;
+ c_cacheable = Eval.Cacheable;
c_from = None;
}
diff --git a/src/plugins/value/domains/cvalue/builtins_string.ml b/src/plugins/value/domains/cvalue/builtins_string.ml
index f5ecbc9c136338a14d037c771107aee4a1a9c3db..2bdf3bc24c443468ba1fdacc65f52e96352ccd11 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.ml
+++ b/src/plugins/value/domains/cvalue/builtins_string.ml
@@ -409,10 +409,10 @@ let apply_builtin _name builtin = fun state args ->
| None -> None, Cvalue.Model.bottom
| Some _ -> result, state
in
- { Value_types.c_values = [ res_cvalue ];
+ { Builtins.c_values = [ res_cvalue ];
c_clobbered = Base.SetLattice.bottom;
c_from = None;
- c_cacheable = Value_types.Cacheable; }
+ c_cacheable = Eval.Cacheable; }
(* Builds, registers and exports a builtin for the C function [c_name]. *)
let register_builtin c_name ~search ~stop_at_0 ~typ ~length ?limit =
diff --git a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
index d9437db43ada64475246d1141d78da3715043b33..6eb8f97c2528fdc84d8fa892989be147a4d194ef 100644
--- a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
+++ b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
@@ -76,10 +76,10 @@ let add_watch make_watch state actuals =
then
watch_table :=
(new_watchpoint dst_e loc target_w number) :: current;
- { Value_types.c_values = [None, state];
+ { Builtins.c_values = [None, state];
c_clobbered = Base.SetLattice.bottom;
c_from = None;
- c_cacheable = Value_types.Cacheable }
+ c_cacheable = Eval.Cacheable }
| _ -> raise (Builtins.Invalid_nb_of_args 4)
let make_watch_value target_value = Value target_value
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index de253c37eb857c9121e644bbc185c3defd8002e2..aa0db0be304767151c9d747d9a4f3ba7b0d5ff02 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -195,7 +195,7 @@ module Make (Abstract: Abstractions.Eva) = struct
if Cil.is_in_libc vi.vattr then
Library_functions.warn_unsupported_spec vi.vorig_name;
Spec.compute_using_specification ~warn:true call_kinstr call spec state,
- Value_types.Cacheable
+ Eval.Cacheable
| `Def _fundec ->
Db.Value.Call_Type_Value_Callbacks.apply (`Def, cvalue_state, call_stack);
Computer.compute kf call_kinstr state
@@ -221,7 +221,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let call_result = default () in
let () =
if not (!Db.Value.use_spec_instead_of_definition call.kf)
- && call_result.Transfer.cacheable = Value_types.Cacheable
+ && call_result.Transfer.cacheable = Eval.Cacheable
then
let final_states = call_result.Transfer.states in
MemExec.store_computed_call call.kf init_state args final_states
@@ -251,7 +251,7 @@ module Make (Abstract: Abstractions.Eva) = struct
Db.Value.Record_Value_Callbacks_New.apply
(stack_with_call, Value_types.Reuse i);
(* call can be cached since it was cached once *)
- Transfer.{states; cacheable = Value_types.Cacheable; builtin=false}
+ Transfer.{states; cacheable = Cacheable; builtin=false}
else
default ()
@@ -296,7 +296,7 @@ module Make (Abstract: Abstractions.Eva) = struct
| `Bottom ->
let cs = Value_util.call_stack () in
Db.Value.Call_Type_Value_Callbacks.apply (`Spec spec, cvalue_state, cs);
- let cacheable = Value_types.Cacheable in
+ let cacheable = Eval.Cacheable in
Transfer.{states; cacheable; builtin=true}
| `Value final_state ->
let cvalue_call = get_cvalue_call call in
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index a7862968059399ccb8f624c7bfe34393d633bbc4..d763e158f76d277a8fcabcd54b5100118181ffd4 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -66,7 +66,7 @@ module Make_Dataflow
let kf = AnalysisParam.kf
let fundec = Kernel_function.get_definition kf
- let cacheable = ref Value_types.Cacheable
+ let cacheable = ref Eval.Cacheable
(* --- Plugin parameters --- *)
@@ -273,9 +273,9 @@ module Make_Dataflow
let result, call_cacheable =
Transfer.call stmt dest callee args state
in
- if call_cacheable = Value_types.NoCacheCallers then
+ if call_cacheable = Eval.NoCacheCallers then
(* Propagate info that the current call cannot be cached either *)
- cacheable := Value_types.NoCacheCallers;
+ cacheable := Eval.NoCacheCallers;
Bottom.list_of_bot result
let transfer_instr (stmt : stmt) (instr : instr) : transfer_function =
diff --git a/src/plugins/value/engine/iterator.mli b/src/plugins/value/engine/iterator.mli
index 0c534749680df8d6ff9c2262595db68814092afa..2e28b637eca6c25952019411529658b034680ede 100644
--- a/src/plugins/value/engine/iterator.mli
+++ b/src/plugins/value/engine/iterator.mli
@@ -46,7 +46,7 @@ module Computer
val compute:
kernel_function -> kinstr -> Abstract.Dom.t ->
- Abstract.Dom.t list or_bottom * Value_types.cacheable
+ Abstract.Dom.t list or_bottom * Eval.cacheable
end
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 953d273cd33cae2924f0fdfe75dee013a2491739..b115d5a5e21bf0ca3a8e1966950e8f6d41abf3c6 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -32,7 +32,7 @@ module type S = sig
val assume: state -> stmt -> exp -> bool -> state or_bottom
val call:
stmt -> lval option -> exp -> exp list -> state ->
- state list or_bottom * Value_types.cacheable
+ state list or_bottom * Eval.cacheable
val check_unspecified_sequence:
stmt ->
state -> (stmt * lval list * lval list * lval list * stmt ref list) list ->
@@ -40,7 +40,7 @@ module type S = sig
val enter_scope: kernel_function -> varinfo list -> state -> state
type call_result = {
states: state list or_bottom;
- cacheable: Value_types.cacheable;
+ cacheable: Eval.cacheable;
builtin: bool;
}
val compute_call_ref:
@@ -290,7 +290,7 @@ module Make (Abstract: Abstractions.Eva) = struct
type call_result = {
states: state list or_bottom;
- cacheable: Value_types.cacheable;
+ cacheable: cacheable;
builtin: bool;
}
@@ -317,7 +317,7 @@ module Make (Abstract: Abstractions.Eva) = struct
Domain.Store.register_initial_state (Value_util.call_stack ()) state;
!compute_call_ref stmt call state
| `Bottom ->
- { states = `Bottom; cacheable = Value_types.Cacheable; builtin=false }
+ { states = `Bottom; cacheable = Cacheable; builtin=false }
in
cleanup ();
res
@@ -716,15 +716,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let cvalue_state = Domain.get_cvalue_or_top state in
Db.Value.Call_Value_Callbacks.apply (cvalue_state, stack_with_call);
Db.Value.merge_initial_state (Value_util.call_stack ()) cvalue_state;
- let result =
- { Value_types.c_values = [ None, cvalue_state] ;
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Value_types.Cacheable;
- }
- in
Db.Value.Call_Type_Value_Callbacks.apply
- (`Builtin result, cvalue_state, stack_with_call)
+ (`Builtin None, cvalue_state, stack_with_call)
(* --------------------- Process the call statement ---------------------- *)
@@ -737,7 +730,7 @@ module Make (Abstract: Abstractions.Eva) = struct
Eval.eval_function_exp ~subdivnb funcexp ~args state
in
Alarmset.emit ki_call alarms;
- let cacheable = ref Value_types.Cacheable in
+ let cacheable = ref Cacheable in
let eval =
functions >>- fun functions ->
let current_kf = Value_util.current_kf () in
@@ -757,8 +750,8 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Do the call. *)
let c, states = do_one_call valuation stmt lval_option call state in
(* If needed, propagate that callers cannot be cached. *)
- if c = Value_types.NoCacheCallers then
- cacheable := Value_types.NoCacheCallers;
+ if c = NoCacheCallers then
+ cacheable := NoCacheCallers;
states
in
(* Process each possible function apart, and append the result list. *)
diff --git a/src/plugins/value/engine/transfer_stmt.mli b/src/plugins/value/engine/transfer_stmt.mli
index 8b0055ab0f7e8afe5c7b35f0618190cabbcb0365..780607b261d8c22fc2e77211bac6742a4cfee47c 100644
--- a/src/plugins/value/engine/transfer_stmt.mli
+++ b/src/plugins/value/engine/transfer_stmt.mli
@@ -37,7 +37,7 @@ module type S = sig
val call:
stmt -> lval option -> exp -> exp list -> state ->
- state list or_bottom * Value_types.cacheable
+ state list or_bottom * Eval.cacheable
val check_unspecified_sequence:
Cil_types.stmt ->
@@ -50,7 +50,7 @@ module type S = sig
type call_result = {
states: state list or_bottom;
- cacheable: Value_types.cacheable;
+ cacheable: Eval.cacheable;
builtin: bool;
}
diff --git a/src/plugins/value/eval.ml b/src/plugins/value/eval.ml
index 6aa0b6a0fe071bb8e1af643cac64c0a5e31918fc..f9b6aa98f2ee4d835dcd7f3a2b9b605c538390cb 100644
--- a/src/plugins/value/eval.ml
+++ b/src/plugins/value/eval.ml
@@ -243,6 +243,8 @@ type ('loc, 'value) call = {
recursive: bool;
}
+type cacheable = Cacheable | NoCache | NoCacheCallers
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index b7de21de5c9b8b4e12c3e0ce40d4250965ad965d..2610008ef2f10c36619460ac5913ff6bbbb46936 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -220,6 +220,8 @@ type ('loc, 'value) call = {
recursive: bool;
}
+type cacheable = Cacheable | NoCache | NoCacheCallers
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/value_types/value_types.ml b/src/plugins/value_types/value_types.ml
index 4ad6d92e4a173af3dbd2fc44aba6e9f0baa88d3e..cee467a27fe435db0357532b394d1922c966dc6d 100644
--- a/src/plugins/value_types/value_types.ml
+++ b/src/plugins/value_types/value_types.ml
@@ -114,18 +114,7 @@ type 'a callback_result =
| NormalStore of 'a * int
| Reuse of int
-type cacheable =
- | Cacheable
- | NoCache
- | NoCacheCallers
-
-
-type call_result = {
- c_values: (Cvalue.V_Offsetmap.t option * Cvalue.Model.t) list;
- c_clobbered: Base.SetLattice.t;
- c_cacheable: cacheable;
- c_from: (Function_Froms.froms * Locations.Zone.t) option
-}
+type call_froms = (Function_Froms.froms * Locations.Zone.t) option
type logic_dependencies = Locations.Zone.t Cil_datatype.Logic_label.Map.t
diff --git a/src/plugins/value_types/value_types.mli b/src/plugins/value_types/value_types.mli
index cdd8f86c51b15e072ea718a42cf62740ba5e5143..0ea1f9edc7a41dd286d6e8e70ddd2d0a0aec2da5 100644
--- a/src/plugins/value_types/value_types.mli
+++ b/src/plugins/value_types/value_types.mli
@@ -63,37 +63,10 @@ type 'a callback_result =
| NormalStore of 'a * int
| Reuse of int
-type cacheable =
- | Cacheable (** Functions whose result can be safely cached *)
- | NoCache (** Functions whose result should not be cached, but for
- which the caller can still be cached. Typically, functions
- printing something during the analysis. *)
- | NoCacheCallers (** Functions for which neither the call, neither the
- callers, can be cached *)
-
-
-(** Results of a a call to a function *)
-type call_result = {
- c_values: (** Memory states after the call *)
- (Cvalue.V_Offsetmap.t option
- (** the value returned (ie. what is after the 'return' C keyword). *)
- * Cvalue.Model.t
- (** the memory state after the function has been executed *))
- list;
-
- c_clobbered: Base.SetLattice.t
- (** An over-approximation of the bases in which addresses of local
- variables might have been written *);
-
- c_cacheable: cacheable
- (** Is it possible to cache the result of this call? *);
-
- c_from: (Function_Froms.froms * Locations.Zone.t) option
- (** If not None, the froms of the function, and its sure outputs;
- i.e. the dependencies of the result, and the dependencies
- of each zone written to. *)
-}
-
+type call_froms = (Function_Froms.froms * Locations.Zone.t) option
+(** If not None, the froms of the function, and its sure outputs;
+ i.e. the dependencies of the result, and the dependencies
+ of each zone written to. *)
(** Dependencies for the evaluation of a term or a predicate: for each
program point involved, sets of zones that must be read *)