diff --git a/src/plugins/e-acsl/tests/runtime/early_exit.c b/src/plugins/e-acsl/tests/runtime/early_exit.c
index 8dd7631bf598e04a990f8b334eb37c3c641d0520..854a04a5573959c997e56c8ba44383e8bf05fb89 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 9e397cceed85674880c38ada0b619246be6b6008..d7a840a8dc17f28ee570606415d6837d0ecc6f06 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 609ef70af854aeec7f35d10f33bc5333171ef639..3e368b613a5012665554059c756dca3d39137bc2 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 a84990844afe9c076130da2f0be55cd6c9a9ca0d..ba226e9e6d64d59137ba1b53851efda350850aa8 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 468635868637f9cf115b7e4b998a56bd9be83e02..3dda7fb5989c12c4b96f5a45a12f145bbd61970d 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); */