From 860df6868da2c367f18ec0b3eb08028f96edcc64 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Thu, 10 Dec 2015 09:42:10 +0100
Subject: [PATCH] Added bts test case for issue #1718 with compound
initializers
---
src/plugins/e-acsl/tests/bts/bts1718.i | 19 +++
.../tests/bts/oracle/bts1718.0.err.oracle | 0
.../tests/bts/oracle/bts1718.0.res.oracle | 22 ++++
.../tests/bts/oracle/bts1718.1.err.oracle | 0
.../tests/bts/oracle/bts1718.1.res.oracle | 22 ++++
.../e-acsl/tests/bts/oracle/gen_bts1718.c | 111 ++++++++++++++++++
.../e-acsl/tests/bts/oracle/gen_bts17182.c | 111 ++++++++++++++++++
7 files changed, 285 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/bts/bts1718.i
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1718.0.err.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1718.1.err.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/gen_bts17182.c
diff --git a/src/plugins/e-acsl/tests/bts/bts1718.i b/src/plugins/e-acsl/tests/bts/bts1718.i
new file mode 100644
index 00000000000..0b13703f0a8
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/bts1718.i
@@ -0,0 +1,19 @@
+/* run.config
+ COMMENT: bts #1718, issue regarding incorrect initialization of literal strings in global arrays with compound initializers
+ STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
+ EXECNOW: LOG gen_bts1718.c BIN gen_bts1718.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1718.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1718.c > /dev/null && ./gcc_bts.sh bts1718
+ EXECNOW: LOG gen_bts17182.c BIN gen_bts17182.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1718.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts17182.c > /dev/null && ./gcc_bts.sh bts17182
+*/
+
+int main(void) {
+ int a = 10, *p;
+ goto lbl_1;
+
+ lbl_2:
+ /*@ assert \valid(p); */
+ return 0;
+
+ lbl_1:
+ p = &a;
+ goto lbl_2;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle
new file mode 100644
index 00000000000..a4617af6a66
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle
@@ -0,0 +1,22 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+tests/bts/bts1718.i:13:[value] Assertion got status valid.
+[value] using specification for function __initialized
+[value] using specification for function __valid
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function __delete_block
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle
new file mode 100644
index 00000000000..a4617af6a66
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle
@@ -0,0 +1,22 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+tests/bts/bts1718.i:13:[value] Assertion got status valid.
+[value] using specification for function __initialized
+[value] using specification for function __valid
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function __delete_block
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
new file mode 100644
index 00000000000..bfd83983a86
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
@@ -0,0 +1,111 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
+
+/*@
+axiomatic dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1)); */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+ assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+extern size_t __memory_size;
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+ */
+int main(void)
+{
+ int __retres;
+ int a;
+ int *p;
+ __store_block((void *)(& p),4U);
+ __store_block((void *)(& a),4U);
+ __full_init((void *)(& a));
+ a = 10;
+ goto lbl_1;
+ lbl_2:
+ /*@ assert \valid(p); */
+ {
+ int __e_acsl_initialized;
+ int __e_acsl_and;
+ __e_acsl_initialized = __initialized((void *)(& p),sizeof(int *));
+ if (__e_acsl_initialized) {
+ int __e_acsl_valid;
+ __e_acsl_valid = __valid((void *)p,sizeof(int));
+ __e_acsl_and = __e_acsl_valid;
+ }
+ else __e_acsl_and = 0;
+ e_acsl_assert(__e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(p)",13);
+ }
+ __retres = 0;
+ goto return_label;
+ lbl_1: __full_init((void *)(& p));
+ p = & a;
+ goto lbl_2;
+ return_label:
+ __delete_block((void *)(& p));
+ __delete_block((void *)(& a));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts17182.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts17182.c
new file mode 100644
index 00000000000..bfd83983a86
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts17182.c
@@ -0,0 +1,111 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
+
+/*@
+axiomatic dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1)); */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+ assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+extern size_t __memory_size;
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+ */
+int main(void)
+{
+ int __retres;
+ int a;
+ int *p;
+ __store_block((void *)(& p),4U);
+ __store_block((void *)(& a),4U);
+ __full_init((void *)(& a));
+ a = 10;
+ goto lbl_1;
+ lbl_2:
+ /*@ assert \valid(p); */
+ {
+ int __e_acsl_initialized;
+ int __e_acsl_and;
+ __e_acsl_initialized = __initialized((void *)(& p),sizeof(int *));
+ if (__e_acsl_initialized) {
+ int __e_acsl_valid;
+ __e_acsl_valid = __valid((void *)p,sizeof(int));
+ __e_acsl_and = __e_acsl_valid;
+ }
+ else __e_acsl_and = 0;
+ e_acsl_assert(__e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(p)",13);
+ }
+ __retres = 0;
+ goto return_label;
+ lbl_1: __full_init((void *)(& p));
+ p = & a;
+ goto lbl_2;
+ return_label:
+ __delete_block((void *)(& p));
+ __delete_block((void *)(& a));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
--
GitLab