From 1422117513acaa0f95feb71b0df17d4f1a74cd1e Mon Sep 17 00:00:00 2001
From: Guillaume Petiot <guillaume.petiot@cea.fr>
Date: Mon, 17 Mar 2014 09:19:59 +0100
Subject: [PATCH] changed test case for bts1700
---
src/plugins/e-acsl/tests/e-acsl-runtime/bts1700.i | 4 ++--
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
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 78c1e1e13c1..bcf7a9e9f42 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 e1369239518..678a82b6e69 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; */
/*@
--
GitLab