From 09401e70a3d74431b9ca7279496c93b61aeebcf9 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 3 Apr 2020 16:11:28 +0200
Subject: [PATCH] [eacsl:tests] Reactivate failed CI tests for dev config
The following tests failed on CI due to Nix's GCC hardening:
- `bts/bts1398.c`
- `full-mmodel/addrOf.i`
- `memory/constructor.c`
- `memory/hidden_malloc.c`
- `memory/local_goto.c`
They have been reactivated in this commit.
---
src/plugins/e-acsl/tests/bts/bts1398.c | 4 ----
src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle | 2 +-
src/plugins/e-acsl/tests/full-mmodel/addrOf.i | 4 ----
src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c | 4 ++--
src/plugins/e-acsl/tests/memory/constructor.c | 4 ----
src/plugins/e-acsl/tests/memory/hidden_malloc.c | 4 ----
src/plugins/e-acsl/tests/memory/local_goto.c | 4 ----
.../e-acsl/tests/memory/oracle_ci/constructor.res.oracle | 2 +-
src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c | 4 ++--
.../e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle | 6 +++---
.../e-acsl/tests/memory/oracle_ci/local_goto.res.oracle | 2 +-
11 files changed, 10 insertions(+), 30 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/bts1398.c b/src/plugins/e-acsl/tests/bts/bts1398.c
index 408d069e4ee..9dbd83d269e 100644
--- a/src/plugins/e-acsl/tests/bts/bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/bts1398.c
@@ -1,7 +1,3 @@
-/* run.config_dev
- COMMENT: issue with printf on CI
- DONTRUN:
-*/
/* run.config_ci
COMMENT: variadic function call
*/
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle
index a9c9e5c65e9..196be478e59 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] tests/bts/bts1398.c:16: Warning:
+[kernel:annot:missing-spec] tests/bts/bts1398.c:12: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/full-mmodel/addrOf.i b/src/plugins/e-acsl/tests/full-mmodel/addrOf.i
index c3726404e6f..28170371985 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/addrOf.i
+++ b/src/plugins/e-acsl/tests/full-mmodel/addrOf.i
@@ -1,7 +1,3 @@
-/* run.config_dev
- COMMENT: issue with function pointers on CI
- DONTRUN:
-*/
/* run.config_ci
COMMENT: addrOf
*/
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
index ca3a611c9bd..e7da245320f 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
@@ -19,7 +19,7 @@ void f(void)
int __gen_e_acsl_initialized;
__gen_e_acsl_initialized = __e_acsl_initialized((void *)p,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized,"Assertion","f",
- "\\initialized(p)","tests/full-mmodel/addrOf.i",14);
+ "\\initialized(p)","tests/full-mmodel/addrOf.i",10);
}
/*@ assert \initialized(p); */ ;
__e_acsl_delete_block((void *)(& p));
@@ -82,7 +82,7 @@ int main(void)
__e_acsl_full_init((void *)(& x));
f();
__e_acsl_assert(& x == & x,"Assertion","main","&x == &x",
- "tests/full-mmodel/addrOf.i",20);
+ "tests/full-mmodel/addrOf.i",16);
/*@ assert &x ≡ &x; */ ;
__e_acsl_full_init((void *)(& __retres));
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/memory/constructor.c b/src/plugins/e-acsl/tests/memory/constructor.c
index 32e630a3278..8530264c83f 100644
--- a/src/plugins/e-acsl/tests/memory/constructor.c
+++ b/src/plugins/e-acsl/tests/memory/constructor.c
@@ -1,7 +1,3 @@
-/* run.config_dev
- COMMENT: issue with printf on CI
- DONTRUN:
-*/
/* run.config_ci
COMMENT: bts #2405. Memory not initialized for code executed before main.
*/
diff --git a/src/plugins/e-acsl/tests/memory/hidden_malloc.c b/src/plugins/e-acsl/tests/memory/hidden_malloc.c
index 3900421de1c..7d220a59517 100644
--- a/src/plugins/e-acsl/tests/memory/hidden_malloc.c
+++ b/src/plugins/e-acsl/tests/memory/hidden_malloc.c
@@ -1,7 +1,3 @@
-/* run.config_dev
- COMMENT: issue on CI
- DONTRUN:
-*/
/* run.config_ci
COMMENT: Malloc executed by a library function
*/
diff --git a/src/plugins/e-acsl/tests/memory/local_goto.c b/src/plugins/e-acsl/tests/memory/local_goto.c
index 397f145cc16..a5448bf0706 100644
--- a/src/plugins/e-acsl/tests/memory/local_goto.c
+++ b/src/plugins/e-acsl/tests/memory/local_goto.c
@@ -1,7 +1,3 @@
-/* run.config_dev
- COMMENT: issue with printf on CI
- DONTRUN:
-*/
/* run.config_ci
COMMENT: Check that deleting statements before goto jumps takes into
COMMENT: account variable declarations given via local inits
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle
index c660eb1a183..850186d110a 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] tests/memory/constructor.c:20: Warning:
+[kernel:annot:missing-spec] tests/memory/constructor.c:16: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
index 707853628e0..2cf1cc44c0c 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
@@ -54,7 +54,7 @@ int main(int argc, char const **argv)
__gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int),
(void *)(& a),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid,"Assertion","main","\\valid(&a)",
- "tests/memory/local_goto.c",29);
+ "tests/memory/local_goto.c",25);
}
/*@ assert \valid(&a); */ ;
if (t == 2) {
@@ -71,7 +71,7 @@ int main(int argc, char const **argv)
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int),
(void *)(& b),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_2,"Assertion","main","\\valid(&b)",
- "tests/memory/local_goto.c",40);
+ "tests/memory/local_goto.c",36);
}
/*@ assert \valid(&b); */ ;
printf(__gen_e_acsl_literal_string_2,t,__gen_e_acsl_literal_string_4);
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle
index 7bb9d547bff..cecec801d91 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle
@@ -1,9 +1,9 @@
-[kernel:typing:implicit-function-declaration] tests/memory/hidden_malloc.c:15: Warning:
+[kernel:typing:implicit-function-declaration] tests/memory/hidden_malloc.c:11: Warning:
Calling undeclared function realpath. Old style K&R code?
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] tests/memory/hidden_malloc.c:15: Warning:
+[kernel:annot:missing-spec] tests/memory/hidden_malloc.c:11: Warning:
Neither code nor specification for function realpath, generating default assigns from the prototype
-[eva:invalid-assigns] tests/memory/hidden_malloc.c:15:
+[eva:invalid-assigns] tests/memory/hidden_malloc.c:11:
Completely invalid destination for assigns clause *((char *)x_1 + (0 ..)).
Ignoring.
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle
index 74588e72426..142c3f2be01 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] tests/memory/local_goto.c:41: Warning:
+[kernel:annot:missing-spec] tests/memory/local_goto.c:37: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype
--
GitLab