diff --git a/src/plugins/e-acsl/tests/bts/bts1398.c b/src/plugins/e-acsl/tests/bts/bts1398.c index 408d069e4ee4d948e31e4575b133f57d414df23b..9dbd83d269e0b636508a91221f8dfbb292c62a9f 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 a9c9e5c65e98d3f5f69ee0dbb2df47c1a5488782..196be478e598103ead236a8d08d82218bc6d0d9d 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 c3726404e6f8607953c074eb6a0ce06307dc1867..281703719852d97b3b865510c8ea8d67c049a045 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 ca3a611c9bd240c6dba0d59cbea332b76cbe4f44..e7da245320f44ca617784993e0bf842400a92cff 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 32e630a32788679eb2571379587ebad512b111fe..8530264c83f3dff89a26d3dc0beaa254942795a8 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 3900421de1c7da2824fd45627ebcfb7fc1c453b8..7d220a59517efd7bd62e13946568cae3d0b613fd 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 397f145cc16cd6eb5cdcdce28a0e0a103f03921a..a5448bf07063eeaa318549d0c51931ddf7357998 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 c660eb1a183b3770435f15404e2c620d30c13493..850186d110a852c7deff7b8cb2ed345dd9a3abe3 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 707853628e0809429f024754938dc89d741936cc..2cf1cc44c0cd0dd389bce183c8fa9c4fdb3ef873 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 7bb9d547bffed4a48e6a08788bb7ec3e12e802c2..cecec801d917584a0d8bcf334b1f14c947fb38a8 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 74588e72426d633d658a62543d219708afb71011..142c3f2be0104e92d2deba3a08cd8d2a0b4b1f10 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