diff --git a/tests/spec/ghost_result_type.i b/tests/spec/ghost_result_type.i index 9adaff7cfb2513d3a55d35b8b2a78730c4df90dc..84ce3ad190cf5ffe9aa476f1c1002353e38ad02a 100644 --- a/tests/spec/ghost_result_type.i +++ b/tests/spec/ghost_result_type.i @@ -3,6 +3,12 @@ int *f(void); */ +/*@ ghost + /@ assigns \result,*\result \from \nothing; @/ + int \ghost * g(void); +*/ + int main(void){ //@ ghost int* p = f() ; + //@ ghost int \ghost* q = g() ; } diff --git a/tests/spec/oracle/ghost_result_type.res.oracle b/tests/spec/oracle/ghost_result_type.res.oracle index 9eb79cb29621eb40e0968d46c24fce005d2965d5..0bd50ab54f799958f03378835fd64024b4f7ec26 100644 --- a/tests/spec/oracle/ghost_result_type.res.oracle +++ b/tests/spec/oracle/ghost_result_type.res.oracle @@ -4,10 +4,18 @@ assigns \result \from \nothing; @/ int *f(void); */ +/*@ ghost +/@ assigns \result, *\result; + assigns \result \from \nothing; + assigns *\result \from \nothing; + @/ +int \ghost *g(void); */ + int main(void) { int __retres; /*@ ghost int *p = f(); */ + /*@ ghost int \ghost *q = g(); */ __retres = 0; return __retres; }