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..879ed7048a11edf67ffcd7883aba3aaacb21c997 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
@@ -16,6 +16,7 @@ int main(void)
int __retres;
temporal t1;
temporal t2;
+ temporal *tp;
temporal tarr[2];
larger l;
larger *lp;
@@ -67,7 +68,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)",31);
}
/*@ assert ¬\valid(t2.p) ∧ ¬\valid(t2.q); */
{
@@ -99,7 +100,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)",32);
}
__e_acsl_temporal_memcpy((void *)(& t2),(void *)(& t1),(size_t)16);
__e_acsl_full_init((void *)(& t2));
@@ -134,7 +135,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)",35);
}
__e_acsl_temporal_store_nblock((void *)(& t2.p),(void *)0);
__e_acsl_initialize((void *)(& t2.p),sizeof(char *));
@@ -174,7 +175,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)",39);
}
__e_acsl_temporal_memcpy((void *)(& l.t),(void *)(& t2),(size_t)16);
__e_acsl_initialize((void *)(& l.t),sizeof(struct temporal_t));
@@ -210,7 +211,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)",42);
}
__e_acsl_temporal_store_nblock((void *)(& lp),(void *)(& l));
__e_acsl_full_init((void *)(& lp));
@@ -229,7 +230,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)",45);
__gen_e_acsl_valid_11 = __e_acsl_valid((void *)lp->t.p,sizeof(char),
(void *)lp->t.p,
(void *)(& lp->t.p));
@@ -237,7 +238,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)",45);
}
__e_acsl_temporal_memcpy((void *)(tarr),(void *)(& t2),(size_t)16);
__e_acsl_initialize((void *)(tarr),sizeof(temporal));
@@ -275,7 +276,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)",48);
}
__e_acsl_temporal_memcpy((void *)(larr),(void *)(& l),(size_t)32);
__e_acsl_initialize((void *)(larr),sizeof(larger));
@@ -315,7 +316,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);
+ 51);
}
__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..e72e879cf605c315e6b69d6579dc479e4e6648f2 100644
--- a/src/plugins/e-acsl/tests/temporal/t_struct.c
+++ b/src/plugins/e-acsl/tests/temporal/t_struct.c
@@ -16,19 +16,13 @@ struct larger_t {
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 a = 1,
b = 2;
- smaller s1, s2;
temporal t1, t2, *tp, tarr[2];
larger l, *lp, larr[2];