Skip to content
Snippets Groups Projects
Commit e821b903 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

Merge branch 'feature/eva/calls-evaluation' into 'master' 

[Eva] Support "calls" ACSL extensions

See merge request frama-c/frama-c!4715
parents 0147629f d11bea83
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/eva/engine/transfer_logic.ml
+ 128
− 86
View file @ e821b903
......@@ -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
......
src/plugins/eva/engine/transfer_logic.mli
+ 6
− 0
View file @ e821b903
......@@ -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
......
src/plugins/eva/engine/transfer_stmt.ml
+ 2
− 0
View file @ e821b903
......@@ -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
......
tests/value/calls_annotation.i 0 → 100644
+ 101
− 0
View file @ e821b903
/* 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);
}
}
}
tests/value/oracle/calls_annotation.res.oracle 0 → 100644
+ 209
− 0
View file @ e821b903
[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]
tests/value/oracle_apron/calls_annotation.res.oracle 0 → 100644
+ 81
− 0
View file @ e821b903
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]
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment