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

[tests] add variation on \ghost result type and assigns test

parent baaea844
No related branches found
No related tags found
No related merge requests found
......@@ -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() ;
}
......@@ -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;
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment