diff --git a/src/plugins/eva/engine/transfer_logic.ml b/src/plugins/eva/engine/transfer_logic.ml
index 5dc4ddfdc11bc4fd0ba6a5465fa363f9a5e852e9..41aa1bc0dcc998b4bc84eaf8866910479fe1784f 100644
--- a/src/plugins/eva/engine/transfer_logic.ml
+++ b/src/plugins/eva/engine/transfer_logic.ml
@@ -27,7 +27,26 @@ open Eval
let ignore_predicate named_pred =
List.exists (fun tag -> tag = "no_eva") named_pred.Cil_types.pred_name
-(* -------------------------- Message emission ------------------------------ *)
+let create_conjunction l=
+ let loc = match l with
+ | [] -> None
+ | p :: _ -> Some (Logic_const.pred_of_id_pred p).pred_loc
+ in
+ Logic_const.(List.fold_right (fun p1 p2 -> pand ?loc (p1, p2)) (List.map pred_of_id_pred l) ptrue)
+
+let ip_from_precondition kf call_ki b pre =
+ let ip_precondition = Property.ip_of_requires kf Kglobal b pre in
+ match call_ki with
+ | Kglobal -> (* status of the main function. We update the global
+ status, and pray that there is no recursion.
+ TODO: check what the WP does.*)
+ ip_precondition
+ | Kstmt stmt ->
+ (* choose the copy of the precondition on the call point [stmt]. *)
+ Statuses_by_call.setup_precondition_proxy kf ip_precondition;
+ Statuses_by_call.precondition_at_call kf ip_precondition stmt
+
+(* --------------------- Message and status emission ------------------------ *)
(* The function that puts statuses on pre- and post-conditions is essentially
agnostic as to which kind of property it operates on. However, the messages
@@ -60,15 +79,15 @@ let post_kind kf =
else PostLeaf
else PostBody
-let conv_status = function
- | Alarmset.False -> Property_status.False_if_reachable;
- | Alarmset.True -> Property_status.True;
- | Alarmset.Unknown -> Property_status.Dont_know
-
let emit_status ppt status =
- if status = Property_status.False_if_reachable then begin
+ let status =
+ match status with
+ | Alarmset.False -> Property_status.False_if_reachable;
+ | Alarmset.True -> Property_status.True;
+ | Alarmset.Unknown -> Property_status.Dont_know
+ in
+ if status = Property_status.False_if_reachable then
Red_statuses.add_red_property (Property.get_kinstr ppt) ppt;
- end;
Property_status.emit ~distinct:true Eva_utils.emitter ~hyps:[] ppt status
(* Display the message as result/warning depending on [status] *)
@@ -111,7 +130,7 @@ let pp_predicate behavior kind fmt named_pred =
in
Format.fprintf fmt "%a%a" pp_p_kind kind pp_predicate named_pred
-let emit_message_and_status kind kf behavior ~active ~empty property named_pred status =
+let emit_contract_status kind kf behavior ~active ~empty property named_pred status =
let pp_predicate = pp_predicate behavior kind in
let source = fst (Property.location property) in
match kind with
@@ -124,34 +143,51 @@ let emit_message_and_status kind kf behavior ~active ~empty property named_pred
Alarmset.Status.pretty status
(if active then (fun _ -> ()) else behavior_inactive)
Eva_utils.pp_callstack;
- emit_status property (conv_status status);
+ emit_status property status;
| Postcondition postk ->
(* Do not emit a status for leaf functions or builtins. Otherwise, we would
overwrite the "considered valid" status of the kernel. *)
if emit_postcond_status postk
- then emit_status property (conv_status status)
+ then emit_status property status
| Assumes ->
(* No statuses are emitted for 'assumes' clauses, and for the moment we
do not emit text either *) ()
-let create_conjunction l=
- let loc = match l with
- | [] -> None
- | p :: _ -> Some (Logic_const.pred_of_id_pred p).pred_loc
+let pp_code_annot fmt ca =
+ match ca.annot_content with
+ | AAssert (_,{ tp_kind; tp_statement }) ->
+ let kind = Cil_printer.name_of_assert tp_kind in
+ Format.fprintf fmt "%s%a" kind Description.pp_named tp_statement
+ | AInvariant (_, _, { tp_statement }) ->
+ Format.fprintf fmt "loop invariant%a" Description.pp_named tp_statement
+ | AExtended (_, _, extension) ->
+ Format.fprintf fmt "%s annotation" extension.ext_name;
+ | APragma _ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _ ->
+ assert false (* currently not treated by Eva *)
+
+(* location of the given code annotation. If unknown, use the location of the
+ statement instead. *)
+let code_annotation_loc stmt code_annot =
+ match Cil_datatype.Code_annotation.loc code_annot with
+ | Some loc when not (Cil_datatype.Location.(equal loc unknown)) -> loc
+ | _ -> Cil_datatype.Stmt.loc stmt
+
+let emit_code_annot_status ~reduce ~empty kf stmt code_annot status =
+ let source, _ = code_annotation_loc stmt code_annot in
+ let ips = Property.ip_of_code_annot kf stmt code_annot in
+ List.iter (fun p -> emit_status p status) ips;
+ let message =
+ match status with
+ | Alarmset.Unknown -> "unknown"
+ | Alarmset.True -> "valid"
+ | Alarmset.False ->
+ "invalid" ^ (if reduce then " (stopping propagation)" else "")
in
- Logic_const.(List.fold_right (fun p1 p2 -> pand ?loc (p1, p2)) (List.map pred_of_id_pred l) ptrue)
+ let prefix = if empty then "no state left, " else "" in
+ msg_status status ~once:true ~source
+ "%s%a got status %s." prefix pp_code_annot code_annot message
-let ip_from_precondition kf call_ki b pre =
- let ip_precondition = Property.ip_of_requires kf Kglobal b pre in
- match call_ki with
- | Kglobal -> (* status of the main function. We update the global
- status, and pray that there is no recursion.
- TODO: check what the WP does.*)
- ip_precondition
- | Kstmt stmt ->
- (* choose the copy of the precondition on the call point [stmt]. *)
- Statuses_by_call.setup_precondition_proxy kf ip_precondition;
- Statuses_by_call.precondition_at_call kf ip_precondition stmt
+(* --------------------- Process inactive behaviors ------------------------- *)
(* Emits informative messages about inactive behaviors, and emits a valid
status for requires and ensures that have not been evaluated. *)
@@ -163,14 +199,14 @@ let process_inactive_behavior kf call_ki behavior =
emitted := true;
if emit_postcond_status (post_kind kf) then
let ip = Property.ip_of_ensures kf Kglobal behavior post in
- emit_status ip Property_status.True;
+ emit_status ip Alarmset.True;
end
) behavior.b_post_cond;
List.iter (fun pre ->
if pre.ip_content.tp_kind <> Admit then begin
emitted := true;
let ip = ip_from_precondition kf call_ki behavior pre in
- emit_status ip Property_status.True;
+ emit_status ip Alarmset.True;
end
) behavior.b_requires;
if !emitted then
@@ -192,7 +228,7 @@ let process_inactive_postconds kf inactive_bhvs =
emitted := true;
if emit_postcond_status (post_kind kf) then
let ip = Property.ip_of_ensures kf Kglobal b post in
- emit_status ip Property_status.True;
+ emit_status ip Alarmset.True;
end
) b.b_post_cond;
if !emitted then
@@ -201,6 +237,57 @@ let process_inactive_postconds kf inactive_bhvs =
(pp_header kf) b Eva_utils.pp_callstack;
) inactive_bhvs
+
+(* ---------------- Evaluation of "calls" ACSL extension ------------------- *)
+
+let get_call term =
+ match term.term_node with
+ | TLval (TVar { lv_origin = Some v }, TNoOffset ) -> Globals.Functions.get v
+ | _ -> raise Not_found
+
+(* Returns the list of kernel functions referred to by a "calls" annotation,
+ or raise exception Not_found if it is not a proper "calls" annotation. *)
+let get_calls_kf code_annot =
+ match code_annot.annot_content with
+ | AExtended (_, _, { ext_kind = Ext_terms terms }) -> List.map get_call terms
+ | _ -> raise Not_found
+
+(* Returns the "calls" annotations at statement [stmt]. *)
+let get_calls_annotations stmt =
+ let filter code_annot =
+ match code_annot.annot_content with
+ | AExtended (_, _, e) -> e.ext_name = "calls" && e.ext_has_status
+ | _ -> false
+ in
+ Annotations.code_annot ~filter stmt
+
+(* Checks one "calls" annotation [code_annot] at statement [stmt]. *)
+let check_calls_annotation stmt called_functions code_annot =
+ match get_calls_kf code_annot with
+ | exception Not_found ->
+ Self.warning ~current:true ~once:true
+ "Ignoring invalid calls annotation: %a"
+ Printer.pp_code_annotation code_annot;
+ called_functions
+ | kfs ->
+ let length = List.length called_functions in
+ let kfs = Kernel_function.Set.of_list kfs in
+ let is_call (kf, _) = Kernel_function.Set.mem kf kfs in
+ let called_functions = List.filter is_call called_functions in
+ let status =
+ match List.length called_functions with
+ | 0 -> Alarmset.False
+ | l when l = length -> Alarmset.True
+ | _ -> Alarmset.Unknown
+ in
+ let kf = Kernel_function.find_englobing_kf stmt in
+ emit_code_annot_status ~reduce:true ~empty:false kf stmt code_annot status;
+ called_functions
+
+let check_calls_annotations stmt called_functions =
+ let calls = get_calls_annotations stmt in
+ List.fold_left (check_calls_annotation stmt) called_functions calls
+
(* -------------------------------- Functor --------------------------------- *)
module type S = sig
@@ -392,7 +479,7 @@ module Make
the pre- and post-states. *)
let eval_and_reduce kf behavior active kind ips states build_prop build_env =
let limit = Eva_utils.get_slevel kf in
- let emit = emit_message_and_status kind kf behavior ~active in
+ let emit = emit_contract_status kind kf behavior ~active in
let aux_pred states pred =
let pr = Logic_const.pred_of_id_pred pred in
let record = pred.ip_content.tp_kind <> Admit in
@@ -534,30 +621,12 @@ module Make
let assumes = create_conjunction behavior.b_assumes in
Domain.evaluate_predicate pre_env state assumes
- let code_annotation_text ca =
- match ca.annot_content with
- | AAssert (_,{tp_kind}) -> Cil_printer.name_of_assert tp_kind
- | AInvariant _ -> "loop invariant"
- | APragma _ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
- | AExtended _ ->
- assert false (* currently not treated by Value *)
-
- (* location of the given code annotation. If unknown, use the location of the
- statement instead. *)
- let code_annotation_loc ca stmt =
- match Cil_datatype.Code_annotation.loc ca with
- | Some loc when not (Cil_datatype.Location.(equal loc unknown)) -> loc
- | _ -> Cil_datatype.Stmt.loc stmt
-
(* Reduce the given states according to the given code annotations.
If [record] is true, update the proof state of the code annotation.
DO NOT PASS record=false unless you know what your are doing *)
let interp_annot ~limit ~record kf ab stmt code_annot ~initial_state states =
- let ips = Property.ip_of_code_annot kf stmt code_annot in
- let source, _ = code_annotation_loc code_annot stmt in
let aux_interp ~record ~reduce code_annot behav p =
- let text = code_annotation_text code_annot in
let in_behavior =
match behav with
| [] -> `True
@@ -573,36 +642,13 @@ module Make
match in_behavior with
| `False -> states
| `True | `Unknown as in_behavior ->
- let emit status =
- let change_status st = List.iter (fun p -> emit_status p st) ips in
- let message =
- match status, in_behavior with
- | Alarmset.Unknown, _ ->
- change_status Property_status.Dont_know;
- "unknown"
- | Alarmset.True, _ ->
- change_status Property_status.True;
- "valid"
- | Alarmset.False, `True ->
- change_status Property_status.False_if_reachable;
- "invalid" ^ (if reduce then " (stopping propagation)" else "")
- | Alarmset.False, `Unknown ->
- change_status Property_status.False_if_reachable;
- "invalid"
- in
- msg_status status ~once:true ~source
- "%s%a got status %s." text Description.pp_named p message
- in
+ (* No reduction if the behavior might be inactive. *)
+ let reduce = reduce && in_behavior = `True in
+ let emit = emit_code_annot_status ~reduce ~empty:false kf stmt in
let reduce_state here res accstateset =
- match res, in_behavior with
- | _, `Unknown ->
- (* Cannot conclude because behavior might be inactive *)
- States.add here accstateset
-
- | Alarmset.False, `True -> (* Dead/invalid branch *)
- accstateset
-
- | (Alarmset.Unknown | Alarmset.True), `True ->
+ match res with
+ | Alarmset.False -> accstateset (* Dead/invalid branch *)
+ | Alarmset.Unknown | Alarmset.True ->
let env = here_env ~pre:initial_state ~here in
(* Reduce by p if it is a disjunction, or if it did not
evaluate to True *)
@@ -618,7 +664,7 @@ module Make
let env = here_env ~pre:initial_state ~here in
let res = Domain.evaluate_predicate env here p in
(* if [record] holds, emit kernel status and print a message *)
- if record then emit res;
+ if record then emit code_annot res;
(* if [reduce] holds, reduce the state. *)
if reduce then reduce_state here res accstateset else accstateset)
states States.empty
@@ -631,13 +677,9 @@ module Make
if ignore_predicate p then
states
else if States.is_empty states then (
- if record then begin
- let text = code_annotation_text code_annot in
- List.iter (fun p -> emit_status p Property_status.True) ips;
- msg_status Alarmset.True ~once:true ~source
- "no state left, %s%a got status valid."
- text Description.pp_named p;
- end;
+ if record then
+ emit_code_annot_status ~reduce:true ~empty:true
+ kf stmt code_annot Alarmset.True;
states
) else
aux_interp ~record ~reduce code_annot behav p
diff --git a/src/plugins/eva/engine/transfer_logic.mli b/src/plugins/eva/engine/transfer_logic.mli
index 38969a61a1fc9c5be16db705370f437549f8f2ae..5cce864ef90908be7a9c194f25e93d63da904c6b 100644
--- a/src/plugins/eva/engine/transfer_logic.mli
+++ b/src/plugins/eva/engine/transfer_logic.mli
@@ -27,6 +27,12 @@ open Eval
val process_inactive_behaviors:
kinstr -> kernel_function -> behavior list -> unit
+(* Checks "calls" annotations at the given statement according to the inferred
+ list of functions at this point. Reduces the given list to the functions
+ referred to by "calls" annotations. *)
+val check_calls_annotations:
+ stmt -> (kernel_function * 'a) list -> (kernel_function * 'a) list
+
module type S = sig
type state
type states
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 33fc8fc4c3abc07ded45489725070c179790d20e..f9e0d865b6134bdc577b419c581cd1b986b022d3 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -735,6 +735,8 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let cacheable = ref Cacheable in
let eval =
let+ functions = functions in
+ (* Check "calls" annotations, and reduce called functions accordingly. *)
+ let functions = Transfer_logic.check_calls_annotations stmt functions in
let process_one_function kf valuation =
(* The special Frama_C_ functions to print states are handled here. *)
if apply_special_directives ~subdivnb kf args state
diff --git a/tests/value/calls_annotation.i b/tests/value/calls_annotation.i
new file mode 100644
index 0000000000000000000000000000000000000000..3a9b799aa1dcca30aebad979fb7ff4e956b437a7
--- /dev/null
+++ b/tests/value/calls_annotation.i
@@ -0,0 +1,101 @@
+/* run.config*
+ STDOPT:
+*/
+
+/* This file tests the evaluation of the logical status of "calls" annotations,
+ and the reduction of called functions accordingly. */
+
+volatile unsigned int nondet;
+
+int incr(int x) {
+ return x+1;
+}
+
+int decr(int x) {
+ return x-1;
+}
+
+int square(int x) {
+ return x*x;
+}
+
+/* Should be never called according to "calls" annotations. */
+int error(int x) {
+ return x / 0;
+}
+
+int unreachable(int x) {
+ return 0;
+}
+
+typedef int (*fptr)(int);
+
+fptr funs[4] = { &incr, &decr, &square, &error };
+
+int apply(fptr fp, int a) {
+ int x;
+ //@ calls incr, decr, square; // unknown: error could also be called
+ x = (*fp)(a);
+ //@ calls incr, decr, square; // valid as consequence of the previous one
+ x = (*fp)(x);
+ return x;
+}
+
+void main(void) {
+ int a = 1, i = 0;
+
+ /* Valid "calls" annotations. */
+ //@ calls decr; // valid singleton
+ a = (*funs[1])(a);
+ i = nondet % 3;
+ //@ calls incr, decr, square; // valid
+ a = (*funs[i])(a);
+ //@ calls incr, decr, square, unreachable; // valid but contains unreachable
+ a = (*funs[i])(a);
+
+ /* Unknown "calls" annotations: Eva can reduce the called functions. */
+ i = nondet % 4;
+ //@ calls incr, decr; // unknown: square and error could also be called
+ a = (*funs[i])(a);
+ Frama_C_show_each_0_1(i); // i can be reduced to {0; 1}
+
+ /* Invalid "calls" annotations. */
+ if (nondet) {
+ //@ calls incr; // invalid
+ a = (*funs[1])(a);
+ Frama_C_show_each_UNREACHABLE();
+ }
+ if (nondet) {
+ i = nondet % 2;
+ //@ calls square, unreachable; // invalid
+ a = (*funs[i])(a);
+ Frama_C_show_each_UNREACHABLE(i);
+ }
+
+ /* "calls" annotations evaluated in multiple states. */
+ //@ loop unroll 4;
+ for (int j = 0; j < 4; j++) {
+ a = 0;
+ //@ calls incr; // valid at each iteration
+ a = (*funs[0])(a);
+ //@ calls incr, decr; // valid at each iteration
+ a = (*funs[j % 2])(a);
+ i = nondet % (j+1);
+ //@ calls incr, decr, square; // valid then unknown at the last iteration
+ a = (*funs[i])(a);
+ if (nondet) {
+ //@ calls incr, decr, square; // invalid at the last iteration
+ a = (*funs[j])(a);
+ if (j == 3) Frama_C_show_each_UNREACHABLE(j); // j == 3 is impossible here.
+ }
+ if (nondet) {
+ a = apply(funs[j], a); // invalid at the last iteration
+ if (j == 3) Frama_C_show_each_UNREACHABLE(j); // j == 3 is impossible here.
+ }
+ if (nondet) {
+ //@ calls unreachable; // invalid at each iteration
+ a = (*funs[j])(a);
+ Frama_C_show_each_UNREACHABLE(a);
+ }
+ }
+}
diff --git a/tests/value/oracle/calls_annotation.res.oracle b/tests/value/oracle/calls_annotation.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e22c92eeaa06b83e9ad93056ae0a1ba807bfda18
--- /dev/null
+++ b/tests/value/oracle/calls_annotation.res.oracle
@@ -0,0 +1,209 @@
+[kernel] Parsing calls_annotation.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 ∈ [--..--]
+ funs[0] ∈ {{ &incr }}
+ [1] ∈ {{ &decr }}
+ [2] ∈ {{ &square }}
+ [3] ∈ {{ &error }}
+[eva] calls_annotation.i:49: calls annotation got status valid.
+[eva] computing for function decr <- main.
+ Called from calls_annotation.i:49.
+[eva] Recording results for decr
+[eva] Done for function decr
+[eva] calls_annotation.i:52: calls annotation got status valid.
+[eva] computing for function square <- main.
+ Called from calls_annotation.i:52.
+[eva] Recording results for square
+[eva] Done for function square
+[eva] computing for function decr <- main.
+ Called from calls_annotation.i:52.
+[eva] Recording results for decr
+[eva] Done for function decr
+[eva] computing for function incr <- main.
+ Called from calls_annotation.i:52.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] calls_annotation.i:54: calls annotation got status valid.
+[eva] computing for function square <- main.
+ Called from calls_annotation.i:54.
+[eva] Recording results for square
+[eva] Done for function square
+[eva] computing for function decr <- main.
+ Called from calls_annotation.i:54.
+[eva] Recording results for decr
+[eva] Done for function decr
+[eva] computing for function incr <- main.
+ Called from calls_annotation.i:54.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva:alarm] calls_annotation.i:59: Warning: calls annotation got status unknown.
+[eva] computing for function decr <- main.
+ Called from calls_annotation.i:59.
+[eva] Recording results for decr
+[eva] Done for function decr
+[eva] computing for function incr <- main.
+ Called from calls_annotation.i:59.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] calls_annotation.i:60: Frama_C_show_each_0_1: {0; 1}
+[eva:alarm] calls_annotation.i:65: Warning:
+ calls annotation got status invalid (stopping propagation).
+[eva:alarm] calls_annotation.i:71: Warning:
+ calls annotation got status invalid (stopping propagation).
+[eva] calls_annotation.i:80: calls annotation got status valid.
+[eva] calls_annotation.i:80: Reusing old results for call to incr
+[eva] calls_annotation.i:82: calls annotation got status valid.
+[eva] computing for function incr <- main.
+ Called from calls_annotation.i:82.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] calls_annotation.i:85: calls annotation got status valid.
+[eva] computing for function incr <- main.
+ Called from calls_annotation.i:85.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] calls_annotation.i:88: calls annotation got status valid.
+[eva] computing for function incr <- main.
+ Called from calls_annotation.i:88.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] computing for function apply <- main.
+ Called from calls_annotation.i:92.
+[eva] calls_annotation.i:38: calls annotation got status valid.
+[eva] computing for function incr <- apply <- main.
+ Called from calls_annotation.i:38.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] calls_annotation.i:40: calls annotation got status valid.
+[eva] computing for function incr <- apply <- main.
+ Called from calls_annotation.i:40.
+[eva] Recording results for incr
+[eva] Done for function incr
+[eva] Recording results for apply
+[eva] Done for function apply
+[eva:alarm] calls_annotation.i:97: Warning:
+ calls annotation got status invalid (stopping propagation).
+[eva] calls_annotation.i:80: Reusing old results for call to incr
+[eva] calls_annotation.i:82: Reusing old results for call to decr
+[eva] calls_annotation.i:85: Reusing old results for call to decr
+[eva] calls_annotation.i:85: Reusing old results for call to incr
+[eva] computing for function decr <- main.
+ Called from calls_annotation.i:88.
+[eva] Recording results for decr
+[eva] Done for function decr
+[eva] computing for function apply <- main.
+ Called from calls_annotation.i:92.
+[eva] computing for function decr <- apply <- main.
+ Called from calls_annotation.i:38.
+[eva] Recording results for decr
+[eva] Done for function decr
+[eva] computing for function decr <- apply <- main.
+ Called from calls_annotation.i:40.
+[eva] Recording results for decr
+[eva] Done for function decr
+[eva] Recording results for apply
+[eva] Done for function apply
+[eva] calls_annotation.i:80: Reusing old results for call to incr
+[eva] calls_annotation.i:82: Reusing old results for call to incr
+[eva] computing for function square <- main.
+ Called from calls_annotation.i:85.
+[eva] Recording results for square
+[eva] Done for function square
+[eva] computing for function decr <- main.
+ Called from calls_annotation.i:85.
+[eva] Recording results for decr
+[eva] Done for function decr
+[eva] calls_annotation.i:85: Reusing old results for call to incr
+[eva] computing for function square <- main.
+ Called from calls_annotation.i:88.
+[eva] Recording results for square
+[eva] Done for function square
+[eva] computing for function apply <- main.
+ Called from calls_annotation.i:92.
+[eva] computing for function square <- apply <- main.
+ Called from calls_annotation.i:38.
+[eva] Recording results for square
+[eva] Done for function square
+[eva] computing for function square <- apply <- main.
+ Called from calls_annotation.i:40.
+[eva] Recording results for square
+[eva] Done for function square
+[eva] Recording results for apply
+[eva] Done for function apply
+[eva] calls_annotation.i:80: Reusing old results for call to incr
+[eva] calls_annotation.i:82: Reusing old results for call to decr
+[eva:alarm] calls_annotation.i:85: Warning: calls annotation got status unknown.
+[eva] calls_annotation.i:85: Reusing old results for call to square
+[eva] calls_annotation.i:85: Reusing old results for call to decr
+[eva] calls_annotation.i:85: Reusing old results for call to incr
+[eva:alarm] calls_annotation.i:88: Warning:
+ calls annotation got status invalid (stopping propagation).
+[eva] computing for function apply <- main.
+ Called from calls_annotation.i:92.
+[eva:alarm] calls_annotation.i:38: Warning:
+ calls annotation got status invalid (stopping propagation).
+[eva] Recording results for apply
+[eva] Done for function apply
+[eva] Recording results for main
+[eva] Done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function decr:
+ __retres ∈ {-4; -3; -2; -1; 0; 1}
+[eva:final-states] Values at end of function incr:
+ __retres ∈ {-1; 0; 1; 2; 3; 4; 5; 6}
+[eva:final-states] Values at end of function square:
+ __retres ∈ [-1..65536]
+[eva:final-states] Values at end of function apply:
+ x ∈ [-4..65536]
+[eva:final-states] Values at end of function main:
+ a ∈ {-1; 0; 1}
+ i ∈ {0; 1; 2}
+[from] Computing for function decr
+[from] Done for function decr
+[from] Computing for function incr
+[from] Done for function incr
+[from] Computing for function square
+[from] Done for function square
+[from] Computing for function apply
+[from] Computing for function error <-apply
+[from] Non-terminating function error (no dependencies)
+[from] Done for function error
+[from] Done for function apply
+[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 decr:
+ \result FROM x
+[from] Function incr:
+ \result FROM x
+[from] Function square:
+ \result FROM x
+[from] Function apply:
+ \result FROM fp; a
+[from] Function main:
+ NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function decr:
+ __retres
+[inout] Inputs for function decr:
+ \nothing
+[inout] Out (internal) for function incr:
+ __retres
+[inout] Inputs for function incr:
+ \nothing
+[inout] Out (internal) for function square:
+ __retres
+[inout] Inputs for function square:
+ \nothing
+[inout] Out (internal) for function apply:
+ x
+[inout] Inputs for function apply:
+ \nothing
+[inout] Out (internal) for function main:
+ a; i; j
+[inout] Inputs for function main:
+ nondet; funs[0..3]
diff --git a/tests/value/oracle_apron/calls_annotation.res.oracle b/tests/value/oracle_apron/calls_annotation.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..2b7f3f96a5e0decd5fd44facaedf808dd051fd07
--- /dev/null
+++ b/tests/value/oracle_apron/calls_annotation.res.oracle
@@ -0,0 +1,81 @@
+57c57,60
+< [eva] calls_annotation.i:80: Reusing old results for call to incr
+---
+> [eva] computing for function incr <- main.
+> Called from calls_annotation.i:80.
+> [eva] Recording results for incr
+> [eva] Done for function incr
+89,92c92,107
+< [eva] calls_annotation.i:80: Reusing old results for call to incr
+< [eva] calls_annotation.i:82: Reusing old results for call to decr
+< [eva] calls_annotation.i:85: Reusing old results for call to decr
+< [eva] calls_annotation.i:85: Reusing old results for call to incr
+---
+> [eva] computing for function incr <- main.
+> Called from calls_annotation.i:80.
+> [eva] Recording results for incr
+> [eva] Done for function incr
+> [eva] computing for function decr <- main.
+> Called from calls_annotation.i:82.
+> [eva] Recording results for decr
+> [eva] Done for function decr
+> [eva] computing for function decr <- main.
+> Called from calls_annotation.i:85.
+> [eva] Recording results for decr
+> [eva] Done for function decr
+> [eva] computing for function incr <- main.
+> Called from calls_annotation.i:85.
+> [eva] Recording results for incr
+> [eva] Done for function incr
+109,110c124,131
+< [eva] calls_annotation.i:80: Reusing old results for call to incr
+< [eva] calls_annotation.i:82: Reusing old results for call to incr
+---
+> [eva] computing for function incr <- main.
+> Called from calls_annotation.i:80.
+> [eva] Recording results for incr
+> [eva] Done for function incr
+> [eva] computing for function incr <- main.
+> Called from calls_annotation.i:82.
+> [eva] Recording results for incr
+> [eva] Done for function incr
+119c140,143
+< [eva] calls_annotation.i:85: Reusing old results for call to incr
+---
+> [eva] computing for function incr <- main.
+> Called from calls_annotation.i:85.
+> [eva] Recording results for incr
+> [eva] Done for function incr
+136,137c160,167
+< [eva] calls_annotation.i:80: Reusing old results for call to incr
+< [eva] calls_annotation.i:82: Reusing old results for call to decr
+---
+> [eva] computing for function incr <- main.
+> Called from calls_annotation.i:80.
+> [eva] Recording results for incr
+> [eva] Done for function incr
+> [eva] computing for function decr <- main.
+> Called from calls_annotation.i:82.
+> [eva] Recording results for decr
+> [eva] Done for function decr
+139,141c169,180
+< [eva] calls_annotation.i:85: Reusing old results for call to square
+< [eva] calls_annotation.i:85: Reusing old results for call to decr
+< [eva] calls_annotation.i:85: Reusing old results for call to incr
+---
+> [eva] computing for function square <- main.
+> Called from calls_annotation.i:85.
+> [eva] Recording results for square
+> [eva] Done for function square
+> [eva] computing for function decr <- main.
+> Called from calls_annotation.i:85.
+> [eva] Recording results for decr
+> [eva] Done for function decr
+> [eva] computing for function incr <- main.
+> Called from calls_annotation.i:85.
+> [eva] Recording results for incr
+> [eva] Done for function incr
+158c197
+< __retres ∈ [-1..65536]
+---
+> __retres ∈ [0..65536]