diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml index 22a066c82e..f92f531f0d 100644 --- a/src/arg/myARG.ml +++ b/src/arg/myARG.ml @@ -156,7 +156,7 @@ struct | n :: stack -> let cfgnode = Arg.Node.cfgnode n in match cfgnode with - | Function _ -> (* TODO: can this be done without cfgnode? *) + | Function cfgnode_fd -> (* TODO: can this be done without cfgnode? *) begin match stack with (* | [] -> failwith "StackArg.next: return stack empty" *) | [] -> [] (* main return *) @@ -171,14 +171,33 @@ struct | _ -> None ) in + let (entry_lval, entry_args) = + Arg.next call_n + (* filter because infinite loops starting with function call + will have another Neg(1) edge from the head *) + |> List.filter_map (fun (edge, to_n) -> + match edge with + | InlineEntry (lval, _, args) -> Some (lval, args) + | _ -> None + ) + |> List.sort_uniq [%ord: CilType.Lval.t option * CilType.Exp.t list] (* TODO: deduplicate unique element in O(n) *) + |> (function + | [lval_args] -> lval_args + | _ -> assert false (* all calls from a node must have same args and lval, even if called function might be different via function pointer *) + ) + in Arg.next n |> List.filter_map (fun (edge, to_n) -> - if BatList.mem_cmp Arg.Node.compare to_n call_next then ( - let to_n' = to_n :: call_stack in - Some (edge, to_n') - ) - else - None + match edge with + | InlineReturn (lval, fd, args) -> + assert (CilType.Fundec.equal fd cfgnode_fd); (* fd in return node should be the same as in InlineReturn edge *) + if BatList.mem_cmp Arg.Node.compare to_n call_next && [%eq: CilType.Lval.t option] lval entry_lval && [%eq: CilType.Exp.t list] args entry_args then ( + let to_n' = to_n :: call_stack in + Some (edge, to_n') + ) + else + None + | _ -> assert false ) end | _ -> diff --git a/tests/sv-comp/basic/if_trier_exclude_multiple_false-unreach-call.c b/tests/sv-comp/basic/if_trier_exclude_multiple_false-unreach-call.c index 7af8b4e967..e021ff930d 100644 --- a/tests/sv-comp/basic/if_trier_exclude_multiple_false-unreach-call.c +++ b/tests/sv-comp/basic/if_trier_exclude_multiple_false-unreach-call.c @@ -25,6 +25,5 @@ int main() __VERIFIER_assert(x != 1); } } - // TODO: double InlineReturn edge in two first cases? return 0; } \ No newline at end of file diff --git a/tests/sv-comp/basic/if_trier_exclude_multiple_false-unreach-call.expected b/tests/sv-comp/basic/if_trier_exclude_multiple_false-unreach-call.expected index eac27d1d8f..f6b7ec87e8 100644 --- a/tests/sv-comp/basic/if_trier_exclude_multiple_false-unreach-call.expected +++ b/tests/sv-comp/basic/if_trier_exclude_multiple_false-unreach-call.expected @@ -1,90 +1,87 @@ - - ┌························································································································┐ - : : - : ┌────────────────────────────────────────┐ : - : │ _ │ : - : └────────────────────────────────────────┘ : - : │ : - : │ Entry main : Inlined Proc '__VERIFIER_assert(x == 0)' - : ▼ ▼ - : InlineReturn ┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ Inlined Proc '__VERIFIER_assert(x != 1)' ┌──────────────────────┐ InlineEntry '(x != 1)' ┌────────────────────────────────┐ - ┌────┼──────────────────────────────────────────────────────────────────────────▶ │ │ ◀·········································· │ _ │ ────────────────────────▶ │ _ │ - │ : │ │ └──────────────────────┘ └────────────────────────────────┘ - │ : InlineReturn │ │ InlineReturn ▲ │ - │ : ┌────────────────────────────────────────▶ │ _ │ ◀─────────────────────────────────────────────┼───────────────────────┐ │ Entry __VERIFIER_assert - │ : │ │ │ │ │ ▼ - │ : │ │ │ │ │ ┌────────────────────────────────┐ Test (! cond,true) ┌─────────────────────────┐ - │ : │ ┌────────────▶ │ │ ◀┐ │ │ │ _ │ ────────────────────▶ │ _ │ - │ : │ │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ │ │ │ └────────────────────────────────┘ └─────────────────────────┘ - │ : │ │ │ ▲ │ │ Test (x == 2,false) │ │ │ - │ : │ │ │ Test (1,true) : Inlined Proc '__VERIFIER_assert(x == 2)' │ InlineReturn │ │ │ Test (! cond,false) │ InlineEntry '()' - │ : │ │ ▼ : │ │ │ ▼ ▼ - │ : │ │ ┌────────────────────────────────────────┐ : │ │ │ ┌────────────────────────────────┐ ┌─────────────────────────┐ - │ : │ │ │ _ │ ·┐ ┌────┼────────────────────────────────────────────┼────────────────────────────────────────────┘ │ │ _ │ │ _ │ - │ : │ │ └────────────────────────────────────────┘ : │ : │ │ └────────────────────────────────┘ └─────────────────────────┘ - │ : │ │ │ : │ : │ │ │ │ - │ : │ │ │ InlineEntry '()' : │ : │ │ │ Ret (None, __VERIFIER_assert) │ Entry __VERIFIER_error - │ : │ │ ▼ : │ : │ │ ▼ ▼ - │ : │ │ ┌────────────────────────────────────────┐ : │ : │ │ ┌────────────────────────────────┐ ┌─────────────────────────┐ - │ : │ │ │ _ │ : │ : │ └─────────────────────── │ _ │ │ _ │ - │ : │ │ └────────────────────────────────────────┘ : │ : │ └────────────────────────────────┘ └─────────────────────────┘ - │ : │ │ │ : │ : │ - │ : │ │ │ Entry __VERIFIER_nondet_int : │ : │ - │ : │ │ ▼ : │ : │ - │ : │ │ ┌────────────────────────────────────────┐ : │ : │ - │ : │ │ InlineReturn │ _ │ : Inlined Proc 'tmp = __VERIFIER_nondet_int()' │ : │ - │ : │ │ └────────────────────────────────────────┘ : │ : │ - │ : │ │ │ : │ : │ - │ : │ │ │ Ret (Some val, __VERIFIER_nondet_int) : │ : │ - │ : │ │ ▼ : │ : │ - │ : │ │ ┌────────────────────────────────────────┐ : │ : │ - │ : │ │ │ _ │ : │ : │ - │ : │ │ └────────────────────────────────────────┘ : │ : │ - │ : │ │ │ : │ : │ - │ : │ │ │ InlineReturn 'tmp' : │ : │ - │ : │ │ ▼ : │ : │ - │ : │ │ ┌────────────────────────────────────────┐ : │ : │ - │ : │ │ │ _ │ ◀┘ │ : │ - │ : │ │ └────────────────────────────────────────┘ │ : │ - │ : │ │ │ │ : │ - │ : │ │ │ Assign 'x = tmp' │ : │ - │ : │ │ ▼ │ : │ - │ ┌────────────────────────────────┐ │ Test (x == 0,true) │ ┌────────────────────────────────────────┐ │ : │ - │ │ _ │ ◀┼───────────────────────────┼───────────── │ _ │ │ : │ - │ └────────────────────────────────┘ │ │ └────────────────────────────────────────┘ │ : │ - │ │ │ │ │ │ : │ - │ │ InlineEntry '(x == 0)' │ │ │ Test (x == 0,false) │ : │ - │ ▼ │ │ ▼ │ : │ - │ ┌────────────────────────────────┐ │ │ ┌────────────────────────────────────────┐ │ : │ - │ │ _ │ │ │ │ _ │ ──────────────────────────────────────────────────┘ : │ - │ └────────────────────────────────┘ │ │ └────────────────────────────────────────┘ : │ - │ │ │ │ │ : │ - │ │ Entry __VERIFIER_assert │ │ │ Test (x == 2,true) : │ - │ ▼ │ │ ▼ : │ - │ ┌────────────────────────────────┐ │ │ ┌────────────────────────────────────────┐ : │ - │ │ _ │ │ │ │ _ │ ·······················································┘ │ - │ └────────────────────────────────┘ │ │ └────────────────────────────────────────┘ │ - │ │ │ │ │ │ - │ │ Test (! cond,false) │ │ │ InlineEntry '(x == 2)' │ - │ ▼ │ │ ▼ │ - │ ┌────────────────────────────────┐ │ │ ┌────────────────────────────────────────┐ │ - │ │ _ │ │ │ │ _ │ │ - │ └────────────────────────────────┘ │ │ └────────────────────────────────────────┘ │ - │ │ │ │ │ │ - │ │ Ret (None, __VERIFIER_assert) │ │ │ Entry __VERIFIER_assert │ - │ ▼ │ │ ▼ │ - │ ┌────────────────────────────────┐ │ │ ┌────────────────────────────────────────┐ │ - └─ │ _ │ ─┘ │ │ _ │ │ - └────────────────────────────────┘ │ └────────────────────────────────────────┘ │ - │ │ │ - │ │ Test (! cond,false) │ - │ ▼ │ - │ ┌────────────────────────────────────────┐ │ - │ │ _ │ │ - │ └────────────────────────────────────────┘ │ - │ │ │ - │ │ Ret (None, __VERIFIER_assert) │ - │ ▼ │ - │ ┌────────────────────────────────────────┐ │ - └───────────── │ _ │ ────────────────────────────────────────────────────────────────────────────────────────────────────┘ - └────────────────────────────────────────┘ + ┌────────────────────────────────────────┐ + │ _ │ + └────────────────────────────────────────┘ + │ + │ Entry main + ▼ + Inlined Proc '__VERIFIER_assert(x == 0)' ┌──────────────────────────────────────────────────────────────────────────────────────────────┐ Inlined Proc '__VERIFIER_assert(x != 1)' ┌──────────────────────┐ InlineEntry '(x != 1)' ┌────────────────────────────────┐ + ┌······································································································▶ │ │ ◀·········································· │ _ │ ────────────────────────▶ │ _ │ + : │ │ └──────────────────────┘ └────────────────────────────────┘ + : InlineReturn │ │ InlineReturn ▲ │ + : ┌────────────────────────────────────────────────────────────────────▶ │ _ │ ◀─────────────────────────────────────────────┼───────────────────────┐ │ Entry __VERIFIER_assert + : │ │ │ │ │ ▼ + : │ │ │ │ │ ┌────────────────────────────────┐ Test (! cond,true) ┌─────────────────────────┐ + : │ ┌········································▶ │ │ ◀┐ │ │ │ _ │ ────────────────────▶ │ _ │ + : │ : └──────────────────────────────────────────────────────────────────────────────────────────────┘ │ │ │ └────────────────────────────────┘ └─────────────────────────┘ + : │ : │ │ │ Test (x == 2,false) │ │ │ + : │ : │ Test (1,true) │ InlineReturn │ │ │ Test (! cond,false) │ InlineEntry '()' + : │ : ▼ │ │ │ ▼ ▼ + : │ : ┌────────────────────────────────────────┐ │ │ │ ┌────────────────────────────────┐ ┌─────────────────────────┐ + : │ : │ _ │ ·┐ ┌────┼────────────────────────────────────────────┘ │ │ _ │ │ _ │ + : │ : └────────────────────────────────────────┘ : │ │ │ └────────────────────────────────┘ └─────────────────────────┘ + : │ : │ : │ │ │ │ │ + : │ : │ InlineEntry '()' : │ │ │ │ Ret (None, __VERIFIER_assert) │ Entry __VERIFIER_error + : │ : ▼ : │ │ │ ▼ ▼ + : │ : ┌────────────────────────────────────────┐ : │ │ │ ┌────────────────────────────────┐ ┌─────────────────────────┐ + : │ : │ _ │ : │ │ └─────────────────────── │ _ │ │ _ │ + : │ : └────────────────────────────────────────┘ : │ │ └────────────────────────────────┘ └─────────────────────────┘ + : │ : │ : │ │ + : │ : │ Entry __VERIFIER_nondet_int : │ │ + : │ : ▼ : │ │ + : │ : ┌────────────────────────────────────────┐ : │ │ + : │ : Inlined Proc '__VERIFIER_assert(x == 2)' │ _ │ : Inlined Proc 'tmp = __VERIFIER_nondet_int()' │ │ + : │ : └────────────────────────────────────────┘ : │ │ + : │ : │ : │ │ + : │ : │ Ret (Some val, __VERIFIER_nondet_int) : │ │ + : │ : ▼ : │ │ + : │ : ┌────────────────────────────────────────┐ : │ │ + : │ : │ _ │ : │ │ + : │ : └────────────────────────────────────────┘ : │ │ + : │ : │ : │ │ + : │ : │ InlineReturn 'tmp' : │ │ + : │ : ▼ : │ │ + : │ : ┌────────────────────────────────────────┐ : │ │ + : │ : │ _ │ ◀┘ │ │ + : │ : └────────────────────────────────────────┘ │ │ + : │ : │ │ │ + : │ : │ Assign 'x = tmp' │ │ + : │ : ▼ │ │ +┌────────────────────────────────┐ │ Test (x == 0,true) : ┌────────────────────────────────────────┐ │ │ +│ _ │ ◀┼───────────────────────────┼───────────────────────────────────────── │ _ │ │ │ +└────────────────────────────────┘ │ : └────────────────────────────────────────┘ │ │ + │ │ : │ │ │ + │ InlineEntry '(x == 0)' │ : │ Test (x == 0,false) │ │ + ▼ │ : ▼ │ │ +┌────────────────────────────────┐ │ : ┌────────────────────────────────────────┐ │ │ +│ _ │ │ : │ _ │ ──────────────────────────────────────────────────┘ │ +└────────────────────────────────┘ │ : └────────────────────────────────────────┘ │ + │ │ : │ │ + │ Entry __VERIFIER_assert │ : │ Test (x == 2,true) │ + ▼ │ : ▼ │ +┌────────────────────────────────┐ │ : ┌────────────────────────────────────────┐ │ +│ _ │ │ └········································· │ _ │ │ +└────────────────────────────────┘ │ └────────────────────────────────────────┘ │ + │ │ │ │ + │ Test (! cond,false) │ │ InlineEntry '(x == 2)' │ + ▼ │ ▼ │ +┌────────────────────────────────┐ │ ┌────────────────────────────────────────┐ │ +│ _ │ │ │ _ │ │ +└────────────────────────────────┘ │ └────────────────────────────────────────┘ │ + │ │ │ │ + │ Ret (None, __VERIFIER_assert) │ │ Entry __VERIFIER_assert │ + ▼ │ ▼ │ +┌────────────────────────────────┐ │ ┌────────────────────────────────────────┐ │ +│ _ │ ─┘ │ _ │ │ +└────────────────────────────────┘ └────────────────────────────────────────┘ │ + │ │ + │ Test (! cond,false) │ + ▼ │ + ┌────────────────────────────────────────┐ │ + │ _ │ │ + └────────────────────────────────────────┘ │ + │ │ + │ Ret (None, __VERIFIER_assert) │ + ▼ │ + ┌────────────────────────────────────────┐ │ + │ _ │ ───────────────────────────────────────────────────────┘ + └────────────────────────────────────────┘ diff --git a/tests/sv-comp/basic/if_trier_exclude_multiple_true-unreach-call.c b/tests/sv-comp/basic/if_trier_exclude_multiple_true-unreach-call.c index 434b6b29fb..83994c2be7 100644 --- a/tests/sv-comp/basic/if_trier_exclude_multiple_true-unreach-call.c +++ b/tests/sv-comp/basic/if_trier_exclude_multiple_true-unreach-call.c @@ -25,6 +25,5 @@ int main() __VERIFIER_assert(x != 0 && x != 2); } } - // TODO: double InlineReturn edge in two first cases? return 0; } \ No newline at end of file diff --git a/tests/sv-comp/basic/if_trier_exclude_multiple_true-unreach-call.expected b/tests/sv-comp/basic/if_trier_exclude_multiple_true-unreach-call.expected index e61915e598..9242e947ca 100644 --- a/tests/sv-comp/basic/if_trier_exclude_multiple_true-unreach-call.expected +++ b/tests/sv-comp/basic/if_trier_exclude_multiple_true-unreach-call.expected @@ -1,96 +1,93 @@ - - ┌························································································································┐ - : : - : ┌────────────────────────────────────────┐ : - : │ _ │ : - : └────────────────────────────────────────┘ : - : │ : InlineReturn - : │ Entry main : Inlined Proc '__VERIFIER_assert(x == 0)' ┌───────────────────────────────────────────────────────────────────────────────────────────────┐ - : ▼ ▼ ▼ │ - : InlineReturn ┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ Inlined Proc '__VERIFIER_assert(x == 2)' ┌────────────────────────────────┐ │ - ┌────┼──────────────────────────────────────────────────────────────────────────▶ │ │ ◀·········································· │ _ │ ◀┼────┐ - │ : │ │ └────────────────────────────────┘ │ │ - │ : InlineReturn │ │ │ │ │ - │ : ┌────────────────────────────────────────▶ │ _ │ │ InlineEntry '(x == 2)' │ │ - │ : │ │ │ ▼ │ │ - │ : │ │ │ ┌────────────────────────────────┐ │ │ - │ : │ ┌────────────▶ │ │ │ _ │ │ │ - │ : │ │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ └────────────────────────────────┘ │ │ - │ : │ │ │ ▲ ▲ │ │ │ - │ : │ │ │ Test (1,true) : Inlined Proc '__VERIFIER_assert(tmp___0)' │ InlineReturn │ Entry __VERIFIER_assert │ │ - │ : │ │ ▼ : │ ▼ │ │ - │ : │ │ ┌────────────────────────────────────────┐ : │ ┌────────────────────────────────┐ │ │ - │ : │ │ │ _ │ ·┐ : │ │ _ │ │ │ - │ : │ │ └────────────────────────────────────────┘ : : │ └────────────────────────────────┘ │ │ - │ : │ │ │ : : │ │ │ │ - │ : │ │ │ InlineEntry '()' : : │ │ Test (! cond,false) │ │ - │ : │ │ ▼ : : │ ▼ │ │ - │ : │ │ ┌────────────────────────────────────────┐ : : │ ┌────────────────────────────────┐ │ │ - │ : │ │ │ _ │ : : │ │ _ │ │ │ - │ : │ │ └────────────────────────────────────────┘ : : │ └────────────────────────────────┘ │ │ - │ : │ │ │ : : │ │ │ │ - │ : │ │ │ Entry __VERIFIER_nondet_int : : │ │ Ret (None, __VERIFIER_assert) │ │ - │ : │ │ ▼ : : │ ▼ │ │ - │ : │ │ ┌────────────────────────────────────────┐ : : │ ┌────────────────────────────────┐ │ │ - │ : │ │ InlineReturn │ _ │ : Inlined Proc 'tmp = __VERIFIER_nondet_int()' : └────────────────────────────────────────────────────────── │ _ │ ─┘ │ Test (x == 2,true) - │ : │ │ └────────────────────────────────────────┘ : : └────────────────────────────────┘ │ - │ : │ │ │ : : │ - │ : │ │ │ Ret (Some val, __VERIFIER_nondet_int) : : │ - │ : │ │ ▼ : : │ - │ : │ │ ┌────────────────────────────────────────┐ : : │ - │ : │ │ │ _ │ : : │ - │ : │ │ └────────────────────────────────────────┘ : : │ - │ : │ │ │ : : │ - │ : │ │ │ InlineReturn 'tmp' : : │ - │ : │ │ ▼ : : │ - │ : │ │ ┌────────────────────────────────────────┐ : : │ - │ : │ │ │ _ │ ◀┘ : │ - │ : │ │ └────────────────────────────────────────┘ : │ - │ : │ │ │ : │ - │ : │ │ │ Assign 'x = tmp' : │ - │ : │ │ ▼ : │ - │ ┌────────────────────────────────┐ │ Test (x == 0,true) │ ┌────────────────────────────────────────┐ : │ - │ │ _ │ ◀┼───────────────────────────┼───────────── │ _ │ : │ - │ └────────────────────────────────┘ │ │ └────────────────────────────────────────┘ : │ - │ │ │ │ │ : │ - │ │ InlineEntry '(x == 0)' │ │ │ Test (x == 0,false) : │ - │ ▼ │ │ ▼ : │ - │ ┌────────────────────────────────┐ │ │ ┌────────────────────────────────────────┐ : │ - │ │ _ │ │ │ │ _ │ ──────────────────────────────────────────────────┼──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ - │ └────────────────────────────────┘ │ │ └────────────────────────────────────────┘ : - │ │ │ │ │ : - │ │ Entry __VERIFIER_assert │ │ │ Test (x == 2,false) : - │ ▼ │ │ ▼ : - │ ┌────────────────────────────────┐ │ │ ┌────────────────────────────────────────┐ : - │ │ _ │ │ │ │ _ │ : - │ └────────────────────────────────┘ │ │ └────────────────────────────────────────┘ : - │ │ │ │ │ : - │ │ Test (! cond,false) │ │ │ Assign 'tmp___0 = x != 0 && x != 2' : - │ ▼ │ │ ▼ : - │ ┌────────────────────────────────┐ │ │ ┌────────────────────────────────────────┐ : - │ │ _ │ │ │ │ _ │ ··················································┘ - │ └────────────────────────────────┘ │ │ └────────────────────────────────────────┘ - │ │ │ │ │ - │ │ Ret (None, __VERIFIER_assert) │ │ │ InlineEntry '(tmp___0)' - │ ▼ │ │ ▼ - │ ┌────────────────────────────────┐ │ │ ┌────────────────────────────────────────┐ - └─ │ _ │ ─┘ │ │ _ │ - └────────────────────────────────┘ │ └────────────────────────────────────────┘ - │ │ - │ │ Entry __VERIFIER_assert - │ ▼ - │ ┌────────────────────────────────────────┐ - │ │ _ │ - │ └────────────────────────────────────────┘ - │ │ - │ │ Test (! cond,false) - │ ▼ - │ ┌────────────────────────────────────────┐ - │ │ _ │ - │ └────────────────────────────────────────┘ - │ │ - │ │ Ret (None, __VERIFIER_assert) - │ ▼ - │ ┌────────────────────────────────────────┐ - └───────────── │ _ │ - └────────────────────────────────────────┘ + ┌────────────────────────────────────────┐ + │ _ │ + └────────────────────────────────────────┘ + │ + │ Entry main + ▼ + Inlined Proc '__VERIFIER_assert(x == 0)' ┌──────────────────────────────────────────────────────────────────────────────────────────────┐ Inlined Proc '__VERIFIER_assert(x == 2)' ┌─────────────────────┐ InlineEntry '(x == 2)' ┌────────────────────────────────┐ + ┌·······································································································▶ │ │ ◀·········································· │ _ │ ────────────────────────▶ │ _ │ + : │ │ └─────────────────────┘ └────────────────────────────────┘ + : InlineReturn │ │ InlineReturn ▲ │ + : ┌─────────────────────────────────────────────────────────────────────▶ │ _ │ ◀─────────────────────────────────────────────┼──────────────────────┐ │ Entry __VERIFIER_assert + : │ │ │ │ │ ▼ + : │ │ │ │ │ ┌────────────────────────────────┐ + : │ ┌·········································▶ │ │ ◀┐ │ │ │ _ │ + : │ : └──────────────────────────────────────────────────────────────────────────────────────────────┘ │ │ │ └────────────────────────────────┘ + : │ : │ │ │ Test (x == 2,true) │ │ + : │ : │ Test (1,true) │ InlineReturn │ │ │ Test (! cond,false) + : │ : ▼ │ │ │ ▼ + : │ : ┌────────────────────────────────────────┐ │ │ │ ┌────────────────────────────────┐ + : │ : │ _ │ ·┐ ┌────┼────────────────────────────────────────────┘ │ │ _ │ + : │ : └────────────────────────────────────────┘ : │ │ │ └────────────────────────────────┘ + : │ : │ : │ │ │ │ + : │ : │ InlineEntry '()' : │ │ │ │ Ret (None, __VERIFIER_assert) + : │ : ▼ : │ │ │ ▼ + : │ : ┌────────────────────────────────────────┐ : │ │ │ ┌────────────────────────────────┐ + : │ : │ _ │ : │ │ └─────────────────────── │ _ │ + : │ : └────────────────────────────────────────┘ : │ │ └────────────────────────────────┘ + : │ : │ : │ │ + : │ : │ Entry __VERIFIER_nondet_int : │ │ + : │ : ▼ : │ │ + : │ : ┌────────────────────────────────────────┐ : │ │ + : │ : Inlined Proc '__VERIFIER_assert(tmp___0)' │ _ │ : Inlined Proc 'tmp = __VERIFIER_nondet_int()' │ │ + : │ : └────────────────────────────────────────┘ : │ │ + : │ : │ : │ │ + : │ : │ Ret (Some val, __VERIFIER_nondet_int) : │ │ + : │ : ▼ : │ │ + : │ : ┌────────────────────────────────────────┐ : │ │ + : │ : │ _ │ : │ │ + : │ : └────────────────────────────────────────┘ : │ │ + : │ : │ : │ │ + : │ : │ InlineReturn 'tmp' : │ │ + : │ : ▼ : │ │ + : │ : ┌────────────────────────────────────────┐ : │ │ + : │ : │ _ │ ◀┘ │ │ + : │ : └────────────────────────────────────────┘ │ │ + : │ : │ │ │ + : │ : │ Assign 'x = tmp' │ │ + : │ : ▼ │ │ +┌────────────────────────────────┐ │ Test (x == 0,true) : ┌────────────────────────────────────────┐ │ │ +│ _ │ ◀┼───────────────────────────┼────────────────────────────────────────── │ _ │ │ │ +└────────────────────────────────┘ │ : └────────────────────────────────────────┘ │ │ + │ │ : │ │ │ + │ InlineEntry '(x == 0)' │ : │ Test (x == 0,false) │ │ + ▼ │ : ▼ │ │ +┌────────────────────────────────┐ │ : ┌────────────────────────────────────────┐ │ │ +│ _ │ │ : │ _ │ ──────────────────────────────────────────────────┘ │ +└────────────────────────────────┘ │ : └────────────────────────────────────────┘ │ + │ │ : │ │ + │ Entry __VERIFIER_assert │ : │ Test (x == 2,false) │ + ▼ │ : ▼ │ +┌────────────────────────────────┐ │ : ┌────────────────────────────────────────┐ │ +│ _ │ │ : │ _ │ │ +└────────────────────────────────┘ │ : └────────────────────────────────────────┘ │ + │ │ : │ │ + │ Test (! cond,false) │ : │ Assign 'tmp___0 = x != 0 && x != 2' │ + ▼ │ : ▼ │ +┌────────────────────────────────┐ │ : ┌────────────────────────────────────────┐ │ +│ _ │ │ └·········································· │ _ │ │ +└────────────────────────────────┘ │ └────────────────────────────────────────┘ │ + │ │ │ │ + │ Ret (None, __VERIFIER_assert) │ │ InlineEntry '(tmp___0)' │ + ▼ │ ▼ │ +┌────────────────────────────────┐ │ ┌────────────────────────────────────────┐ │ +│ _ │ ─┘ │ _ │ │ +└────────────────────────────────┘ └────────────────────────────────────────┘ │ + │ │ + │ Entry __VERIFIER_assert │ + ▼ │ + ┌────────────────────────────────────────┐ │ + │ _ │ │ + └────────────────────────────────────────┘ │ + │ │ + │ Test (! cond,false) │ + ▼ │ + ┌────────────────────────────────────────┐ │ + │ _ │ │ + └────────────────────────────────────────┘ │ + │ │ + │ Ret (None, __VERIFIER_assert) │ + ▼ │ + ┌────────────────────────────────────────┐ │ + │ _ │ ───────────────────────────────────────────────────────┘ + └────────────────────────────────────────┘ diff --git a/tests/sv-comp/cfg/nondetcall_same_true-unreach-call.expected b/tests/sv-comp/cfg/nondetcall_same_true-unreach-call.expected new file mode 100644 index 0000000000..e8ade1f42d --- /dev/null +++ b/tests/sv-comp/cfg/nondetcall_same_true-unreach-call.expected @@ -0,0 +1,105 @@ + ┌────────────────────────────────────────┐ + │ _ │ + └────────────────────────────────────────┘ + │ + │ Entry main + ▼ + ┌────────────────────────────────────────┐ + │ _ │ ·┐ + └────────────────────────────────────────┘ : + │ : + │ InlineEntry '()' : + ▼ : + ┌────────────────────────────────────────┐ : + │ _ │ : + └────────────────────────────────────────┘ : + │ : + │ Entry __VERIFIER_nondet_int : + ▼ : + ┌────────────────────────────────────────┐ : + │ _ │ : Inlined Proc 'tmp = __VERIFIER_nondet_int()' + └────────────────────────────────────────┘ : + │ : + │ Ret (Some val, __VERIFIER_nondet_int) : + ▼ : + ┌────────────────────────────────────────┐ : + │ _ │ : + └────────────────────────────────────────┘ : + │ : + │ InlineReturn 'tmp' : + ▼ : +┌───┐ Test (tmp,false) ┌────────────────────────────────────────┐ : +│ _ │ ◀───────────────────────────────────────────── │ _ │ ◀┘ +└───┘ └────────────────────────────────────────┘ + │ │ + │ │ Test (tmp,true) + │ ▼ + │ ┌────────────────────────────────────────┐ + │ │ _ │ + │ └────────────────────────────────────────┘ + │ │ + │ │ Assign 'fun = & foo' + │ ▼ + │ Assign 'fun = & foo' ┌────────────────────────────────────────┐ + └────────────────────────────────────────────────▶ │ _ │ ·┐ + └────────────────────────────────────────┘ : + │ : + │ InlineEntry '(1)' : + ▼ : + ┌────────────────────────────────────────┐ : + │ _ │ : + └────────────────────────────────────────┘ : + │ : + │ Entry foo : + ▼ : + ┌────────────────────────────────────────┐ : + ┌············································ │ _ │ : + : └────────────────────────────────────────┘ : + : │ : + : │ InlineEntry '(x - 1 < x)' : + : ▼ : + : ┌────────────────────────────────────────┐ : + : │ _ │ : + : └────────────────────────────────────────┘ : + : │ : + : │ Entry __VERIFIER_assert : + : ▼ : + : ┌────────────────────────────────────────┐ : + : │ _ │ : + : └────────────────────────────────────────┘ : + : │ : + : Inlined Proc '__VERIFIER_assert(x - 1 < x)' │ Test (! cond,false) : Inlined Proc '*fun(1)' + : ▼ : + : ┌────────────────────────────────────────┐ : + : │ _ │ : + : └────────────────────────────────────────┘ : + : │ : + : │ Ret (None, __VERIFIER_assert) : + : ▼ : + : ┌────────────────────────────────────────┐ : + : │ _ │ : + : └────────────────────────────────────────┘ : + : │ : + : │ InlineReturn : + : ▼ : + : ┌────────────────────────────────────────┐ : + └···········································▶ │ _ │ : + └────────────────────────────────────────┘ : + │ : + │ Ret (None, foo) : + ▼ : + ┌────────────────────────────────────────┐ : + │ _ │ : + └────────────────────────────────────────┘ : + │ : + │ InlineReturn : + ▼ : + ┌────────────────────────────────────────┐ : + │ _ │ ◀┘ + └────────────────────────────────────────┘ + │ + │ Ret (Some 0, main) + ▼ + ┌────────────────────────────────────────┐ + │ _ │ + └────────────────────────────────────────┘ diff --git a/tests/sv-comp/cfg/nondetcall_true-unreach-call.expected b/tests/sv-comp/cfg/nondetcall_true-unreach-call.expected new file mode 100644 index 0000000000..2706425f8b --- /dev/null +++ b/tests/sv-comp/cfg/nondetcall_true-unreach-call.expected @@ -0,0 +1,107 @@ + ┌────────────────────────────────────────┐ + │ _ │ + └────────────────────────────────────────┘ + │ + │ Entry main + ▼ + ┌────────────────────────────────────────┐ + │ _ │ ·┐ + └────────────────────────────────────────┘ : + │ : + │ InlineEntry '()' : + ▼ : + ┌────────────────────────────────────────┐ : + │ _ │ : + └────────────────────────────────────────┘ : + │ : + │ Entry __VERIFIER_nondet_int : + ▼ : + ┌────────────────────────────────────────┐ : + │ _ │ : Inlined Proc 'tmp = __VERIFIER_nondet_int()' + └────────────────────────────────────────┘ : + │ : + │ Ret (Some val, __VERIFIER_nondet_int) : + ▼ : + ┌────────────────────────────────────────┐ : + │ _ │ : + └────────────────────────────────────────┘ : + │ : + │ InlineReturn 'tmp' : + ▼ : +┌───┐ Test (tmp,false) ┌────────────────────────────────────────┐ : +│ _ │ ◀───────────────────────────────────────────── │ _ │ ◀┘ +└───┘ └────────────────────────────────────────┘ + │ │ + │ │ Test (tmp,true) + │ ▼ + │ ┌────────────────────────────────────────┐ + │ │ _ │ + │ └────────────────────────────────────────┘ + │ │ + │ │ Assign 'fun = & foo' + │ ▼ + │ Assign 'fun = & bar' ┌─────────────────────────────────────────────────────────────────────────────────────────┐ InlineEntry '(1)' ┌────────────────────────────────┐ + └────────────────────────────────────────────────▶ │ _ │ ───────────────────▶ │ _ │ + └─────────────────────────────────────────────────────────────────────────────────────────┘ └────────────────────────────────┘ + │ : │ + │ InlineEntry '(1)' : │ Entry bar + ▼ : ▼ + ┌────────────────────────────────────────┐ : ┌────────────────────────────────┐ + │ _ │ : │ _ │ ·┐ + └────────────────────────────────────────┘ : └────────────────────────────────┘ : + │ : │ : + │ Entry foo : │ InlineEntry '(x < x + 1)' : + ▼ : ▼ : + ┌────────────────────────────────────────┐ : ┌────────────────────────────────┐ : + ┌············································ │ _ │ : │ _ │ : + : └────────────────────────────────────────┘ : └────────────────────────────────┘ : + : │ : │ : + : │ InlineEntry '(x - 1 < x)' : │ Entry __VERIFIER_assert : + : ▼ : ▼ : + : ┌────────────────────────────────────────┐ : ┌────────────────────────────────┐ : + : │ _ │ : │ _ │ : + : └────────────────────────────────────────┘ : └────────────────────────────────┘ : + : │ : │ : + : │ Entry __VERIFIER_assert : │ Test (! cond,false) : Inlined Proc '__VERIFIER_assert(x < x + 1)' + : ▼ : ▼ : + : ┌────────────────────────────────────────┐ : ┌────────────────────────────────┐ : + : │ _ │ : │ _ │ : + : └────────────────────────────────────────┘ : └────────────────────────────────┘ : + : │ : │ : + : Inlined Proc '__VERIFIER_assert(x - 1 < x)' │ Test (! cond,false) : │ Ret (None, __VERIFIER_assert) : + : ▼ : ▼ : + : ┌────────────────────────────────────────┐ : Inlined Proc '*fun(1)' ┌────────────────────────────────┐ : + : │ _ │ : │ _ │ : + : └────────────────────────────────────────┘ : └────────────────────────────────┘ : + : │ : │ : + : │ Ret (None, __VERIFIER_assert) : │ InlineReturn : + : ▼ : ▼ : + : ┌────────────────────────────────────────┐ : ┌────────────────────────────────┐ : + : │ _ │ : │ _ │ ◀┘ + : └────────────────────────────────────────┘ : └────────────────────────────────┘ + : │ : │ + : │ InlineReturn : │ Ret (None, bar) + : ▼ : ▼ + : ┌────────────────────────────────────────┐ : ┌────────────────────────────────┐ + └···········································▶ │ _ │ : │ _ │ + └────────────────────────────────────────┘ : └────────────────────────────────┘ + │ : │ + │ Ret (None, foo) : │ + ▼ : │ + ┌────────────────────────────────────────┐ : │ + │ _ │ : │ + └────────────────────────────────────────┘ : │ + │ : │ + │ InlineReturn : │ + ▼ : │ + ┌────────────────────────────────────────┐ : │ + ┌───────────────────────────────────────────▶ │ _ │ ◀┘ │ + │ └────────────────────────────────────────┘ │ + │ │ │ + │ │ Ret (Some 0, main) │ + │ ▼ │ + │ InlineReturn ┌────────────────────────────────────────┐ │ + │ │ _ │ │ + │ └────────────────────────────────────────┘ │ + │ │ + └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ diff --git a/tests/sv-comp/dune b/tests/sv-comp/dune index bf44bb8cb1..6a50c261bf 100644 --- a/tests/sv-comp/dune +++ b/tests/sv-comp/dune @@ -4,10 +4,11 @@ (alias runtest) (mode promote) (deps - (:files ; patterns from ReachSafety-Basic.set + (:files ; patterns from ReachSafety-Basic.set and now more (glob_files basic/*.c) (glob_files eq/*.c) (glob_files cfg/multicall_*.c) + (glob_files cfg/nondetcall_*.c) (glob_files cfg/join_true-unreach-call.c) (glob_files cfg/builtin_expect_true-unreach-call.c) (glob_files cfg/region_global_init_true-unreach-call.c) diff --git a/tests/sv-comp/dune.inc b/tests/sv-comp/dune.inc index 5ef014aec7..06d9e23b10 100644 --- a/tests/sv-comp/dune.inc +++ b/tests/sv-comp/dune.inc @@ -550,6 +550,50 @@ (action (diff multicall_true-unreach-call.expected multicall_true-unreach-call.output)))) +(subdir cfg + (rule + (deps + (sandbox always) ; must sandbox to prevent arg.dot-s from parallel runs from interfering + (package goblint) ; depend on entire goblint package for svcomp21 conf + (:c nondetcall_same_true-unreach-call.c) + (:prop %{project_root}/tests/sv-comp/unreach-call-__VERIFIER_error.prp)) + (target nondetcall_same_true-unreach-call.output) + (enabled_if %{bin-available:graph-easy}) + (action + (progn + (ignore-outputs + (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (with-outputs-to %{target} + (run graph-easy --as=boxart arg.dot))))) + + (rule + (alias runtest) + (enabled_if %{bin-available:graph-easy}) + (action + (diff nondetcall_same_true-unreach-call.expected nondetcall_same_true-unreach-call.output)))) + +(subdir cfg + (rule + (deps + (sandbox always) ; must sandbox to prevent arg.dot-s from parallel runs from interfering + (package goblint) ; depend on entire goblint package for svcomp21 conf + (:c nondetcall_true-unreach-call.c) + (:prop %{project_root}/tests/sv-comp/unreach-call-__VERIFIER_error.prp)) + (target nondetcall_true-unreach-call.output) + (enabled_if %{bin-available:graph-easy}) + (action + (progn + (ignore-outputs + (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (with-outputs-to %{target} + (run graph-easy --as=boxart arg.dot))))) + + (rule + (alias runtest) + (enabled_if %{bin-available:graph-easy}) + (action + (diff nondetcall_true-unreach-call.expected nondetcall_true-unreach-call.output)))) + (subdir cfg (rule (deps