From 7db690c0d1160fbcc7ba827138d6911bbf042164 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Sat, 14 Oct 2017 22:52:18 +0200
Subject: [PATCH] Update tests and oracles against kernel modifications
- improvement in Variadic
- local variables are now always kept, even if unused.
---
src/plugins/e-acsl/tests/runtime/early_exit.c | 2 +-
.../runtime/oracle/local_goto.res.oracle | 1 -
.../tests/temporal/oracle/gen_t_struct.c | 27 ++++++++++++-------
.../temporal/oracle/t_malloc-asan.res.oracle | 1 -
src/plugins/e-acsl/tests/temporal/t_struct.c | 3 +++
5 files changed, 22 insertions(+), 12 deletions(-)
diff --git a/src/plugins/e-acsl/tests/runtime/early_exit.c b/src/plugins/e-acsl/tests/runtime/early_exit.c
index 8dd7631bf59..854a04a5573 100644
--- a/src/plugins/e-acsl/tests/runtime/early_exit.c
+++ b/src/plugins/e-acsl/tests/runtime/early_exit.c
@@ -124,7 +124,7 @@ int while_valid() {
* are not recorded twice. */
void continue_valid() {
int i = 0;
- int *p, *q, *r;
+ int *p, *q;
while (i++) {
/*@ assert ! \valid(p); */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
index 9e397cceed8..d7a840a8dc1 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
@@ -1,4 +1,3 @@
-[variadic] warning: Unable to locate global __fc_stdout which should be in the Frama-C LibC. Correct specifications can't be generated.
[e-acsl] beginning translation.
[e-acsl] warning: annotating undefined function `printf_va_1':
the generated program may miss memory instrumentation
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_struct.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_struct.c
index 609ef70af85..3e368b613a5 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_struct.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_struct.c
@@ -9,13 +9,20 @@ struct larger_t {
char *q ;
struct temporal_t t ;
};
+struct smaller_t {
+ char c ;
+};
typedef struct temporal_t temporal;
typedef struct larger_t larger;
+typedef struct smaller_t smaller;
int main(void)
{
int __retres;
+ smaller s1 __attribute__((__aligned__(4)));
+ smaller s2 __attribute__((__aligned__(4)));
temporal t1;
temporal t2;
+ temporal *tp;
temporal tarr[2];
larger l;
larger *lp;
@@ -31,6 +38,8 @@ int main(void)
__e_acsl_store_block((void *)(& a),(size_t)4);
__e_acsl_full_init((void *)(& a));
int b = 2;
+ s1.c = (char)'a';
+ s2 = s1;
__e_acsl_temporal_store_nblock((void *)(& t1.p),(void *)(& a));
__e_acsl_initialize((void *)(& t1.p),sizeof(char *));
t1.p = (char *)(& a);
@@ -67,7 +76,7 @@ int main(void)
}
else __gen_e_acsl_and_3 = 0;
__e_acsl_assert(__gen_e_acsl_and_3,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(t1.p) && \\valid(t1.q)",37);
+ (char *)"\\valid(t1.p) && \\valid(t1.q)",40);
}
/*@ assert ¬\valid(t2.p) ∧ ¬\valid(t2.q); */
{
@@ -99,7 +108,7 @@ int main(void)
}
else __gen_e_acsl_and_6 = 0;
__e_acsl_assert(__gen_e_acsl_and_6,(char *)"Assertion",(char *)"main",
- (char *)"!\\valid(t2.p) && !\\valid(t2.q)",38);
+ (char *)"!\\valid(t2.p) && !\\valid(t2.q)",41);
}
__e_acsl_temporal_memcpy((void *)(& t2),(void *)(& t1),(size_t)16);
__e_acsl_full_init((void *)(& t2));
@@ -134,7 +143,7 @@ int main(void)
}
else __gen_e_acsl_and_9 = 0;
__e_acsl_assert(__gen_e_acsl_and_9,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(t2.p) && \\valid(t2.q)",41);
+ (char *)"\\valid(t2.p) && \\valid(t2.q)",44);
}
__e_acsl_temporal_store_nblock((void *)(& t2.p),(void *)0);
__e_acsl_initialize((void *)(& t2.p),sizeof(char *));
@@ -174,7 +183,7 @@ int main(void)
}
else __gen_e_acsl_and_12 = 0;
__e_acsl_assert(__gen_e_acsl_and_12,(char *)"Assertion",(char *)"main",
- (char *)"!\\valid(t2.p) && \\valid(t2.q)",45);
+ (char *)"!\\valid(t2.p) && \\valid(t2.q)",48);
}
__e_acsl_temporal_memcpy((void *)(& l.t),(void *)(& t2),(size_t)16);
__e_acsl_initialize((void *)(& l.t),sizeof(struct temporal_t));
@@ -210,7 +219,7 @@ int main(void)
}
else __gen_e_acsl_and_15 = 0;
__e_acsl_assert(__gen_e_acsl_and_15,(char *)"Assertion",(char *)"main",
- (char *)"!\\valid(l.t.p) && \\valid(l.t.q)",48);
+ (char *)"!\\valid(l.t.p) && \\valid(l.t.q)",51);
}
__e_acsl_temporal_store_nblock((void *)(& lp),(void *)(& l));
__e_acsl_full_init((void *)(& lp));
@@ -229,7 +238,7 @@ int main(void)
(void *)(& lp->t.p),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(&lp->t.p)",51);
+ (char *)"mem_access: \\valid_read(&lp->t.p)",54);
__gen_e_acsl_valid_11 = __e_acsl_valid((void *)lp->t.p,sizeof(char),
(void *)lp->t.p,
(void *)(& lp->t.p));
@@ -237,7 +246,7 @@ int main(void)
}
else __gen_e_acsl_and_16 = 0;
__e_acsl_assert(! __gen_e_acsl_and_16,(char *)"Assertion",(char *)"main",
- (char *)"!\\valid(lp->t.p)",51);
+ (char *)"!\\valid(lp->t.p)",54);
}
__e_acsl_temporal_memcpy((void *)(tarr),(void *)(& t2),(size_t)16);
__e_acsl_initialize((void *)(tarr),sizeof(temporal));
@@ -275,7 +284,7 @@ int main(void)
}
else __gen_e_acsl_and_19 = 0;
__e_acsl_assert(__gen_e_acsl_and_19,(char *)"Assertion",(char *)"main",
- (char *)"!\\valid(tarr[0].p) && \\valid(tarr[0].q)",54);
+ (char *)"!\\valid(tarr[0].p) && \\valid(tarr[0].q)",57);
}
__e_acsl_temporal_memcpy((void *)(larr),(void *)(& l),(size_t)32);
__e_acsl_initialize((void *)(larr),sizeof(larger));
@@ -315,7 +324,7 @@ int main(void)
else __gen_e_acsl_and_22 = 0;
__e_acsl_assert(__gen_e_acsl_and_22,(char *)"Assertion",(char *)"main",
(char *)"!\\valid(larr[0].t.p) && \\valid(larr[0].t.q)",
- 57);
+ 60);
}
__retres = 0;
__e_acsl_delete_block((void *)(larr));
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
index a84990844af..ba226e9e6d6 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
@@ -1,4 +1,3 @@
-[variadic] warning: Unable to locate global __fc_stdout which should be in the Frama-C LibC. Correct specifications can't be generated.
[e-acsl] beginning translation.
[e-acsl] warning: annotating undefined function `printf_va_1':
the generated program may miss memory instrumentation
diff --git a/src/plugins/e-acsl/tests/temporal/t_struct.c b/src/plugins/e-acsl/tests/temporal/t_struct.c
index 46863586863..3dda7fb5989 100644
--- a/src/plugins/e-acsl/tests/temporal/t_struct.c
+++ b/src/plugins/e-acsl/tests/temporal/t_struct.c
@@ -32,6 +32,9 @@ int main(void) {
temporal t1, t2, *tp, tarr[2];
larger l, *lp, larr[2];
+ s1.c = 'a';
+ s2 = s1;
+
t1.p = &a;
t1.q = t1.p;
/*@assert \valid(t1.p) && \valid(t1.q); */
--
GitLab