From 9b68391bc40e29ab1149fb1d5c5ff371deb76ac4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 4 Sep 2020 16:34:15 +0200
Subject: [PATCH] [Eva] Removes state_import.ml and options
-eva-[save|load]-fun-state.
---
Makefile | 1 -
src/plugins/value/engine/compute_functions.ml | 7 +-
src/plugins/value/register.ml | 3 +-
src/plugins/value/utils/state_import.ml | 308 --------
src/plugins/value/utils/state_import.mli | 43 -
src/plugins/value/value_parameters.ml | 93 ---
src/plugins/value/value_parameters.mli | 9 -
tests/builtins/Longinit_sequencer.i | 4 -
tests/builtins/Longinit_sequencer.ml | 67 --
.../oracle/Longinit_sequencer.res.oracle | 733 ------------------
10 files changed, 3 insertions(+), 1265 deletions(-)
delete mode 100644 src/plugins/value/utils/state_import.ml
delete mode 100644 src/plugins/value/utils/state_import.mli
delete mode 100644 tests/builtins/Longinit_sequencer.i
delete mode 100644 tests/builtins/Longinit_sequencer.ml
delete mode 100644 tests/builtins/oracle/Longinit_sequencer.res.oracle
diff --git a/Makefile b/Makefile
index 7f7d6c9d995..31c65947753 100644
--- a/Makefile
+++ b/Makefile
@@ -899,7 +899,6 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
domains/cvalue/builtins_watchpoint \
domains/cvalue/builtins_float domains/cvalue/builtins_split \
domains/inout_domain \
- utils/state_import \
legacy/eval_terms legacy/eval_annots \
domains/powerset engine/transfer_logic \
domains/cvalue/cvalue_transfer domains/cvalue/cvalue_init \
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 6fbf9dbd503..e7d1b0f5a42 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -91,12 +91,9 @@ let post_analysis_cleanup ~aborted =
if Value_parameters.JoinResults.get () then
Db.Value.Table_By_Callstack.iter
(fun s _ -> ignore (Db.Value.get_stmt_state s));
- if not aborted then begin
+ if not aborted then
(* Keep memexec results for users that want to resume the analysis *)
- Mem_exec.cleanup_results ();
- if not (Value_parameters.SaveFunctionState.is_empty ()) then
- State_import.save_globals_state ();
- end
+ Mem_exec.cleanup_results ()
let post_analysis () =
(* Garbled mix must be dumped here -- at least before the call to
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index 1a396420b8e..00dc42fad17 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -138,8 +138,7 @@ 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.is_builtin_overridden kf ||
- Kernel_function.Set.mem kf (Value_parameters.UsePrototype.get ()) ||
- Value_parameters.LoadFunctionState.mem kf
+ Kernel_function.Set.mem kf (Value_parameters.UsePrototype.get ())
let eval_predicate ~pre ~here p =
let open Eval_terms in
diff --git a/src/plugins/value/utils/state_import.ml b/src/plugins/value/utils/state_import.ml
deleted file mode 100644
index f20c361e991..00000000000
--- a/src/plugins/value/utils/state_import.ml
+++ /dev/null
@@ -1,308 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2020 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cvalue
-open Cil_types
-
-let dkey = Value_parameters.register_category "restart"
-
-let base_cache : (int, Base.t) Hashtbl.t = Hashtbl.create 41
-let v_cache = V.Hashtbl.create 53
-
-(* Used to identify and remove escaping values from globals *)
-exception Possibly_escaping_value
-
-let import_varinfo (vi : varinfo) ~importing_value =
- try
- if Cil.isFunctionType vi.vtype then
- let kf = Globals.Functions.find_by_name vi.vname in
- Kernel_function.get_vi kf
- else begin
- let vi' = Globals.Vars.find_from_astinfo vi.vname VGlobal in
- if vi.vstorage = Static then
- Value_parameters.warning ~once:true
- "loaded state contains static variables;@ AST ordering@ \
- cannot be enforced and must be manually checked for soundness@ \
- (e.g. ensure that files are processed in the same order)";
- vi'
- end
- with Not_found ->
- (* search in the state *)
- if importing_value then begin
- (* Variable may be an escaping local value *)
- Value_parameters.warning "variable `%a' is not global, \
- possibly an escaping value; ignoring"
- Printer.pp_varinfo vi;
- raise Possibly_escaping_value
- end else
- Value_parameters.abort "global not found: `%a'"
- Printer.pp_varinfo vi
-
-let import_validity = function
- | Base.Empty | Base.Known _ | Base.Unknown _ | Base.Invalid as v -> v
- | Base.Variable { Base.weak; min_alloc; max_alloc; max_allocable } ->
- let var = Base.create_variable_validity ~weak ~min_alloc ~max_alloc in
- if Integer.equal max_allocable var.Base.max_allocable then
- Base.Variable var
- else Kernel.abort "Incompatible maximum size for variable %a vs. %a"
- Abstract_interp.Int.pretty max_allocable
- Abstract_interp.Int.pretty var.Base.max_allocable
-
-let import_base (base : Base.t) ~importing_value =
- let make_base = function
- | Base.Var (vi, _validity) ->
- Base.of_varinfo (import_varinfo vi ~importing_value)
- | Base.CLogic_Var (lv, _ty, _validity) ->
- (* Value states do not contain logic variables anyway
- (except when evaluating ACSL clauses, which is not the case here *)
- Value_parameters.fatal "importing logic variables (%a) is unsupported"
- Printer.pp_logic_var lv
- | Base.Null -> Base.null
- | Base.String (_, s) ->
- (* TODO: currently, we recreate a new string unrelated to the original
- one. This is probably not the good solution *)
- let c = match s with
- | Base.CSString s -> Const (CStr s)
- | Base.CSWstring s -> Const (CWStr s)
- in
- let e = Cil.new_exp Cil_datatype.Location.unknown c in
- Base.of_string_exp e
- | Base.Allocated (vi, deallocation, validity) ->
- Value_parameters.feedback ~dkey "recreating allocated base for alloc: `%a'"
- Printer.pp_varinfo vi;
- let new_vi = Value_util.create_new_var vi.vname vi.vtype in
- let validity = import_validity validity in
- let new_base = Base.register_allocated_var new_vi deallocation validity in
- Builtins_malloc.register_malloced_base new_base;
- new_base
- in
- let id = Base.id base in
- try
- let res = Hashtbl.find base_cache id in
- res
- with Not_found ->
- let base' = make_base base in
- Hashtbl.replace base_cache id base';
- base'
-
-let import_base_setlattice (sl : Base.SetLattice.t) ~importing_value =
- Base.SetLattice.fold (fun base acc ->
- let b' = import_base base ~importing_value in
- Base.Hptset.add b' acc
- ) sl Base.Hptset.empty
-
-let import_ival = Ival.rehash
-
-let import_map (m : Cvalue.V.M.t) =
- let add base ival m =
- let new_base = import_base base ~importing_value:true in
- let new_ival = import_ival ival in
- Cvalue.V.add new_base new_ival m
- in
- Cvalue.V.M.fold add m Cvalue.V.bottom
-
-let import_v (v : Cvalue.V.t) =
- match v with
- | Cvalue.V.Top (sl, o) ->
- Value_parameters.warning ~once:true
- "importing garbled mix, locations may have changed";
- (*let o' = import_origin o in*)
- let s = import_base_setlattice sl ~importing_value:true in
- Cvalue.V.inject_top_origin o s
- | Cvalue.V.Map m ->
- import_map m
-
-let import_v_or_uninit (vu : Cvalue.V_Or_Uninitialized.t) =
- let find v =
- try
- let res = V.Hashtbl.find v_cache v in
- res
- with Not_found ->
- let v' = import_v v
- in
- V.Hashtbl.replace v_cache v v';
- v'
- in
- try
- V_Or_Uninitialized.map find vu
- with Possibly_escaping_value ->
- (* replace variable with ESCAPINGADDR *)
- Cvalue.V_Or_Uninitialized.C_init_esc V.bottom
-
-let import_offsetmap (offsetmap : V_Offsetmap.t) =
- V_Offsetmap.map_on_values import_v_or_uninit offsetmap
-
-let import_model (state : Model.t) =
- match state with
- | Model.Bottom -> Model.bottom
- | Model.Top -> Model.top
- | Model.Map map ->
- let add base offsetmap map =
- let new_offsetmap = import_offsetmap offsetmap in
- let new_base = import_base base ~importing_value:false in
- Model.add_base new_base new_offsetmap map
- in
- Model.fold add map Model.empty_map
-
-(*and import_origin (o : Origin.t) =
- (* the "new" origin location is arbitrary, since no guarantees about the
- actual location can be given *)
- let loc = Origin.LocationSetLattice.currentloc_singleton () in
- match o with
- | Origin.Misalign_read _ -> Origin.Misalign_read loc
- | Origin.Leaf _ -> Origin.Leaf loc
- | Origin.Merge _ -> Origin.Merge loc
- | Origin.Arith _ -> Origin.Arith loc
- | Origin.Well | Origin.Unknown -> o*)
-
-let load_globals_from_file filename : Model.t =
- let ic = open_in_bin filename in
- let (state : Model.t) = Marshal.from_channel ic in
- close_in ic;
- Value_parameters.feedback ~dkey "DE-MARSHALLED STATE (before import):@.%a"
- Cvalue.Model.pretty state;
- import_model state
-
-let save_globals_to_file kf state_with_locals filename =
- Value_parameters.feedback "Saving globals state after call to function: %a"
- Kernel_function.pretty kf;
- let state = Model.filter_base Base.is_global state_with_locals in
- Value_parameters.feedback ~dkey "SAVED STATE:@.%a" Model.pretty state;
- let oc = open_out_bin filename in
- Marshal.to_channel oc state [];
- close_out oc
-
-let load_and_merge_function_state state : Model.t =
- let (kf, filename) = Value_parameters.get_LoadFunctionState () in
- Value_parameters.feedback
- "@[<hov 0>Skipping call to %a,@ loading globals state from file:@ %s@]"
- Kernel_function.pretty kf filename;
- let saved_state = load_globals_from_file filename in
- Value_parameters.debug ~dkey "LOADED STATE:@.%a"
- Cvalue.Model.pretty saved_state;
- (* warn about missing globals in the new AST, and add new globals that were
- not present before *)
- let saved_map = match saved_state with
- | Model.Map m -> m
- | _ -> assert false
- in
- let locals =
- Model.filter_base (fun base -> not (Base.is_global base)) state
- in
- let state_without_locals =
- Model.filter_base (fun base -> Base.is_global base) state
- in
- Value_parameters.debug ~dkey "Merging state with locals: %a@."
- Model.pretty locals;
- let new_globals =
- Model.filter_base
- (fun base ->
- try
- let _ = Model.find_base base saved_state in
- false (* previously existing global *)
- with
- | Not_found ->
- Value_parameters.warning "found new global variable `%a'"
- Base.pretty base;
- true (* new global *)
- ) state_without_locals
- in
- let merged_globals_state =
- Model.fold (fun new_base offsm acc ->
- Model.add_base new_base offsm acc
- ) saved_map new_globals
- in
- let map_with_globals = match merged_globals_state with
- | Model.Map m -> m
- | _ -> Value_parameters.fatal "invalid saved state: %a"
- Model.pretty saved_state
- in
- let merged_globals_and_locals =
- Model.fold (fun new_base offsm acc ->
- Model.add_base new_base offsm acc
- ) map_with_globals locals
- in
- merged_globals_and_locals
-
-let save_globals_state () : unit =
- let (kf, filename) = Value_parameters.get_SaveFunctionState () in
- let ret_stmt = Kernel_function.find_return kf in
- try
- let ret_state = Db.Value.get_stmt_state ret_stmt in
- match ret_state with
- | Model.Top ->
- Value_parameters.abort "cannot save state at return statement of %a \
- (too imprecise)" Kernel_function.pretty kf
- | Model.Bottom ->
- Value_parameters.abort "cannot save state at return statement of %a \
- (bottom)" Kernel_function.pretty kf
- | Model.Map _ -> save_globals_to_file kf ret_state filename
- with Not_found ->
- if Value_parameters.LoadFunctionState.is_set () then
- let (load_kf, _) = Value_parameters.get_LoadFunctionState () in
- Value_parameters.abort "could not find saved state for function `%a';@ \
- this can happen if it is called from `%a'"
- Kernel_function.pretty kf Kernel_function.pretty load_kf;
- else
- Value_parameters.failure "could not find saved state for function `%a'"
- Kernel_function.pretty kf
-
-
-exception Warn_local_addresses
-(* visitor used by frama_c_load_state *)
-class locals_visitor = object(_self) inherit Visitor.frama_c_inplace
- method! vlval (lhost, _) =
- match lhost with
- | Var vi ->
- if not vi.vglob then raise Warn_local_addresses;
- Cil.DoChildren
- | Mem _ -> Cil.DoChildren
-end
-
-
-(* Builtin to load a saved analysis state *)
-let frama_c_load_state state actuals =
- (* Warn if arguments contain pointers to local variables,
- in which case the loaded state may be unsound. *)
- begin
- try
- List.iter (fun (exp_arg, arg, _) ->
- let vis = new locals_visitor in
- if Cil.isPointerType (Cil.typeOf exp_arg) then
- ignore (Visitor.visitFramacExpr vis exp_arg);
- if Cvalue.V.contains_addresses_of_any_locals arg then
- raise Warn_local_addresses
- ) actuals;
- with Warn_local_addresses ->
- Value_parameters.warning ~current:true ~once:true
- "arguments to loaded function state contain local addresses,@ \
- possible unsoundness";
- end;
- let merged_loaded_state = load_and_merge_function_state state in
- {
- Value_types.c_values = [None, merged_loaded_state];
- c_clobbered = Base.SetLattice.empty;
- c_cacheable = Value_types.NoCacheCallers;
- c_from = None
- }
-
-let () = Builtins.register_builtin "Frama_C_load_state" frama_c_load_state
diff --git a/src/plugins/value/utils/state_import.mli b/src/plugins/value/utils/state_import.mli
deleted file mode 100644
index b1c140858e2..00000000000
--- a/src/plugins/value/utils/state_import.mli
+++ /dev/null
@@ -1,43 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2020 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(** Saving/loading of Value states, possibly among different ASTs.
- Used by the command-line options defined by
- [Value_parameters.SaveFunctionState] and
- [Value_parameters.LoadFunctionState].
- @since Aluminium-20160501 *)
-
-(** Loads the saved initial global state, and merges it with the given state
- (locals plus new globals which were not present in the original AST).
- The saved state may come from a different project.
- Note that, to ensure soundness of the merge, some constraints must be
- respected according to where the merge takes place.
- The intended use is to replace costly function calls, in which case
- the state of local variables should not be modified by the function. *)
-val load_and_merge_function_state: Cvalue.Model.t -> Cvalue.Model.t
-
-(** Saves the final state of globals variables after the return statement of
- the function defined via [Value_parameters.SaveFunctionState]. The result
- is saved in the file defined by the same option.
- The function must have been called exactly once during the value analysis,
- otherwise the saved state is unspecified. *)
-val save_globals_state: unit -> unit
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index f3bd9c4baed..97e54167787 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -1035,99 +1035,6 @@ let () = add_precision_dep ArrayPrecisionLevel.parameter
let () = ArrayPrecisionLevel.add_update_hook
(fun _ v -> Offsetmap.set_plevel v)
-(* Options SaveFunctionState and LoadFunctionState are related
- and mutually dependent for sanity checking.
- Also, they depend on BuiltinsOverrides, so they cannot be defined before it. *)
-let () = Parameter_customize.set_group initial_context
-let () = Parameter_customize.is_invisible ()
-module SaveFunctionState =
- Kernel_function_map
- (struct
- include Datatype.String
- type key = Cil_types.kernel_function
- let of_string ~key:_ ~prev:_ file = file
- let to_string ~key:_ file = file
- end)
- (struct
- let option_name = "-eva-save-fun-state"
- let arg_name = "function:filename"
- let help = "Experimental. Save state of function <function> in file <filename>"
- let default = Kernel_function.Map.empty
- end)
-let () = SaveFunctionState.add_aliases ["-val-save-fun-state"]
-let () = Parameter_customize.set_group initial_context
-let () = Parameter_customize.is_invisible ()
-module LoadFunctionState =
- Kernel_function_map
- (struct
- include Datatype.String
- type key = Cil_types.kernel_function
- let of_string ~key:_ ~prev:_ file = file
- let to_string ~key:_ file = file
- end)
- (struct
- let option_name = "-eva-load-fun-state"
- let arg_name = "function:filename"
- let help = "Experimental. Load state of function <function> from file <filename>"
- let default = Kernel_function.Map.empty
- end)
-let () = LoadFunctionState.add_aliases ["-val-load-fun-state"]
-let () = add_correctness_dep SaveFunctionState.parameter
-let () = add_correctness_dep LoadFunctionState.parameter
-(* checks that SaveFunctionState has a unique argument pair, and returns it. *)
-let get_SaveFunctionState () =
- let is_first = ref true in
- let (kf, filename) = SaveFunctionState.fold
- (fun (kf, opt_filename) _acc ->
- if !is_first then is_first := false
- else abort "option `%s' requires a single function:filename pair"
- SaveFunctionState.name;
- let filename = Extlib.the opt_filename in
- kf, filename
- ) (Kernel_function.dummy (), "")
- in
- if filename = "" then abort "option `%s' requires a function:filename pair"
- SaveFunctionState.name
- else kf, filename
-(* checks that LoadFunctionState has a unique argument pair, and returns it. *)
-let get_LoadFunctionState () =
- let is_first = ref true in
- let (kf, filename) = LoadFunctionState.fold
- (fun (kf, opt_filename) _acc ->
- if !is_first then is_first := false
- else abort "option `%s' requires a single function:filename pair"
- LoadFunctionState.name;
- let filename = Extlib.the opt_filename in
- kf, filename
- ) (Kernel_function.dummy (), "")
- in
- if filename = "" then abort "option `%s' requires a function:filename pair"
- LoadFunctionState.name
- else kf, filename
-(* perform early sanity checks to avoid aborting the analysis only at the end *)
-let () = Ast.apply_after_computed (fun _ ->
- (* check the function to save returns 'void' *)
- if SaveFunctionState.is_set () then begin
- let (kf, _) = get_SaveFunctionState () in
- if not (Kernel_function.returns_void kf) then
- abort "option `%s': function `%a' must return void"
- SaveFunctionState.name Kernel_function.pretty kf
- end;
- if SaveFunctionState.is_set () && LoadFunctionState.is_set () then begin
- (* check that if both save and load are set, they do not specify the
- same function name (note: cannot compare using function ids) *)
- let (save_kf, _) = get_SaveFunctionState () in
- let (load_kf, _) = get_LoadFunctionState () in
- if Kernel_function.equal save_kf load_kf then
- abort "options `%s' and `%s' cannot save/load the same function `%a'"
- SaveFunctionState.name LoadFunctionState.name
- Kernel_function.pretty save_kf
- end;
- if LoadFunctionState.is_set () then
- let (kf, _) = get_LoadFunctionState () in
- BuiltinsOverrides.add (kf, Some "Frama_C_load_state");
- )
-
(* ------------------------------------------------------------------------- *)
(* --- Messages --- *)
(* ------------------------------------------------------------------------- *)
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 8e5d5161ad5..6e126920273 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -91,15 +91,6 @@ module ArrayPrecisionLevel: Parameter_sig.Int
module AllocatedContextValid: Parameter_sig.Bool
module InitializationPaddingGlobals: Parameter_sig.String
-module SaveFunctionState:
- Parameter_sig.Map with type key = Cil_types.kernel_function
- and type value = string
-module LoadFunctionState:
- Parameter_sig.Map with type key = Cil_types.kernel_function
- and type value = string
-val get_SaveFunctionState : unit -> Cil_types.kernel_function * string
-val get_LoadFunctionState : unit -> Cil_types.kernel_function * string
-
module Numerors_Real_Size : Parameter_sig.Int
module Numerors_Mode : Parameter_sig.String
diff --git a/tests/builtins/Longinit_sequencer.i b/tests/builtins/Longinit_sequencer.i
deleted file mode 100644
index 919f247cf5d..00000000000
--- a/tests/builtins/Longinit_sequencer.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config*
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: @EVA_OPTIONS@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -res-file @PTEST_RESULT@
-*/
diff --git a/tests/builtins/Longinit_sequencer.ml b/tests/builtins/Longinit_sequencer.ml
deleted file mode 100644
index e08e24d518d..00000000000
--- a/tests/builtins/Longinit_sequencer.ml
+++ /dev/null
@@ -1,67 +0,0 @@
-(* Small script to test long_init*.c files, which require one test to run
- before the other. *)
-
-open Kernel
-
-include Plugin.Register
-(struct
- let name = "long init testing module"
- let shortname = "test-long-init"
- let help = "utility script for tests"
- end)
-
-module Res = String(struct
- let option_name = "-res-file"
- let help = ""
- let arg_name = "file"
- let default = "result"
- end)
-
-let ok = ref false
-
-let tmpfile () = Res.get () ^ "/Longinit_sequencer.sav"
-
-let () =
- at_exit (fun () ->
- let tmpfile = tmpfile () in
- if Debug.get () >= 1 || not !ok then
- result "Keeping temp file %s" tmpfile
- else
- try Sys.remove tmpfile with Sys_error _ -> ())
-
-let main () =
- let tmpfile = tmpfile () in
- let fmt = Format.std_formatter in
- let display_results state = Format.fprintf fmt "@[%a@]@\n" !Db.Value.display state in
- Dynamic.Parameter.String.set "" "tests/builtins/long_init.c";
- Dynamic.Parameter.String.set "-eva-save-fun-state" ("init_inner:" ^ tmpfile);
- Dynamic.Parameter.String.set "-eva-alloc-builtin" "fresh";
- Dynamic.Parameter.Bool.set "-eva-alloc-returns-null" false;
- Dynamic.Parameter.String.set "-eva-warn-key" "builtins:override=inactive";
- !Db.Value.compute ();
- Callgraph.Uses.iter_in_rev_order display_results;
- Files.clear ();
- Dynamic.Parameter.String.set "" "tests/builtins/long_init2.c";
- (* clear and set parameters to the same value to recompute
- kernel function IDs *)
- Dynamic.Parameter.String.clear "-eva-save-fun-state" ();
- Dynamic.Parameter.String.set "-eva-save-fun-state" ("init_outer:" ^ tmpfile);
- Dynamic.Parameter.String.set "-eva-load-fun-state" ("init_inner:" ^ tmpfile);
- (* set builtins in a different order to force kernel to recompute
- kernel function IDs *)
- Dynamic.Parameter.String.set "-eva-alloc-builtin" "fresh";
- !Db.Value.compute ();
- Callgraph.Uses.iter_in_rev_order display_results;
- Files.clear ();
- Dynamic.Parameter.String.set "" "tests/builtins/long_init3.c";
- Dynamic.Parameter.String.clear "-eva-save-fun-state" ();
- Dynamic.Parameter.String.clear "-eva-load-fun-state" ();
- Dynamic.Parameter.String.set "-eva-load-fun-state" ("init_outer:" ^ tmpfile);
- (* set builtins in a different order to force kernel to recompute
- kernel function IDs *)
- Dynamic.Parameter.String.set "-eva-alloc-builtin" "fresh";
- !Db.Value.compute ();
- Callgraph.Uses.iter_in_rev_order display_results;
- ok:=true (* no error, we can erase the file *)
-
-let () = Db.Main.extend main
diff --git a/tests/builtins/oracle/Longinit_sequencer.res.oracle b/tests/builtins/oracle/Longinit_sequencer.res.oracle
deleted file mode 100644
index c07049acaa7..00000000000
--- a/tests/builtins/oracle/Longinit_sequencer.res.oracle
+++ /dev/null
@@ -1,733 +0,0 @@
-[kernel] Parsing tests/builtins/Longinit_sequencer.i (no preprocessing)
-[kernel] Parsing tests/builtins/long_init.c (with preprocessing)
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva:alarm] tests/builtins/long_init.c:34: Warning:
- pointer downcast. assert (unsigned int)"abc" ≤ 127;
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- nondet ∈ [--..--]
- a1[0..9] ∈ {0}
- stuff ∈ {0}
- garbled_mix ∈ {{ "abc" }}
- s ∈ {{ "abc" }}
- pr ∈ {0}
- pr2 ∈ {0}
- pr_escaping ∈ {0}
- ppr ∈ {0}
- alloc1 ∈ {0}
- alloc2 ∈ {0}
- alloc3 ∈ {0}
- fp ∈ {{ &fun }}
- inited ∈ {0}
-[eva] computing for function init_outer <- main.
- Called from tests/builtins/long_init.c:90.
-[eva] computing for function init_inner <- init_outer <- main.
- Called from tests/builtins/long_init.c:85.
-[eva] tests/builtins/long_init.c:61: starting to merge loop iterations
-[eva] computing for function analyze <- init_inner <- init_outer <- main.
- Called from tests/builtins/long_init.c:68.
-[eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <-
- main.
- Called from tests/builtins/long_init.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <-
- main.
- Called from tests/builtins/long_init.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <-
- main.
- Called from tests/builtins/long_init.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <-
- main.
- Called from tests/builtins/long_init.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <-
- main.
- Called from tests/builtins/long_init.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] Recording results for analyze
-[eva] Done for function analyze
-[eva] computing for function analyze <- init_inner <- init_outer <- main.
- Called from tests/builtins/long_init.c:69.
-[eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
-[eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
-[eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
-[eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
-[eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <-
- main.
- Called from tests/builtins/long_init.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] Recording results for analyze
-[eva] Done for function analyze
-[eva] tests/builtins/long_init.c:73: Call to builtin malloc
-[eva] tests/builtins/long_init.c:73: allocating variable __malloc_init_inner_l73
-[eva:alarm] tests/builtins/long_init.c:74: Warning:
- pointer downcast. assert (unsigned int)alloc1 ≤ 2147483647;
-[eva] tests/builtins/long_init.c:75: Call to builtin malloc
-[eva] tests/builtins/long_init.c:75: allocating variable __malloc_init_inner_l75
-[eva] tests/builtins/long_init.c:77: Call to builtin free
-[eva] tests/builtins/long_init.c:77:
- function free: precondition 'freeable' got status valid.
-[eva:malloc] tests/builtins/long_init.c:77:
- strong free on bases: {__malloc_init_inner_l75}
-[eva] Recording results for init_inner
-[eva] Done for function init_inner
-[eva:locals-escaping] tests/builtins/long_init.c:85: Warning:
- locals {r, r2} escaping the scope of init_inner through pr
-[eva:locals-escaping] tests/builtins/long_init.c:85: Warning:
- locals {r2} escaping the scope of init_inner through pr2
-[eva:locals-escaping] tests/builtins/long_init.c:85: Warning:
- locals {r2} escaping the scope of init_inner through pr_escaping
-[eva] Recording results for init_outer
-[eva] Done for function init_outer
-[eva] tests/builtins/long_init.c:92:
- Frama_C_dump_each:
- # Cvalue domain:
- __fc_heap_status ∈ [--..--]
- __fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
- __fc_random48_init ∈ {0}
- __fc_random48_counter[0..2] ∈ [--..--]
- __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
- __fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
- [1] ∈ {{ NULL ; &S_1___fc_env[0] }}
- [2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
- __fc_mblen_state ∈ [--..--]
- __fc_mbtowc_state ∈ [--..--]
- __fc_wctomb_state ∈ [--..--]
- nondet ∈ [--..--]
- a1[0] ∈ {0}
- [1] ∈ {1}
- [2] ∈ {2}
- [3] ∈ {3}
- [4] ∈ {4}
- [5] ∈ {5}
- [6] ∈ {6}
- [7] ∈ {7}
- [8] ∈ {8}
- [9] ∈ {9}
- stuff.t[0..4] ∈ {3}
- .t[5..9] ∈ {4}
- .t[10..49] ∈ [0..12]
- .d[0] ∈ {0}
- .d[1] ∈ {3.125}
- .d[2] ∈ {6.25}
- .d[3] ∈ {9.375}
- .d[4] ∈ {12.5}
- .d[5] ∈ {15.625}
- .d[6] ∈ {18.75}
- .d[7] ∈ {21.875}
- .d[8] ∈ {25.}
- .d[9] ∈ {28.125}
- garbled_mix ∈ {{ "abc" }}
- s ∈ {{ "abc" }}
- pr ∈ ESCAPINGADDR
- pr2 ∈ ESCAPINGADDR
- pr_escaping ∈ ESCAPINGADDR
- ppr ∈ {0}
- alloc1 ∈ {{ &__malloc_init_inner_l73 }}
- alloc2 ∈ ESCAPINGADDR
- alloc3 ∈ {0}
- fp ∈ {{ &fun }}
- inited ∈ {1}
- sa ∈ {{ "abc" }}
- tmp_2 ∈ UNINITIALIZED
- __retres ∈ UNINITIALIZED
- S_0___fc_env[0..1] ∈ [--..--]
- S_1___fc_env[0..1] ∈ [--..--]
- __malloc_init_inner_l73 ∈ {{ (int)&__malloc_init_inner_l73 }}
- ==END OF DUMP==
-[eva] tests/builtins/long_init.c:93: Reusing old results for call to analyze
-[eva] tests/builtins/long_init.c:94: Reusing old results for call to analyze
-[eva] computing for function dmin <- main.
- Called from tests/builtins/long_init.c:98.
-[eva] Recording results for dmin
-[eva] Done for function dmin
-[eva] computing for function fun <- main.
- Called from tests/builtins/long_init.c:99.
-[eva] Recording results for fun
-[eva] Done for function fun
-[eva] tests/builtins/long_init.c:103: Call to builtin free
-[eva] tests/builtins/long_init.c:103:
- function free: precondition 'freeable' got status valid.
-[eva:malloc] tests/builtins/long_init.c:103:
- strong free on bases: {__malloc_init_inner_l73}
-[eva] tests/builtins/long_init.c:104: Call to builtin malloc
-[eva] tests/builtins/long_init.c:104: allocating variable __malloc_main_l104
-[eva] Recording results for main
-[eva] done for function main
-[eva] tests/builtins/long_init.c:34:
- cannot evaluate ACSL term, unsupported ACSL construct: constant strings
-[eva] Saving globals state after call to function: init_inner
-Values at end of function dmin:
- __retres ∈ [93.9166666667 .. 110.791666667]
-
-
-Values at end of function fun:
- __retres ∈ {32}
-
-
-Values at end of function subanalyze:
-
-
-Values at end of function analyze:
- i ∈ {5}
- res ∈ [93.9166666667 .. 110.791666667]
-
-Values at end of function init_inner:
- __fc_heap_status ∈ [--..--]
- a1[0] ∈ {0}
- [1] ∈ {1}
- [2] ∈ {2}
- [3] ∈ {3}
- [4] ∈ {4}
- [5] ∈ {5}
- [6] ∈ {6}
- [7] ∈ {7}
- [8] ∈ {8}
- [9] ∈ {9}
- stuff.t[0..4] ∈ {3}
- .t[5..9] ∈ {4}
- .t[10..49] ∈ [0..12]
- .d[0] ∈ {0}
- .d[1] ∈ {3.125}
- .d[2] ∈ {6.25}
- .d[3] ∈ {9.375}
- .d[4] ∈ {12.5}
- .d[5] ∈ {15.625}
- .d[6] ∈ {18.75}
- .d[7] ∈ {21.875}
- .d[8] ∈ {25.}
- .d[9] ∈ {28.125}
- pr ∈ {{ &r ; &r2 }}
- pr2 ∈ {{ &r2 }}
- pr_escaping ∈ {{ &r2 }}
- alloc1 ∈ {{ &__malloc_init_inner_l73 }}
- alloc2 ∈ ESCAPINGADDR
- i ∈ {10}
- r ∈ {93.9166666667}
- r2 ∈ {110.791666667}
- __malloc_init_inner_l73 ∈ {{ (int)&__malloc_init_inner_l73 }}
-
-Values at end of function init_outer:
- __fc_heap_status ∈ [--..--]
- a1[0] ∈ {0}
- [1] ∈ {1}
- [2] ∈ {2}
- [3] ∈ {3}
- [4] ∈ {4}
- [5] ∈ {5}
- [6] ∈ {6}
- [7] ∈ {7}
- [8] ∈ {8}
- [9] ∈ {9}
- stuff.t[0..4] ∈ {3}
- .t[5..9] ∈ {4}
- .t[10..49] ∈ [0..12]
- .d[0] ∈ {0}
- .d[1] ∈ {3.125}
- .d[2] ∈ {6.25}
- .d[3] ∈ {9.375}
- .d[4] ∈ {12.5}
- .d[5] ∈ {15.625}
- .d[6] ∈ {18.75}
- .d[7] ∈ {21.875}
- .d[8] ∈ {25.}
- .d[9] ∈ {28.125}
- pr ∈ ESCAPINGADDR
- pr2 ∈ ESCAPINGADDR
- pr_escaping ∈ ESCAPINGADDR
- alloc1 ∈ {{ &__malloc_init_inner_l73 }}
- alloc2 ∈ ESCAPINGADDR
- inited ∈ {1}
- __malloc_init_inner_l73 ∈ {{ (int)&__malloc_init_inner_l73 }}
-
-Values at end of function main:
- __fc_heap_status ∈ [--..--]
- a1[0] ∈ {0}
- [1] ∈ {1}
- [2] ∈ {2}
- [3] ∈ {3}
- [4] ∈ {4}
- [5] ∈ {5}
- [6] ∈ {6}
- [7] ∈ {7}
- [8] ∈ {8}
- [9] ∈ {9}
- stuff.t[0..4] ∈ {3}
- .t[5..9] ∈ {4}
- .t[10..49] ∈ [0..12]
- .d[0] ∈ {0}
- .d[1] ∈ {3.125}
- .d[2] ∈ {6.25}
- .d[3] ∈ {9.375}
- .d[4] ∈ {12.5}
- .d[5] ∈ {15.625}
- .d[6] ∈ {18.75}
- .d[7] ∈ {21.875}
- .d[8] ∈ {25.}
- .d[9] ∈ {28.125}
- pr ∈ {{ &r ; &r2 }}
- pr2 ∈ {{ &r ; &r2 }}
- pr_escaping ∈ ESCAPINGADDR
- ppr ∈ {{ &pr ; &pr2 }}
- alloc1 ∈ ESCAPINGADDR
- alloc2 ∈ ESCAPINGADDR
- alloc3 ∈ {{ &__malloc_main_l104 }}
- inited ∈ {1}
- sa ∈ {{ "abc" }}
- r ∈ {93.9166666667}
- r2 ∈ {110.791666667}
- dm ∈ [93.9166666667 .. 110.791666667]
- res_from_fp ∈ {32}
- res ∈ {93}
- local ∈ {1}
- __retres ∈ {0}[kernel] Parsing tests/builtins/long_init2.c (with preprocessing)
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva:alarm] tests/builtins/long_init2.c:34: Warning:
- pointer downcast. assert (unsigned int)"abc" ≤ 127;
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- nondet ∈ [--..--]
- a1[0..9] ∈ {0}
- stuff ∈ {0}
- garbled_mix ∈ {{ "abc" }}
- s ∈ {{ "abc" }}
- another_global ∈ {42}
- pr ∈ {0}
- pr2 ∈ {0}
- pr_escaping ∈ {0}
- ppr ∈ {0}
- alloc1 ∈ {0}
- alloc2 ∈ {0}
- alloc3 ∈ {0}
- fp ∈ {{ &fun }}
- inited ∈ {0}
-[eva] computing for function init_outer <- main.
- Called from tests/builtins/long_init2.c:90.
-[eva] tests/builtins/long_init2.c:85:
- Call to builtin Frama_C_load_state for function init_inner
-[eva] Skipping call to init_inner, loading globals state from file:
- tests/builtins/result/Longinit_sequencer.sav
-[eva] Warning: variable `r' is not global, possibly an escaping value; ignoring
-[eva] Warning: variable `r2' is not global, possibly an escaping value; ignoring
-[eva] Warning: variable `r2' is not global, possibly an escaping value; ignoring
-[eva] Warning: found new global variable `another_global'
-[eva] Recording results for init_outer
-[eva] Done for function init_outer
-[eva] tests/builtins/long_init2.c:92:
- Frama_C_dump_each:
- # Cvalue domain:
- __fc_heap_status ∈ [--..--]
- __fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
- __fc_random48_init ∈ {0}
- __fc_random48_counter[0..2] ∈ [--..--]
- __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
- __fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
- [1] ∈ {{ NULL ; &S_1___fc_env[0] }}
- [2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
- __fc_mblen_state ∈ [--..--]
- __fc_mbtowc_state ∈ [--..--]
- __fc_wctomb_state ∈ [--..--]
- nondet ∈ [--..--]
- a1[0] ∈ {0}
- [1] ∈ {1}
- [2] ∈ {2}
- [3] ∈ {3}
- [4] ∈ {4}
- [5] ∈ {5}
- [6] ∈ {6}
- [7] ∈ {7}
- [8] ∈ {8}
- [9] ∈ {9}
- stuff.t[0..4] ∈ {3}
- .t[5..9] ∈ {4}
- .t[10..49] ∈ [0..12]
- .d[0] ∈ {0}
- .d[1] ∈ {3.125}
- .d[2] ∈ {6.25}
- .d[3] ∈ {9.375}
- .d[4] ∈ {12.5}
- .d[5] ∈ {15.625}
- .d[6] ∈ {18.75}
- .d[7] ∈ {21.875}
- .d[8] ∈ {25.}
- .d[9] ∈ {28.125}
- garbled_mix ∈ {{ "abc" }}
- s ∈ {{ "abc" }}
- another_global ∈ {42}
- pr ∈ ESCAPINGADDR
- pr2 ∈ ESCAPINGADDR
- pr_escaping ∈ ESCAPINGADDR
- ppr ∈ {0}
- alloc1 ∈ {{ &__malloc_init_inner_l73 }}
- alloc2 ∈ ESCAPINGADDR
- alloc3 ∈ {0}
- fp ∈ {{ &fun }}
- inited ∈ {1}
- sa ∈ {{ "abc" }}
- tmp_2 ∈ UNINITIALIZED
- __retres ∈ UNINITIALIZED
- S_0___fc_env[0..1] ∈ [--..--]
- S_1___fc_env[0..1] ∈ [--..--]
- __malloc_init_inner_l73 ∈ {{ (int)&__malloc_init_inner_l73 }}
- ==END OF DUMP==
-[eva] computing for function analyze <- main.
- Called from tests/builtins/long_init2.c:93.
-[eva] computing for function subanalyze <- analyze <- main.
- Called from tests/builtins/long_init2.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] computing for function subanalyze <- analyze <- main.
- Called from tests/builtins/long_init2.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] computing for function subanalyze <- analyze <- main.
- Called from tests/builtins/long_init2.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] computing for function subanalyze <- analyze <- main.
- Called from tests/builtins/long_init2.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] computing for function subanalyze <- analyze <- main.
- Called from tests/builtins/long_init2.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] Recording results for analyze
-[eva] Done for function analyze
-[eva] computing for function analyze <- main.
- Called from tests/builtins/long_init2.c:94.
-[eva] tests/builtins/long_init2.c:29: Reusing old results for call to subanalyze
-[eva] tests/builtins/long_init2.c:29: Reusing old results for call to subanalyze
-[eva] tests/builtins/long_init2.c:29: Reusing old results for call to subanalyze
-[eva] tests/builtins/long_init2.c:29: Reusing old results for call to subanalyze
-[eva] computing for function subanalyze <- analyze <- main.
- Called from tests/builtins/long_init2.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] Recording results for analyze
-[eva] Done for function analyze
-[eva] computing for function dmin <- main.
- Called from tests/builtins/long_init2.c:98.
-[eva] Recording results for dmin
-[eva] Done for function dmin
-[eva] computing for function fun <- main.
- Called from tests/builtins/long_init2.c:99.
-[eva] Recording results for fun
-[eva] Done for function fun
-[eva] tests/builtins/long_init2.c:103: Call to builtin free
-[eva] tests/builtins/long_init2.c:103:
- function free: precondition 'freeable' got status valid.
-[eva:malloc] tests/builtins/long_init2.c:103:
- strong free on bases: {__malloc_init_inner_l73}
-[eva] tests/builtins/long_init2.c:104: Call to builtin malloc
-[eva] tests/builtins/long_init2.c:104: allocating variable __malloc_main_l104
-[eva] Recording results for main
-[eva] done for function main
-[eva] tests/builtins/long_init2.c:34:
- cannot evaluate ACSL term, unsupported ACSL construct: constant strings
-[eva] Saving globals state after call to function: init_outer
-
-
-Values at end of function dmin:
- __retres ∈ [93.9166666667 .. 110.791666667]
-
-
-Values at end of function fun:
- __retres ∈ {32}
-
-
-Values at end of function init_outer:
- a1[0] ∈ {0}
- [1] ∈ {1}
- [2] ∈ {2}
- [3] ∈ {3}
- [4] ∈ {4}
- [5] ∈ {5}
- [6] ∈ {6}
- [7] ∈ {7}
- [8] ∈ {8}
- [9] ∈ {9}
- stuff.t[0..4] ∈ {3}
- .t[5..9] ∈ {4}
- .t[10..49] ∈ [0..12]
- .d[0] ∈ {0}
- .d[1] ∈ {3.125}
- .d[2] ∈ {6.25}
- .d[3] ∈ {9.375}
- .d[4] ∈ {12.5}
- .d[5] ∈ {15.625}
- .d[6] ∈ {18.75}
- .d[7] ∈ {21.875}
- .d[8] ∈ {25.}
- .d[9] ∈ {28.125}
- pr ∈ ESCAPINGADDR
- pr2 ∈ ESCAPINGADDR
- pr_escaping ∈ ESCAPINGADDR
- alloc1 ∈ {{ &__malloc_init_inner_l73 }}
- alloc2 ∈ ESCAPINGADDR
- inited ∈ {1}
-
-
-Values at end of function subanalyze:
-
-
-Values at end of function analyze:
- i ∈ {5}
- res ∈ [93.9166666667 .. 110.791666667]
-
-Values at end of function main:
- __fc_heap_status ∈ [--..--]
- a1[0] ∈ {0}
- [1] ∈ {1}
- [2] ∈ {2}
- [3] ∈ {3}
- [4] ∈ {4}
- [5] ∈ {5}
- [6] ∈ {6}
- [7] ∈ {7}
- [8] ∈ {8}
- [9] ∈ {9}
- stuff.t[0..4] ∈ {3}
- .t[5..9] ∈ {4}
- .t[10..49] ∈ [0..12]
- .d[0] ∈ {0}
- .d[1] ∈ {3.125}
- .d[2] ∈ {6.25}
- .d[3] ∈ {9.375}
- .d[4] ∈ {12.5}
- .d[5] ∈ {15.625}
- .d[6] ∈ {18.75}
- .d[7] ∈ {21.875}
- .d[8] ∈ {25.}
- .d[9] ∈ {28.125}
- pr ∈ {{ &r ; &r2 }}
- pr2 ∈ {{ &r ; &r2 }}
- pr_escaping ∈ ESCAPINGADDR
- ppr ∈ {{ &pr ; &pr2 }}
- alloc1 ∈ ESCAPINGADDR
- alloc2 ∈ ESCAPINGADDR
- alloc3 ∈ {{ &__malloc_main_l104 }}
- inited ∈ {1}
- sa ∈ {{ "abc" }}
- r ∈ {93.9166666667}
- r2 ∈ {110.791666667}
- dm ∈ [93.9166666667 .. 110.791666667]
- res_from_fp ∈ {32}
- res ∈ {93}
- local ∈ {42}
- __retres ∈ {0}[kernel] Parsing tests/builtins/long_init3.c (with preprocessing)
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva:alarm] tests/builtins/long_init3.c:34: Warning:
- pointer downcast. assert (unsigned int)"abc" ≤ 127;
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- nondet ∈ [--..--]
- a1[0..9] ∈ {0}
- stuff ∈ {0}
- garbled_mix ∈ {{ "abc" }}
- s ∈ {{ "abc" }}
- another_global ∈ {42}
- yet_another_global ∈ {43}
- pr ∈ {0}
- pr2 ∈ {0}
- pr_escaping ∈ {0}
- ppr ∈ {0}
- alloc1 ∈ {0}
- alloc2 ∈ {0}
- alloc3 ∈ {0}
- fp ∈ {{ &fun }}
- inited ∈ {0}
-[eva] tests/builtins/long_init3.c:90:
- Call to builtin Frama_C_load_state for function init_outer
-[eva] Skipping call to init_outer, loading globals state from file:
- tests/builtins/result/Longinit_sequencer.sav
-[eva] Warning: found new global variable `yet_another_global'
-[eva] tests/builtins/long_init3.c:92:
- Frama_C_dump_each:
- # Cvalue domain:
- __fc_heap_status ∈ [--..--]
- __fc_random_counter ∈ [--..--]
- __fc_rand_max ∈ {32767}
- __fc_random48_init ∈ {0}
- __fc_random48_counter[0..2] ∈ [--..--]
- __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
- __fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
- [1] ∈ {{ NULL ; &S_1___fc_env[0] }}
- [2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
- __fc_mblen_state ∈ [--..--]
- __fc_mbtowc_state ∈ [--..--]
- __fc_wctomb_state ∈ [--..--]
- nondet ∈ [--..--]
- a1[0] ∈ {0}
- [1] ∈ {1}
- [2] ∈ {2}
- [3] ∈ {3}
- [4] ∈ {4}
- [5] ∈ {5}
- [6] ∈ {6}
- [7] ∈ {7}
- [8] ∈ {8}
- [9] ∈ {9}
- stuff.t[0..4] ∈ {3}
- .t[5..9] ∈ {4}
- .t[10..49] ∈ [0..12]
- .d[0] ∈ {0}
- .d[1] ∈ {3.125}
- .d[2] ∈ {6.25}
- .d[3] ∈ {9.375}
- .d[4] ∈ {12.5}
- .d[5] ∈ {15.625}
- .d[6] ∈ {18.75}
- .d[7] ∈ {21.875}
- .d[8] ∈ {25.}
- .d[9] ∈ {28.125}
- garbled_mix ∈ {{ "abc" }}
- s ∈ {{ "abc" }}
- another_global ∈ {42}
- yet_another_global ∈ {43}
- pr ∈ ESCAPINGADDR
- pr2 ∈ ESCAPINGADDR
- pr_escaping ∈ ESCAPINGADDR
- ppr ∈ {0}
- alloc1 ∈ {{ &__malloc_init_inner_l73 }}
- alloc2 ∈ ESCAPINGADDR
- alloc3 ∈ {0}
- fp ∈ {{ &fun }}
- inited ∈ {1}
- sa ∈ {{ "abc" }}
- tmp_2 ∈ UNINITIALIZED
- __retres ∈ UNINITIALIZED
- S_0___fc_env[0..1] ∈ [--..--]
- S_1___fc_env[0..1] ∈ [--..--]
- __malloc_init_inner_l73 ∈ {{ (int)&__malloc_init_inner_l73 }}
- ==END OF DUMP==
-[eva] computing for function analyze <- main.
- Called from tests/builtins/long_init3.c:93.
-[eva] computing for function subanalyze <- analyze <- main.
- Called from tests/builtins/long_init3.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] computing for function subanalyze <- analyze <- main.
- Called from tests/builtins/long_init3.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] computing for function subanalyze <- analyze <- main.
- Called from tests/builtins/long_init3.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] computing for function subanalyze <- analyze <- main.
- Called from tests/builtins/long_init3.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] computing for function subanalyze <- analyze <- main.
- Called from tests/builtins/long_init3.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] Recording results for analyze
-[eva] Done for function analyze
-[eva] computing for function analyze <- main.
- Called from tests/builtins/long_init3.c:94.
-[eva] tests/builtins/long_init3.c:29: Reusing old results for call to subanalyze
-[eva] tests/builtins/long_init3.c:29: Reusing old results for call to subanalyze
-[eva] tests/builtins/long_init3.c:29: Reusing old results for call to subanalyze
-[eva] tests/builtins/long_init3.c:29: Reusing old results for call to subanalyze
-[eva] computing for function subanalyze <- analyze <- main.
- Called from tests/builtins/long_init3.c:29.
-[eva] Recording results for subanalyze
-[eva] Done for function subanalyze
-[eva] Recording results for analyze
-[eva] Done for function analyze
-[eva] computing for function dmin <- main.
- Called from tests/builtins/long_init3.c:98.
-[eva] Recording results for dmin
-[eva] Done for function dmin
-[eva] computing for function fun <- main.
- Called from tests/builtins/long_init3.c:99.
-[eva] Recording results for fun
-[eva] Done for function fun
-[eva] tests/builtins/long_init3.c:103: Call to builtin free
-[eva] tests/builtins/long_init3.c:103:
- function free: precondition 'freeable' got status valid.
-[eva:malloc] tests/builtins/long_init3.c:103:
- strong free on bases: {__malloc_init_inner_l73}
-[eva] tests/builtins/long_init3.c:104: Call to builtin malloc
-[eva] tests/builtins/long_init3.c:104: allocating variable __malloc_main_l104
-[eva] Recording results for main
-[eva] done for function main
-[eva] tests/builtins/long_init3.c:34:
- cannot evaluate ACSL term, unsupported ACSL construct: constant strings
-
-
-Values at end of function dmin:
- __retres ∈ [93.9166666667 .. 110.791666667]
-
-
-Values at end of function fun:
- __retres ∈ {32}
-
-
-
-
-Values at end of function subanalyze:
-
-
-Values at end of function analyze:
- i ∈ {5}
- res ∈ [93.9166666667 .. 110.791666667]
-
-Values at end of function main:
- __fc_heap_status ∈ [--..--]
- a1[0] ∈ {0}
- [1] ∈ {1}
- [2] ∈ {2}
- [3] ∈ {3}
- [4] ∈ {4}
- [5] ∈ {5}
- [6] ∈ {6}
- [7] ∈ {7}
- [8] ∈ {8}
- [9] ∈ {9}
- stuff.t[0..4] ∈ {3}
- .t[5..9] ∈ {4}
- .t[10..49] ∈ [0..12]
- .d[0] ∈ {0}
- .d[1] ∈ {3.125}
- .d[2] ∈ {6.25}
- .d[3] ∈ {9.375}
- .d[4] ∈ {12.5}
- .d[5] ∈ {15.625}
- .d[6] ∈ {18.75}
- .d[7] ∈ {21.875}
- .d[8] ∈ {25.}
- .d[9] ∈ {28.125}
- pr ∈ {{ &r ; &r2 }}
- pr2 ∈ {{ &r ; &r2 }}
- pr_escaping ∈ ESCAPINGADDR
- ppr ∈ {{ &pr ; &pr2 }}
- alloc1 ∈ ESCAPINGADDR
- alloc2 ∈ ESCAPINGADDR
- alloc3 ∈ {{ &__malloc_main_l104 }}
- inited ∈ {1}
- sa ∈ {{ "abc" }}
- r ∈ {93.9166666667}
- r2 ∈ {110.791666667}
- dm ∈ [93.9166666667 .. 110.791666667]
- res_from_fp ∈ {32}
- res ∈ {93}
- local ∈ {42}
- local2 ∈ {43}
- __retres ∈ {0}
-
--
GitLab