diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1700.i b/src/plugins/e-acsl/tests/e-acsl-runtime/bts1700.i index 78c1e1e13c1b83a39372fc4a9201c6e21bcd98ce..bcf7a9e9f42fdc2681324d8f9b3676feceb4c4d9 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1700.i +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/bts1700.i @@ -1,6 +1,6 @@ /* 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 {}; diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c index e13692395184cab2d8c75f780ac5b97bebf57f7c..678a82b6e694e6fcd652dcc99f1c04476ef6021b 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c @@ -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; */ /*@