Skip to content
Snippets Groups Projects
Commit 7fa2cffe authored by Andre Maroneze's avatar Andre Maroneze
Browse files

Merge branch 'fix/eva/pointer-comparable' into 'master'

Updates a test oracle to synchronize with frama-c/frama-c!1668.

See merge request frama-c/e-acsl!193
parents 900ab734 7d446618
No related branches found
No related tags found
No related merge requests found
...@@ -58,6 +58,7 @@ int main(void) ...@@ -58,6 +58,7 @@ int main(void)
(char *)"!\\valid(q)",36); (char *)"!\\valid(q)",36);
} }
__e_acsl_initialize((void *)q,sizeof(int)); __e_acsl_initialize((void *)q,sizeof(int));
/*@ assert Value: mem_access: \valid(q); */
*q = 1; *q = 1;
__retres = 0; __retres = 0;
return_label: __e_acsl_store_block_duplicate((void *)(& q),(size_t)8); return_label: __e_acsl_store_block_duplicate((void *)(& q),(size_t)8);
......
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