diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index b0c836e186176f19395425c2b1b709f87db67755..9f6972f4626c17ca89e4dfa9f547d53e5986446e 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -149,23 +149,23 @@ let () = Extlib.safe_at_exit time
(* Save Frama-c on disk if required *)
let save_binary error_extension =
if not (Kernel.SaveState.is_empty ()) then begin
- let filename = Kernel.SaveState.get () in
+ let path = Kernel.SaveState.get () in
Kernel.SaveState.clear ();
- let realname =
+ let realpath =
match error_extension with
- | None -> filename
+ | None -> path
| Some err_ext ->
- let s = (filename:>string) ^ err_ext in
+ let err_path = Filepath.Normalized.extend path err_ext in
Kernel.warning
"attempting to save on non-zero exit code: \
- modifying filename into `%s'." s;
- Filepath.Normalized.of_string s
+ modifying filename into `%a'." Filepath.Normalized.pretty err_path;
+ err_path
in
try
- Project.save_all realname
+ Project.save_all realpath
with Project.IOError s ->
Kernel.error "problem while saving to file %a (%s)."
- Filepath.Normalized.pretty realname s
+ Filepath.Normalized.pretty realpath s
end
let () =
(* implement a refinement of the behavior described in BTS #1388:
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index ae2a20ae8290e181f17ee018e2e4de1c84967ba0..9807305d313ebbcdaa354103847e76ce590d8792 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -632,9 +632,6 @@ module Assigns: sig
module DepsOrUnassigned : sig
type t =
- | DepsBottom (** Bottom of the lattice, never bound inside a memory state
- at a valid location. (May appear for bases for which the
- validity does not start at 0, currently only NULL.) *)
| Unassigned (** Location has never been assigned *)
| AssignedFrom of Deps.t (** Location guaranteed to have been overwritten,
its contents depend on the [Deps.t] value *)
diff --git a/src/plugins/eva/engine/recursion.ml b/src/plugins/eva/engine/recursion.ml
index 5a1b9728c4252e6b8fe860d74641f4898a354382..4852aa7590e40d00a7c3e812a6fe31fb0e423da7 100644
--- a/src/plugins/eva/engine/recursion.ml
+++ b/src/plugins/eva/engine/recursion.ml
@@ -71,46 +71,6 @@ let check_spec kinstr kf =
Kernel_function.pretty kf;
mark_unknown_requires kinstr kf funspec
-(* Find a spec for a function [kf] that begins a recursive call. If [kf]
- has no existing specification, generate (an incorrect) one, and warn
- loudly. *)
-let _spec_for_recursive_call kf =
- let initial_spec = Annotations.funspec kf in
- match Cil.find_default_behavior initial_spec with
- | Some bhv when bhv.b_assigns <> WritesAny -> initial_spec
- | _ ->
- let assigns = Infer_assigns.from_prototype kf in
- let bhv = Cil.mk_behavior ~assigns:(Writes assigns) () in
- let spec = { (Cil.empty_funspec ()) with spec_behavior = [bhv] } in
- Self.error ~once:true
- "@[recursive@ call@ on@ an unspecified@ \
- function.@ Using@ potentially@ invalid@ inferred assigns '%t'@]"
- (fun fmt -> match assigns with
- | [] -> Format.pp_print_string fmt "assigns \\nothing"
- | _ :: _ ->
- Pretty_utils.pp_list ~sep:"@ " Printer.pp_from fmt assigns);
- (* Merge existing spec into our custom one with assigns *)
- Logic_utils.merge_funspec
- ~silent_about_merging_behav:true spec initial_spec;
- spec
-
-let _empty_spec_for_recursive_call kf =
- let typ_res = Kernel_function.get_return_type kf in
- let empty = Cil.empty_funspec () in
- let assigns =
- if Cil.isVoidType typ_res then
- Writes []
- else
- let res = TResult typ_res, TNoOffset in
- let res = Logic_const.term (TLval res) (Ctype typ_res) in
- let res = Logic_const.new_identified_term res in
- Writes [res, From []]
- in
- let bhv = Cil.mk_behavior ~assigns ~name:Cil.default_behavior_name () in
- empty.spec_behavior <- [bhv];
- empty
-
-
(* -------------------------------------------------------------------------- *)
module CallDepth =
diff --git a/src/plugins/eva/gui/gui_types.ml b/src/plugins/eva/gui/gui_types.ml
index e49f3961817d73337ed630cf402bde872e684849..a1dbdfac667ccb479dd3299f0a333f38b5fb261a 100644
--- a/src/plugins/eva/gui/gui_types.ml
+++ b/src/plugins/eva/gui/gui_types.ml
@@ -141,7 +141,7 @@ module Make (V: Abstract.Value.External) = struct
| GR_Empty -> ()
| GR_Offsm (offsm, typ) -> pretty_gui_offsetmap_res ?typ fmt offsm
| GR_Value (v, typ) -> Eval.Flagged_Value.pretty (V.pretty_typ typ) fmt v
- | GR_Status s -> Eval_terms.pretty_predicate_status fmt s
+ | GR_Status s -> Alarmset.Status.pretty fmt s
| GR_Zone z -> Locations.Zone.pretty fmt z
let equal_gui_res r1 r2 = match r1, r2 with
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 029f84e732e389ca469429048ccbc590200ad788..a2ca78a5b407832479f225467b45ade789e294ef 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -28,37 +28,12 @@ open Cvalue
type predicate_status = Abstract_interp.Comp.result = True | False | Unknown
-let string_of_predicate_status = function
- | Unknown -> "unknown"
- | True -> "valid"
- | False -> "invalid"
-
-let pretty_predicate_status fmt v =
- Format.fprintf fmt "%s" (string_of_predicate_status v)
-
let join_predicate_status x y = match x, y with
| True, True -> True
| False, False -> False
| True, False | False, True
| Unknown, _ | _, Unknown -> Unknown
-let _join_list_predicate_status l =
- let exception Stop in
- try
- let r =
- List.fold_left
- (fun acc e ->
- match e, acc with
- | Unknown, _ -> raise Stop
- | e, None -> Some e
- | e, Some eacc -> Some (join_predicate_status eacc e)
- ) None l
- in
- match r with
- | None -> True
- | Some r -> r
- with Stop -> Unknown
-
(* Type of possible errors during evaluation. See pretty-printer for details *)
type logic_evaluation_error =
| Unsupported of string
diff --git a/src/plugins/eva/legacy/eval_terms.mli b/src/plugins/eva/legacy/eval_terms.mli
index bf8dd3212d21aeac27019bb2d66ef52c0bcc23ac..b4a426ed9e2c36bd443cf82e2dc3728ffcad388b 100644
--- a/src/plugins/eva/legacy/eval_terms.mli
+++ b/src/plugins/eva/legacy/eval_terms.mli
@@ -28,7 +28,6 @@ open Cvalue
(** Evaluating a predicate. [Unknown] is the Top of the lattice *)
type predicate_status = Abstract_interp.Comp.result = True | False | Unknown
-val pretty_predicate_status : Format.formatter -> predicate_status -> unit
val join_predicate_status :
predicate_status -> predicate_status -> predicate_status
diff --git a/src/plugins/eva/types/assigns.ml b/src/plugins/eva/types/assigns.ml
index 012d7bee76053319fa155e0fe3da511f75c5730e..ba5ac5946caa0df13d83e7e69abcdf8e72ed9164 100644
--- a/src/plugins/eva/types/assigns.ml
+++ b/src/plugins/eva/types/assigns.ml
@@ -25,7 +25,6 @@ module DepsOrUnassigned = struct
include Datatype.Serializable_undefined
type t =
- | DepsBottom
| Unassigned
| AssignedFrom of Deps.t
| MaybeAssignedFrom of Deps.t
@@ -34,17 +33,15 @@ module DepsOrUnassigned = struct
let name = "Eva.Froms.DepsOrUnassigned"
let pretty fmt = function
- | DepsBottom -> Format.pp_print_string fmt "DEPS_BOTTOM"
| Unassigned -> Format.pp_print_string fmt "UNASSIGNED"
| AssignedFrom fd -> Deps.pretty_precise fmt fd
| MaybeAssignedFrom fd ->
Format.fprintf fmt "%a (or UNASSIGNED)" Deps.pretty_precise fd
let hash = function
- | DepsBottom -> 1
- | Unassigned -> 2
- | AssignedFrom fd -> Hashtbl.hash (3, Deps.hash fd)
- | MaybeAssignedFrom fd -> Hashtbl.hash (4, Deps.hash fd)
+ | Unassigned -> 1
+ | AssignedFrom fd -> Hashtbl.hash (2, Deps.hash fd)
+ | MaybeAssignedFrom fd -> Hashtbl.hash (3, Deps.hash fd)
let reprs = Unassigned :: List.map (fun r -> AssignedFrom r) Deps.reprs
end
@@ -53,7 +50,6 @@ module DepsOrUnassigned = struct
include Datatype_Input
let join d1 d2 = match d1, d2 with
- | DepsBottom, d | d, DepsBottom -> d
| Unassigned, Unassigned -> Unassigned
| Unassigned, AssignedFrom fd | AssignedFrom fd, Unassigned ->
MaybeAssignedFrom fd
@@ -68,14 +64,11 @@ module DepsOrUnassigned = struct
MaybeAssignedFrom (Deps.join fd1 fd2)
let is_included d1 d2 = match d1, d2 with
- | DepsBottom, (DepsBottom | Unassigned | AssignedFrom _ |
- MaybeAssignedFrom _)
| Unassigned, (Unassigned | AssignedFrom _ | MaybeAssignedFrom _) ->
true
| MaybeAssignedFrom fd1, (AssignedFrom fd2 | MaybeAssignedFrom fd2)
| AssignedFrom fd1, AssignedFrom fd2 ->
Deps.is_included fd1 fd2
- | (Unassigned | AssignedFrom _ | MaybeAssignedFrom _), DepsBottom
| (AssignedFrom _ | MaybeAssignedFrom _), Unassigned
| AssignedFrom _, MaybeAssignedFrom _ ->
false
@@ -85,11 +78,11 @@ module DepsOrUnassigned = struct
let default_is_bottom = false
let to_zone = function
- | DepsBottom | Unassigned -> Locations.Zone.bottom
+ | Unassigned -> Locations.Zone.bottom
| AssignedFrom fd | MaybeAssignedFrom fd -> Deps.to_zone fd
let may_be_unassigned = function
- | DepsBottom | AssignedFrom _ -> false
+ | AssignedFrom _ -> false
| Unassigned | MaybeAssignedFrom _ -> true
end
@@ -97,7 +90,7 @@ module Memory = struct
(* A From table is internally represented as a Lmap of [DepsOrUnassigned].
However, the API mostly hides this fact, and exports access functions
that take or return [Deps.t] values. This way, the user needs not
- understand the subtleties of DepsBottom/Unassigned/MaybeAssigned. *)
+ understand the subtleties of Unassigned/MaybeAssigned. *)
include Lmap_bitwise.Make_bitwise(DepsOrUnassigned)
@@ -150,7 +143,6 @@ module Memory = struct
(* If the interval can be unassigned, we collect its bound. We also
return the dependencies stored at this interval. *)
let default, v = match v with
- | DepsOrUnassigned.DepsBottom -> false, Deps.bottom
| DepsOrUnassigned.Unassigned -> true, Deps.bottom
| DepsOrUnassigned.MaybeAssignedFrom v -> true, v
| DepsOrUnassigned.AssignedFrom v -> false, v
@@ -234,6 +226,6 @@ let outputs assigns =
(fun z v acc ->
let open DepsOrUnassigned in
match v with
- | DepsBottom | Unassigned -> acc
+ | Unassigned -> acc
| AssignedFrom _ | MaybeAssignedFrom _ -> Locations.Zone.join z acc)
m Locations.Zone.bottom
diff --git a/src/plugins/eva/types/assigns.mli b/src/plugins/eva/types/assigns.mli
index a4b3fb16b0b08959ada08b3ab2e7428bb46e8778..cd354ebbb5d1600b0b7ca12489c08b9cd5403901 100644
--- a/src/plugins/eva/types/assigns.mli
+++ b/src/plugins/eva/types/assigns.mli
@@ -27,9 +27,6 @@
module DepsOrUnassigned : sig
type t =
- | DepsBottom (** Bottom of the lattice, never bound inside a memory state
- at a valid location. (May appear for bases for which the
- validity does not start at 0, currently only NULL.) *)
| Unassigned (** Location has never been assigned *)
| AssignedFrom of Deps.t (** Location guaranteed to have been overwritten,
its contents depend on the [Deps.t] value *)
diff --git a/src/plugins/eva/utils/eval_typ.ml b/src/plugins/eva/utils/eval_typ.ml
index 8b12eff33519677727bb594b369962c97940591b..1cc53588178d9592d24c62a473009653a9c8d9eb 100644
--- a/src/plugins/eva/utils/eval_typ.ml
+++ b/src/plugins/eva/utils/eval_typ.ml
@@ -23,14 +23,6 @@
open Cil_types
open Cvalue
-let is_bitfield typlv =
- match Cil.unrollType typlv with
- | TInt (_, attrs) | TEnum (_, attrs) ->
- (match Cil.findAttribute Cil.bitfield_attribute_name attrs with
- | [AInt _] -> true
- | _ -> false)
- | _ -> false
-
let bitfield_size_attributes attrs =
match Cil.findAttribute Cil.bitfield_attribute_name attrs with
| [AInt size] -> Some size
diff --git a/src/plugins/eva/utils/eval_typ.mli b/src/plugins/eva/utils/eval_typ.mli
index 9a62832b61803c19865f9bc96a4bac4eb3317102..94bac41196b043ad9435469af54feef1adf97140 100644
--- a/src/plugins/eva/utils/eval_typ.mli
+++ b/src/plugins/eva/utils/eval_typ.mli
@@ -24,9 +24,6 @@ open Cil_types
(** Functions related to type conversions *)
-(** Bitfields *)
-val is_bitfield: typ -> bool
-
val sizeof_lval_typ: typ -> Int_Base.t
(** Size of the type of a lval, taking into account that the lval might have
been a bitfield. *)
diff --git a/src/plugins/from/from_memory.ml b/src/plugins/from/from_memory.ml
index 9446b88258bf9610b94b42ce0140b2c7ded02bf4..bf8e718ac28c518efdfbfa16aa74e04beb72f1b8 100644
--- a/src/plugins/from/from_memory.ml
+++ b/src/plugins/from/from_memory.ml
@@ -28,7 +28,6 @@ module DepsOrUnassigned = struct
let subst f d =
match d with
- | DepsBottom -> DepsBottom
| Unassigned -> Unassigned
| AssignedFrom fd ->
let fd' = f fd in
@@ -39,8 +38,6 @@ module DepsOrUnassigned = struct
let compose d1 d2 =
match d1, d2 with
- | DepsBottom, _ | _, DepsBottom ->
- DepsBottom (* could indicate dead code. Not used in practice anyway *)
| Unassigned, _ -> d2
| AssignedFrom _, _ -> d1
| MaybeAssignedFrom _, Unassigned -> d1
@@ -52,14 +49,12 @@ module DepsOrUnassigned = struct
(* for backwards compatibility *)
let pretty fmt fd =
match fd with
- | DepsBottom -> Format.pp_print_string fmt "DEPS_BOTTOM"
| Unassigned -> Format.pp_print_string fmt "(SELF)"
| AssignedFrom d -> Zone.pretty fmt (Deps.to_zone d)
| MaybeAssignedFrom d ->
Format.fprintf fmt "%a (and SELF)" Zone.pretty (Deps.to_zone d)
let pretty_precise fmt = function
- | DepsBottom -> Format.pp_print_string fmt "DEPS_BOTTOM"
| Unassigned -> Format.pp_print_string fmt "UNASSIGNED"
| AssignedFrom fd -> Deps.pretty_precise fmt fd
| MaybeAssignedFrom fd ->
@@ -197,7 +192,6 @@ let collapse_return x = x
(* ----- Pretty-printing ---------------------------------------------------- *)
let pretty_skip = function
- | DepsOrUnassigned.DepsBottom -> true
| DepsOrUnassigned.Unassigned -> true
| DepsOrUnassigned.AssignedFrom _ -> false
| DepsOrUnassigned.MaybeAssignedFrom _ -> false
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 3c4ca70562ce8dd7da47f16b043c443c61c937be..98e6aee809bcc8eaa0abe9bcd2004e290aa4edb6 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -526,7 +526,7 @@ let extract_inout_from_froms assigns =
(* Skip zones fully unassigned, they are not really port of the
dependencies, but just present in the offsetmap to avoid "holes" *)
match (in_ : Eva.Assigns.DepsOrUnassigned.t) with
- | DepsBottom | Unassigned -> acc
+ | Unassigned -> acc
| AssignedFrom in_ | MaybeAssignedFrom in_ ->
Zone.join acc_in (Eva.Deps.to_zone in_),
Zone.join acc_out out
diff --git a/tests/builtins/oracle_bitwise/allocated.0.res.oracle b/tests/builtins/oracle_bitwise/allocated.0.res.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests/builtins/oracle_bitwise/allocated.1.res.oracle b/tests/builtins/oracle_bitwise/allocated.1.res.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests/builtins/oracle_bitwise/malloc-optimistic.res.oracle b/tests/builtins/oracle_bitwise/malloc-optimistic.res.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests/value/clean_abort.i b/tests/value/clean_abort.i
new file mode 100644
index 0000000000000000000000000000000000000000..d06a5c35c0809af4b2ff5b4786c31fc01c4e6c7d
--- /dev/null
+++ b/tests/value/clean_abort.i
@@ -0,0 +1,55 @@
+/* run.config
+ EXIT: 1
+ EXECNOW: BIN @PTEST_NAME@.sav.error LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -eva @EVA_OPTIONS@ -eva-stop-at-nth-alarm 4 @PTEST_FILE@ -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
+ EXIT: 0
+ PLUGIN: @PTEST_PLUGIN@ report
+ OPT: -load %{dep:@PTEST_NAME@.sav.error} -out -input -deps -report
+*/
+/* run.config*
+ DONTRUN: avoids duplication of oracles
+*/
+
+/* Tests the "clean" stop of the analysis (here via -eva-stop-at-nth-alarm)
+ with -save name: save a valid session file "name.error", which can then be
+ reloaded and contains partial results of the functions analyzed before the
+ crash. */
+
+volatile unsigned int nondet;
+
+int t[10];
+
+int g;
+
+/* Completely analyzed: results should be correct. */
+void init (int x) {
+ int i = 0;
+ //@ loop unroll 10;
+ for (; i < 10; i++) {
+ t[i] = nondet % x; // alarm: modulo by zero
+ }
+ g = t[x]; // alarm: out of bound index
+ if (nondet) g = t[i]; // invalid alarm: out of bound index
+ //@ assert valid: i == 10;
+}
+
+/* Partially analyzed, so partial results… */
+void partial (int x) {
+ //@ assert valid: 0 <= x;
+ g = 100 / x; // division by zero
+ // The analysis stops here. Alarms below are never emitted.
+ g = nondet + x; // overflow alarm
+ g = t[x]; // out of bounds alarms
+ //@ assert unreached: g > 0;
+}
+
+/* Unreached by the analysis, as it stops before. */
+void unreached (int x) {
+ g = x / x;
+ //@ assert unreached: g == 1;
+}
+
+void main (void) {
+ init(nondet % 100);
+ partial(nondet % 100);
+ unreached(nondet % 100);
+}
diff --git a/tests/value/domains.i b/tests/value/domains.i
index 22b198ea39fc8bd5e37848ce41c3dbf82294acd3..defe295b671a8d02072cef7f0ba5962ce1f40674 100644
--- a/tests/value/domains.i
+++ b/tests/value/domains.i
@@ -1,29 +1,58 @@
+/* run.config
+ LOG: domains_dump_0
+ STDOPT: #"-eva-domains sign,equality,bitwise,symbolic-locations,gauges,octagon,multidim -eva-msg-key=d-equality,d-symbolic-locations,d-gauges,d-octagon,d-multidim,d-bitwise,d-sign -eva-warn-key experimental=inactive"
+*/
/* run.config*
- STDOPT: #"-eva-domains sign,equality,bitwise,symbolic-locations,gauges -eva-slevel 2"
+ DONTRUN: avoids duplication of domains_dump oracle
*/
-/* Tests five domains together. */
+volatile int nondet;
+
+/* Tests multiple domains together. */
void main (int a) {
- int b, i, k, r;
- /* Tests the equality domain: b is reduced after the condition, no overflow. */
- b = a;
- if (a < 10)
- r = b + 1;
- /* Tests the symbolic locations domain: t[i] is smaller than 10, no overflow. */
- int t[2] = {a, a};
- i = a > 0;
- if (t[i] < 10)
- r = t[i] + 1;
+ int i, j, k, r;
+ int t[100];
+ /* Tests the multidim domain: the array is initialized after the loop. */
+ for (i = 0; i < 100; i++) {
+ t[i] = nondet;
+ }
+ i = t[64];
+ /* Tests the equality domain: i is reduced through the condition,
+ no invalid read. */
+ int b1 = i <= 0;
+ int b2 = i >= 100;
+ if (b1 || b2)
+ i = 1;
+ r = t[i];
+ /* Tests the symbolic locations domain: t[i]/i is smaller than 1000,
+ no overflow. */
+ if (t[i] / i < 1000)
+ r = t[i] / i + 1;
/* Tests the gauges domain: k==i during the loop, no overflow. */
k = 0;
- while (k < 12) {
+ j = 10;
+ while (k < 200 && nondet) {
k++;
- i++;
+ j++;
}
+ /* Tests the octagon domain. */
+ r = i - j + 1;
+ k = r + j;
+ r = t[k-1];
/* Tests the sign domain: no division by zero. */
if (a != 0)
r = 100 / a;
/* Tests the bitwise domain: a == 8, no division by zero. */
a = (a | 8) & 8;
r = 10 / a;
+
+ /* Tests printing of domains. */
+ Frama_C_domain_show_each(a, i, j, k, r);
+ Frama_C_dump_each();
+ Frama_C_dump_each_file_domains_dump();
+
+ /* Tests printing offsetmap of scalar value. */
+ int scalar = 65537;
+ *(((char *)&scalar)+1) = 42;
+ Frama_C_domain_show_each(scalar);
}
diff --git a/tests/value/oracle/clean_abort.res.oracle b/tests/value/oracle/clean_abort.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..284520def20c908f60df07663cb8c12522334efd
--- /dev/null
+++ b/tests/value/oracle/clean_abort.res.oracle
@@ -0,0 +1,62 @@
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
+[from] Computing for function init
+[from] Done for function init
+[from] Computing for function partial
+[from] Non-terminating function partial (no dependencies)
+[from] Done for function partial
+[from] Computing for function main
+[from] Non-terminating function main (no dependencies)
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function init:
+ t[0..9] FROM nondet; x (and SELF)
+ g FROM nondet; t[1..9]; x
+[from] Function partial:
+ NON TERMINATING - NO EFFECTS
+[from] Function main:
+ NON TERMINATING - NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function init:
+ t[0..9]; g; i
+[inout] Inputs for function init:
+ nondet; t[1..9]
+[inout] Out (internal) for function partial:
+ g
+[inout] Inputs for function partial:
+ \nothing
+[inout] Out (internal) for function main:
+ t[0..9]; g
+[inout] Inputs for function main:
+ nondet; t[1..9]
+[report] Computing properties status...
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'init'
+--------------------------------------------------------------------------------
+
+[ Valid ] Assertion 'valid' (file clean_abort.i, line 32)
+ by Eva.
+[ - ] Assertion 'Eva,division_by_zero' (file clean_abort.i, line 28)
+ tried with Eva.
+[ - ] Assertion 'Eva,index_bound' (file clean_abort.i, line 30)
+ tried with Eva.
+[ - ] Assertion 'Eva,index_bound' (file clean_abort.i, line 31)
+ tried with Eva.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'partial'
+--------------------------------------------------------------------------------
+
+[ Valid ] Assertion 'valid' (file clean_abort.i, line 37)
+ by Eva.
+[ - ] Assertion 'Eva,division_by_zero' (file clean_abort.i, line 38)
+ tried with Eva.
+
+--------------------------------------------------------------------------------
+--- Status Report Summary
+--------------------------------------------------------------------------------
+ 2 Completely validated
+ 4 To be validated
+ 6 Total
+--------------------------------------------------------------------------------
diff --git a/tests/value/oracle/clean_abort_sav.res b/tests/value/oracle/clean_abort_sav.res
new file mode 100644
index 0000000000000000000000000000000000000000..575493d727d3d6a4d6a1da0dacd3037642b30fc0
--- /dev/null
+++ b/tests/value/oracle/clean_abort_sav.res
@@ -0,0 +1,27 @@
+[kernel] Parsing clean_abort.i (no 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
+ nondet ∈ [--..--]
+ t[0..9] ∈ {0}
+ g ∈ {0}
+[eva] computing for function init <- main.
+ Called from clean_abort.i:52.
+[eva:alarm] clean_abort.i:28: Warning:
+ division by zero. assert (unsigned int)x ≢ 0;
+[eva:alarm] clean_abort.i:30: Warning:
+ accessing out of bounds index. assert x < 10;
+[eva:alarm] clean_abort.i:31: Warning:
+ accessing out of bounds index. assert i < 10;
+[eva] clean_abort.i:32: assertion 'valid' got status valid.
+[eva] Recording results for init
+[eva] Done for function init
+[eva] computing for function partial <- main.
+ Called from clean_abort.i:53.
+[eva] clean_abort.i:37: assertion 'valid' got status valid.
+[eva:alarm] clean_abort.i:38: Warning: division by zero. assert x ≢ 0;
+[eva] User Error: Stopping at nth alarm
+[eva] Clean up and save partial results.
+[kernel] Plug-in eva aborted: invalid user input.
+[kernel] Warning: attempting to save on non-zero exit code: modifying filename into `clean_abort.sav.error'.
diff --git a/tests/value/oracle/domains.res.oracle b/tests/value/oracle/domains.res.oracle
index 5bb482d01c270bc8a4f948c4ec50f9277129a034..55968e3431b11513fcc643d7834169af391b5f10 100644
--- a/tests/value/oracle/domains.res.oracle
+++ b/tests/value/oracle/domains.res.oracle
@@ -3,18 +3,156 @@
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
+ nondet ∈ [--..--]
+[eva:partition] domains.i:16: starting to merge loop iterations
+[eva:partition] domains.i:34: starting to merge loop iterations
+[eva] domains.i:50:
+ Frama_C_domain_show_each:
+ a : # cvalue: {8}
+ # equality:
+ # symbolic-locations: (not implemented)
+ # octagon: (not implemented)
+ # gauges: (not implemented)
+ # sign: +
+ # bitwise: (not implemented)
+ # multidim: {8}
+ i : # cvalue: [1..99]
+ # equality:
+ # symbolic-locations: (not implemented)
+ # octagon: (not implemented)
+ # gauges: (not implemented)
+ # sign: +
+ # bitwise: (not implemented)
+ # multidim: [1..99]
+ j : # cvalue: [10..210]
+ # equality:
+ # symbolic-locations: (not implemented)
+ # octagon: (not implemented)
+ # gauges: (not implemented)
+ # sign: +
+ # bitwise: (not implemented)
+ # multidim: [10..210]
+ k : # cvalue: [2..100]
+ # equality: {k = ((i - j) + 1) + j}
+ # symbolic-locations: (not implemented)
+ # octagon: (not implemented)
+ # gauges: (not implemented)
+ # sign: -0+
+ # bitwise: (not implemented)
+ # multidim: [2..100]
+ r : # cvalue: {1}
+ # equality:
+ # symbolic-locations: (not implemented)
+ # octagon: (not implemented)
+ # gauges: (not implemented)
+ # sign: 0+
+ # bitwise: (not implemented)
+ # multidim: {1}
+[eva] domains.i:51:
+ Frama_C_dump_each:
+ # cvalue:
+ nondet ∈ [--..--]
+ a ∈ {8}
+ i ∈ [1..99]
+ j ∈ [10..210]
+ k ∈ [2..100]
+ r ∈ {1}
+ t[0..63] ∈ [--..--] or UNINITIALIZED
+ [64] ∈ [--..--]
+ [65..99] ∈ [--..--] or UNINITIALIZED
+ b1 ∈ {0; 1}
+ b2 ∈ {0; 1}
+ scalar ∈ UNINITIALIZED
+ # equality:
+ {k = ((i - j) + 1) + j}
+ # symbolic-locations:
+ V: {[ t[i] -> [-2147483648..2147483647]
+ t[i] / i -> [-2147483648..2147483647]
+ i - j -> [-209..89]
+ t[k - 1] -> [-2147483648..2147483647] ]}
+ Z: {[ t[i] -> i; t[1..99]
+ t[i] / i -> i; t[1..99]
+ i - j -> i; j
+ t[k - 1] -> k; t[1..99] ]}
+ I: {[ i -> {t[i], t[i] / i, i - j}
+ j -> {i - j}
+ k -> {t[k - 1]}
+ t -> {t[i], t[i] / i, t[k - 1]} ]}
+ S: {[ i -> {t[i], t[i] / i, i - j}
+ j -> {i - j}
+ k -> {t[k - 1]}
+ t -> {t[i], t[i] / i, t[k - 1]} ]}
+ # octagon:
+ {[ i + j ∈ [11..309]
+ j + k ∈ [12..310]
+ j - k ∈ [-90..208]
+ ]}
+ # gauges:
+ V: [{[ a -> {8}
+ i -> [-2147483648..2147483647]
+ j -> [10..210]
+ k -> [-2147483847..2147483848]
+ r -> {1}
+ b1 -> {0; 1}
+ b2 -> {0; 1} ]}]
-[eva:partition] domains.i:19: starting to merge loop iterations
+ # sign:
+ {[ a -> +
+ i -> +
+ j -> +
+ r -> 0+ ]}
+ # bitwise:
+ a[bits 0 to 2] ∈ {0}
+ [bits 3 to 3] ∈ {1}
+ [bits 4 to 31] ∈ {0}
+ # multidim:
+ ({[ a -> ({8}, {})
+ i -> ([1..99], {t})
+ j -> ([10..210], {})
+ k -> ([2..100], {t})
+ r -> ({1}, {})
+ t -> ({
+ [0 .. k - 2] = [-2147483648..2147483647],
+ [k - 1] = [-2147483648..2147483647],
+ [k .. 99] = [-2147483648..2147483647]
+ },
+ {})
+ b1 -> ({0; 1}, {})
+ b2 -> ({0; 1}, {})
+ scalar -> (UNINITIALIZED, {}) ]},
+ None)
+ ==END OF DUMP==
+[eva] domains.i:52: Dumping state in file 'domains_dump_0'
+[eva] domains.i:57:
+ Frama_C_domain_show_each:
+ scalar : # cvalue: [bits 0 to 7]# ∈ {65537}%32, bits 0 to 7
+ [bits 8 to 15] ∈ {42}
+ [bits 16 to 31]# ∈ {65537}%32, bits 16 to 31
+ This amounts to: {76289}
+ # equality:
+ # symbolic-locations: (not implemented)
+ # octagon: (not implemented)
+ # gauges: (not implemented)
+ # sign: -0+
+ # bitwise: (not implemented)
+ # multidim: T
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
a ∈ {8}
- b ∈ [--..--]
- i ∈ [1..2147483647]
- k ∈ {12}
+ i ∈ [1..99]
+ j ∈ [10..210]
+ k ∈ [2..100]
r ∈ {1}
- t[0..1] ∈ [--..--]
+ t[0..63] ∈ [--..--] or UNINITIALIZED
+ [64] ∈ [--..--]
+ [65..99] ∈ [--..--] or UNINITIALIZED
+ b1 ∈ {0; 1}
+ b2 ∈ {0; 1}
+ scalar[bits 0 to 7]# ∈ {65537}%32, bits 0 to 7
+ [bits 8 to 15] ∈ {42}
+ [bits 16 to 31]# ∈ {65537}%32, bits 16 to 31
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
@@ -23,6 +161,6 @@
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
- a; b; i; k; r; t[0..1]
+ a; i; j; k; r; t[0..99]; b1; b2; scalar
[inout] Inputs for function main:
- \nothing
+ nondet
diff --git a/tests/value/oracle/domains_dump_0 b/tests/value/oracle/domains_dump_0
new file mode 100644
index 0000000000000000000000000000000000000000..69dce4193ff046e66371f19194c77cb6cdfbbc42
--- /dev/null
+++ b/tests/value/oracle/domains_dump_0
@@ -0,0 +1,72 @@
+DUMPING STATE at file domains.i line 52
+# cvalue:
+nondet ∈ [--..--]
+a ∈ {8}
+i ∈ [1..99]
+j ∈ [10..210]
+k ∈ [2..100]
+r ∈ {1}
+t[0..63] ∈ [--..--] or UNINITIALIZED
+ [64] ∈ [--..--]
+ [65..99] ∈ [--..--] or UNINITIALIZED
+b1 ∈ {0; 1}
+b2 ∈ {0; 1}
+scalar ∈ UNINITIALIZED
+# equality:
+{k = ((i - j) + 1) + j}
+# symbolic-locations:
+V: {[ t[i] -> [-2147483648..2147483647]
+ t[i] / i -> [-2147483648..2147483647]
+ i - j -> [-209..89]
+ t[k - 1] -> [-2147483648..2147483647] ]}
+Z: {[ t[i] -> i; t[1..99]
+ t[i] / i -> i; t[1..99]
+ i - j -> i; j
+ t[k - 1] -> k; t[1..99] ]}
+I: {[ i -> {t[i], t[i] / i, i - j}
+ j -> {i - j}
+ k -> {t[k - 1]}
+ t -> {t[i], t[i] / i, t[k - 1]} ]}
+S: {[ i -> {t[i], t[i] / i, i - j}
+ j -> {i - j}
+ k -> {t[k - 1]}
+ t -> {t[i], t[i] / i, t[k - 1]} ]}
+# octagon:
+{[ i + j ∈ [11..309]
+ j + k ∈ [12..310]
+ j - k ∈ [-90..208]
+ ]}
+# gauges:
+V: [{[ a -> {8}
+ i -> [-2147483648..2147483647]
+ j -> [10..210]
+ k -> [-2147483847..2147483848]
+ r -> {1}
+ b1 -> {0; 1}
+ b2 -> {0; 1} ]}]
+
+# sign:
+{[ a -> +
+ i -> +
+ j -> +
+ r -> 0+ ]}
+# bitwise:
+a[bits 0 to 2] ∈ {0}
+ [bits 3 to 3] ∈ {1}
+ [bits 4 to 31] ∈ {0}
+# multidim:
+({[ a -> ({8}, {})
+ i -> ([1..99], {t})
+ j -> ([10..210], {})
+ k -> ([2..100], {t})
+ r -> ({1}, {})
+ t -> ({
+ [0 .. k - 2] = [-2147483648..2147483647],
+ [k - 1] = [-2147483648..2147483647],
+ [k .. 99] = [-2147483648..2147483647]
+ },
+ {})
+ b1 -> ({0; 1}, {})
+ b2 -> ({0; 1}, {})
+ scalar -> (UNINITIALIZED, {}) ]},
+ None)
diff --git a/tests/value/oracle/show_perf.res.oracle b/tests/value/oracle/show_perf.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..511d75fbce0f7e17de7b69486622af124f2b07bd
--- /dev/null
+++ b/tests/value/oracle/show_perf.res.oracle
@@ -0,0 +1,150 @@
+[kernel] Parsing show_perf.i (no 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
+ nondet ∈ [--..--]
+[eva] computing for function print_collatz <- main.
+ Called from show_perf.i:44.
+[eva] computing for function collatz <- print_collatz <- main.
+ Called from show_perf.i:38.
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+ Called from show_perf.i:31.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+ Called from show_perf.i:31.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+ Called from show_perf.i:31.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+ Called from show_perf.i:31.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+ Called from show_perf.i:31.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+ Called from show_perf.i:31.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+ Called from show_perf.i:31.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+ Called from show_perf.i:31.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+ Called from show_perf.i:31.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+ Called from show_perf.i:31.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+ Called from show_perf.i:31.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+ Called from show_perf.i:31.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+ Called from show_perf.i:31.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+ Called from show_perf.i:31.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+ Called from show_perf.i:31.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] computing for function compute_next <- collatz <- print_collatz <- main.
+ Called from show_perf.i:31.
+[eva] Recording results for compute_next
+[eva] Done for function compute_next
+[eva] Recording results for collatz
+[eva] Done for function collatz
+[eva] show_perf.i:39: Reusing old results for call to collatz
+[eva] show_perf.i:40: Frama_C_show_each: {7}, {16}, {52}
+[eva] Recording results for print_collatz
+[eva] Done for function print_collatz
+[eva] Recording results for main
+[eva] Done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function compute_next:
+ __retres ∈ [1..52]
+[eva:final-states] Values at end of function collatz:
+ i ∈ {16}
+ v ∈ {1}
+ max ∈ {52}
+ r.length ∈ {16}
+ .max ∈ {52}
+[eva:final-states] Values at end of function print_collatz:
+ r.length ∈ {16}
+ .max ∈ {52}
+[eva:final-states] Values at end of function main:
+
+[eva] ######## Eva execution feedback ########
+ Long running functions:
+ ================================================================
+ * main: executed: 1x total: ?s
+ | print_collatz 1x ?s (?%) | self: ?s (?%)
+ * print_collatz: executed: 1x total: ?s
+ | collatz 2x ?s (?%) | self: ?s (?%)
+ * collatz: executed: 2x total: ?s
+ | compute_next 16x ?s (?%) | self: ?s (?%)
+ * compute_next: executed: 16x total: ?s
+ | self: ?s (?%)
+
+ Execution time per callstack:
+ ================================================================
+ * main: executed: 1x total: ?s
+ | * print_collatz: executed: 1x total: ?s
+ | | * collatz: executed: 2x total: ?s
+ | | | * compute_next: executed: 16x total: ?s
+ Â
+[from] Computing for function compute_next
+[from] Done for function compute_next
+[from] Computing for function collatz
+[from] Done for function collatz
+[from] Computing for function print_collatz
+[from] Done for function print_collatz
+[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 compute_next:
+ \result FROM x
+[from] Function collatz:
+ \result FROM n
+[from] Function print_collatz:
+ NO EFFECTS
+[from] Function main:
+ NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function compute_next:
+ tmp; __retres
+[inout] Inputs for function compute_next:
+ \nothing
+[inout] Out (internal) for function collatz:
+ i; v; max; tmp; r
+[inout] Inputs for function collatz:
+ \nothing
+[inout] Out (internal) for function print_collatz:
+ r
+[inout] Inputs for function print_collatz:
+ \nothing
+[inout] Out (internal) for function main:
+ \nothing
+[inout] Inputs for function main:
+ \nothing
diff --git a/tests/value/oracle/uninit_callstack.res.oracle b/tests/value/oracle/uninit_callstack.res.oracle
index d91968decd6248cd0c1d0eae1aaa9901b3450e8a..ae41012e4f12e448023b9d7d21d747747c4bb5b2 100644
--- a/tests/value/oracle/uninit_callstack.res.oracle
+++ b/tests/value/oracle/uninit_callstack.res.oracle
@@ -3,7 +3,7 @@
[eva:initial-state] Values of globals at initialization
p ∈ {0}
x ∈ {0}
-[eva:alarm] uninit_callstack.i:8: Warning:
+[eva:alarm] uninit_callstack.i:9: Warning:
accessing uninitialized left-value. assert \initialized(p);
- stack: f :: uninit_callstack.i:14 <- main
+ stack: <????> f :: uninit_callstack.i:15 <- main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle_apron/show_perf.res.oracle b/tests/value/oracle_apron/show_perf.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e00947e9f838d930475745273ef6d19b64e82c24
--- /dev/null
+++ b/tests/value/oracle_apron/show_perf.res.oracle
@@ -0,0 +1,81 @@
+77c77,144
+< [eva] show_perf.i:39: Reusing old results for call to collatz
+---
+> [eva] computing for function collatz <- print_collatz <- main.
+> Called from show_perf.i:39.
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+> Called from show_perf.i:31.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+> Called from show_perf.i:31.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+> Called from show_perf.i:31.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+> Called from show_perf.i:31.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+> Called from show_perf.i:31.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+> Called from show_perf.i:31.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+> Called from show_perf.i:31.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+> Called from show_perf.i:31.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+> Called from show_perf.i:31.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+> Called from show_perf.i:31.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+> Called from show_perf.i:31.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+> Called from show_perf.i:31.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+> Called from show_perf.i:31.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+> Called from show_perf.i:31.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+> Called from show_perf.i:31.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
+> Called from show_perf.i:31.
+> [eva] Recording results for compute_next
+> [eva] Done for function compute_next
+> [eva] Recording results for collatz
+> [eva] Done for function collatz
+105,106c172,173
+< | compute_next 16x ?s (?%) | self: ?s (?%)
+< * compute_next: executed: 16x total: ?s
+---
+> | compute_next 32x ?s (?%) | self: ?s (?%)
+> * compute_next: executed: 32x total: ?s
+114c181
+< | | | * compute_next: executed: 16x total: ?s
+---
+> | | | * compute_next: executed: 32x total: ?s
diff --git a/tests/value/show_perf.i b/tests/value/show_perf.i
new file mode 100644
index 0000000000000000000000000000000000000000..f37e9d7b80c1b7a5b6bbe9f098727b9400e43350
--- /dev/null
+++ b/tests/value/show_perf.i
@@ -0,0 +1,45 @@
+/* run.config*
+ FILTER: sed -e 's/\([0-9.]\+\(%\|s\)\)/?\2/g'
+ STDOPT: +"-eva-show-perf"
+ EXECNOW: BIN flamegraph.txt BIN flamegraph.err { PTESTS_TESTING=1 %{bin:frama-c} @PTEST_FILE@ -eva -eva-flamegraph flamegraph.txt && NOGUI=1 %{bin:frama-c-script} flamegraph flamegraph.txt; } 1> /dev/null 2> flamegraph.err
+*/
+
+/* This example is kept minimal to ensure the stability of the output
+ of -eva-show-perf on the first run.
+ The second run only tests that the flamegraph generated by -eva-flamegraph
+ is valid. */
+
+volatile int nondet;
+
+typedef struct S {
+ unsigned int length;
+ unsigned int max;
+} result;
+
+int compute_next(unsigned int x) {
+ return (x % 2 == 0) ? x / 2 : 3*x + 1;
+}
+
+result collatz(unsigned int n) {
+ unsigned int i = 0;
+ unsigned int v = n;
+ unsigned int max = n;
+ //@ loop unroll 100;
+ for (i = 0; i < 100; i++) {
+ if (v == 1) break;
+ if (v > max) max = v;
+ v = compute_next(v);
+ }
+ result r = { .length = i, .max = max };
+ return r;
+}
+
+void print_collatz(unsigned int n) {
+ result r = collatz(n); // 1 call to collatz
+ r = collatz(n); // 1 call cached by memexec
+ Frama_C_show_each(n, r.length, r.max);
+}
+
+void main (void) {
+ print_collatz(7); // 16 calls to [compute_next] for n = 7.
+}
diff --git a/tests/value/uninit_callstack.i b/tests/value/uninit_callstack.i
index 8ee2bed040ae9d010226ded9ee9ddf6883fe8985..595fa78096ba06aff83cd9eb86589cc73c789caf 100644
--- a/tests/value/uninit_callstack.i
+++ b/tests/value/uninit_callstack.i
@@ -1,6 +1,7 @@
/* run.config*
PLUGIN: @EVA_MAIN_PLUGINS@
- OPT: -eva @EVA_CONFIG@ -eva-no-show-progress -eva-print-callstacks -eva-no-results
+ FILTER: sed -e 's/<....>/<????>/g'
+ OPT: -eva @EVA_CONFIG@ -eva-no-show-progress -eva-print-callstacks -eva-msg-key=callstack -eva-no-results
*/
int *p, x;
void f(void)