Skip to content
Snippets Groups Projects
Commit 14221175 authored by Guillaume Petiot's avatar Guillaume Petiot
Browse files

changed test case for bts1700

parent 63a4eb7c
No related branches found
No related tags found
No related merge requests found
/* run.config
COMMENT: argument of functions must be kept, so keep its parameter
EXECNOW: LOG gen_bts1700.c BIN gen_bts1700.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1700.i -constfold -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1700.c > /dev/null && ./gcc_test.sh bts1700
COMMENT: pointer to an empty struct
EXECNOW: LOG gen_bts1700.c BIN gen_bts1700.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1700.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1700.c > /dev/null && ./gcc_test.sh bts1700
*/
struct toto {};
......
......@@ -22,7 +22,7 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
model __mpz_struct { ℤ n };
*/
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = 32767UL;
unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
......
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