diff --git a/tests/bugs/oracle/logiccast.res.oracle b/tests/bugs/oracle/logiccast.res.oracle index 264135561713fbc1ddeba1e4f4b9989d9a5fb02e..6cc697016a957f8faf2c4a81ffd35596fa4e4c05 100644 --- a/tests/bugs/oracle/logiccast.res.oracle +++ b/tests/bugs/oracle/logiccast.res.oracle @@ -9,10 +9,12 @@ Now output intermediate result [wp] Proved goals: 0 / 2 Alt-Ergo: 0 (unsuccess: 2) [wp] Warning: Memory model hypotheses for function '_Z1mPv': - /*@ behavior typed: requires \separated(&base,r+(..)); */ + /*@ behavior typed: + requires \separated(r + (..), &_Z4base); */ void _Z1mPv(void *r); [wp] Warning: Memory model hypotheses for function '_Z1nPc': - /*@ behavior typed: requires \separated(&base,r+(..)); */ + /*@ behavior typed: + requires \separated(r + (..), &_Z4base); */ void _Z1nPc(char *r); /* Generated by Frama-C */ char *base;