Skip to content
Snippets Groups Projects
Commit bd76d738 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[tests] oracle

parent b0e0549d
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/bugs/oracle/logiccast.res.oracle
+ 3
− 3
View file @ bd76d738
...@@ -3,10 +3,10 @@ Now output intermediate result ...@@ -3,10 +3,10 @@ Now output intermediate result
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
[wp] 2 goals scheduled [wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_Z1nPc_assert : Unknown [wp] [Alt-Ergo] Goal typed_Z1nPc_assert : Timeout
[wp] [Alt-Ergo] Goal typed_Z1mPv_assert : Unknown [wp] [Alt-Ergo] Goal typed_Z1mPv_assert : Timeout
[wp] Proved goals: 0 / 2 [wp] Proved goals: 0 / 2
Alt-Ergo: 0 (unknown: 2) Alt-Ergo: 0 (interrupted: 2)
[wp] Warning: Memory model hypotheses for function '_Z1mPv': [wp] Warning: Memory model hypotheses for function '_Z1mPv':
/*@ behavior typed: requires \separated(&base,r+(..)); */ /*@ behavior typed: requires \separated(&base,r+(..)); */
void _Z1mPv(void *r); void _Z1mPv(void *r);
......
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