diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c index c212a2c38bb7b613b64dfdd4e3fc16884d09291e..4e462743c9d2aeacd2d6c8b4a1e21a2055c020fb 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c +++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c @@ -58,6 +58,7 @@ int main(void) (char *)"!\\valid(q)",36); } __e_acsl_initialize((void *)q,sizeof(int)); + /*@ assert Value: mem_access: \valid(q); */ *q = 1; __retres = 0; return_label: __e_acsl_store_block_duplicate((void *)(& q),(size_t)8);