From 3be07742d5f56c85dbcc3956c20e501cbd5f2ab7 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 4 Jun 2015 17:43:09 +0200
Subject: [PATCH] [tests] update wrt support of literal strings
mend
---
.../tests/bts/oracle/bts1390.res.oracle | 2 ++
.../tests/bts/oracle/bts1398.res.oracle | 3 --
.../tests/bts/oracle/bts1837.1.res.oracle | 4 +--
.../tests/bts/oracle/bts1837.err.oracle | 0
.../tests/bts/oracle/bts1837.res.oracle | 34 +++++++++++++++++++
.../e-acsl/tests/bts/oracle/gen_bts1837.c | 4 +--
.../tests/e-acsl-runtime/oracle/gen_stdout.c | 20 +++++------
.../tests/e-acsl-runtime/oracle/gen_stdout2.c | 20 +++++------
.../e-acsl-runtime/oracle/stdout.1.res.oracle | 2 ++
.../e-acsl-runtime/oracle/stdout.res.oracle | 2 ++
10 files changed, 64 insertions(+), 27 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1837.err.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
index 617549275c1..0dc7fb06cc0 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
@@ -10,6 +10,8 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
+ __e_acsl_literal_string ∈ {0}
+ __e_acsl_literal_string_2 ∈ {0}
[value] using specification for function __store_block
[value] using specification for function __full_init
[value] using specification for function __literal_string
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
index e8aef1cfbc2..a36a786f4a7 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
@@ -34,8 +34,5 @@
S___fc_real_data_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
S___fc_real_data_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function __store_block
-[value] using specification for function __full_init
-[value] using specification for function __literal_string
[value] using specification for function printf
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
index ad8c7116d47..efd924c5562 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
@@ -4,8 +4,8 @@
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
- random_counter ∈ {0}
- rand_max ∈ {32767}
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
new file mode 100644
index 00000000000..efd924c5562
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
@@ -0,0 +1,34 @@
+[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 ∈ [--..--]
+ S ∈ {0}
+ __e_acsl_literal_string ∈ {0}
+ __e_acsl_literal_string_2 ∈ {0}
+ __e_acsl_literal_string_3 ∈ {0}
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __literal_string
+tests/bts/bts1837.i:19:[value] entering loop for the first time
+tests/bts/bts1837.i:21:[value] Assertion got status valid.
+[value] using specification for function __initialized
+[value] using specification for function __valid_read
+[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.
+tests/bts/bts1837.i:22:[value] Assertion got status valid.
+[value] using specification for function __valid
+[value] using specification for function __delete_block
+tests/bts/bts1837.i:19:[kernel] warning: signed overflow. assert -2147483648 ≤ i-1;
+tests/bts/bts1837.i:11:[value] Assertion got status valid.
+tests/bts/bts1837.i:12:[value] Assertion got status valid.
+tests/bts/bts1837.i:13:[value] Assertion got status valid.
+[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_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
index 5860ba5a000..6a0ea2b012a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -21,8 +21,8 @@ extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
/*@
model __mpz_struct { ℤ n };
*/
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+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__)); */
/*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
index f4eedb8b927..404c5700de4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
@@ -1,4 +1,6 @@
/* Generated by Frama-C */
+char *__e_acsl_literal_string_2;
+char *__e_acsl_literal_string;
struct __anonstruct___mpz_struct_1 {
int _mp_alloc ;
int _mp_size ;
@@ -127,6 +129,14 @@ FILE *__e_acsl_fopen(char const *filename, char const *mode)
void __e_acsl_memory_init(void)
{
+ __e_acsl_literal_string_2 = "wb";
+ __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
+ __full_init((void *)__e_acsl_literal_string_2);
+ __literal_string((void *)__e_acsl_literal_string_2);
+ __e_acsl_literal_string = "foo";
+ __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
+ __full_init((void *)__e_acsl_literal_string);
+ __literal_string((void *)__e_acsl_literal_string);
__store_block((void *)(& stdout),8UL);
__full_init((void *)(& stdout));
return;
@@ -134,8 +144,6 @@ void __e_acsl_memory_init(void)
int main(void)
{
- char *__e_acsl_literal_string_2;
- char *__e_acsl_literal_string;
int __retres;
FILE *f;
FILE *f2;
@@ -144,14 +152,6 @@ int main(void)
__store_block((void *)(& f),8UL);
__full_init((void *)(& f));
f = stdout;
- __e_acsl_literal_string = "foo";
- __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
- __full_init((void *)__e_acsl_literal_string);
- __literal_string((void *)__e_acsl_literal_string);
- __e_acsl_literal_string_2 = "wb";
- __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
- __full_init((void *)__e_acsl_literal_string_2);
- __literal_string((void *)__e_acsl_literal_string_2);
__full_init((void *)(& f2));
f2 = __e_acsl_fopen(__e_acsl_literal_string,__e_acsl_literal_string_2);
/*@ assert f ≡ __fc_stdout; */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
index 13b9fa9cf18..b583971541f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
@@ -1,4 +1,6 @@
/* Generated by Frama-C */
+char *__e_acsl_literal_string_2;
+char *__e_acsl_literal_string;
struct __anonstruct___mpz_struct_1 {
int _mp_alloc ;
int _mp_size ;
@@ -134,6 +136,14 @@ FILE *__e_acsl_fopen(char const *filename, char const *mode)
void __e_acsl_memory_init(void)
{
+ __e_acsl_literal_string_2 = "wb";
+ __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
+ __full_init((void *)__e_acsl_literal_string_2);
+ __literal_string((void *)__e_acsl_literal_string_2);
+ __e_acsl_literal_string = "foo";
+ __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
+ __full_init((void *)__e_acsl_literal_string);
+ __literal_string((void *)__e_acsl_literal_string);
__store_block((void *)(& stdout),8UL);
__full_init((void *)(& stdout));
return;
@@ -141,8 +151,6 @@ void __e_acsl_memory_init(void)
int main(void)
{
- char *__e_acsl_literal_string_2;
- char *__e_acsl_literal_string;
int __retres;
FILE *f;
FILE *f2;
@@ -151,14 +159,6 @@ int main(void)
__store_block((void *)(& f),8UL);
__full_init((void *)(& f));
f = stdout;
- __e_acsl_literal_string = "foo";
- __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
- __full_init((void *)__e_acsl_literal_string);
- __literal_string((void *)__e_acsl_literal_string);
- __e_acsl_literal_string_2 = "wb";
- __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
- __full_init((void *)__e_acsl_literal_string_2);
- __literal_string((void *)__e_acsl_literal_string_2);
__full_init((void *)(& f2));
f2 = __e_acsl_fopen(__e_acsl_literal_string,__e_acsl_literal_string_2);
/*@ assert f ≡ __fc_stdout; */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
index c99d74f71f1..29505bbf903 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
@@ -20,6 +20,8 @@ FRAMAC_SHARE/libc/stdio.h:95:[e-acsl] warning: E-ACSL construct `logic function
stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
__fc_fopen[0..511] ∈ {0}
_p__fc_fopen ∈ {{ &__fc_fopen[0] }}
+ __e_acsl_literal_string ∈ {0}
+ __e_acsl_literal_string_2 ∈ {0}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
[--..--]
[0].[bits 80 to 95] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
index c99d74f71f1..29505bbf903 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
@@ -20,6 +20,8 @@ FRAMAC_SHARE/libc/stdio.h:95:[e-acsl] warning: E-ACSL construct `logic function
stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
__fc_fopen[0..511] ∈ {0}
_p__fc_fopen ∈ {{ &__fc_fopen[0] }}
+ __e_acsl_literal_string ∈ {0}
+ __e_acsl_literal_string_2 ∈ {0}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
[--..--]
[0].[bits 80 to 95] ∈ UNINITIALIZED
--
GitLab