Skip to content
Snippets Groups Projects
Commit 5b924bea authored by Thibault Martin's avatar Thibault Martin
Browse files

Update test oracles

parent bbec67ab
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/value/oracle/behavior_statuses.1.res.oracle
+ 0
− 3
View file @ 5b924bea
...@@ -13,9 +13,6 @@ ...@@ -13,9 +13,6 @@
[eva] Initial state computed [eva] Initial state computed
[eva:initial-state] Values of globals at initialization [eva:initial-state] Values of globals at initialization
nondet ∈ [--..--] nondet ∈ [--..--]
[kernel:prop-status:emit]
Frama-C kernel emits status unknown for property default behavior
under 2 hypothesis
[eva] computing for function f <- main. [eva] computing for function f <- main.
Called from behavior_statuses.i:26. Called from behavior_statuses.i:26.
[eva] using specification for function f [eva] using specification for function f
......
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