Commit 85af222e authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl:tests] deactive tests in dev mode that do not work on CI

parent 345bb518
/* run.config /* run.config_dev
COMMENT: issue with printf on CI
DONTRUN:
*/
/* run.config_ci
COMMENT: variadic function call COMMENT: variadic function call
*/ */
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[kernel:annot:missing-spec] tests/bts/bts1398.c:12: Warning: [kernel:annot:missing-spec] tests/bts/bts1398.c:16: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype Neither code nor specification for function printf, generating default assigns from the prototype
/* run.config /* run.config_dev
COMMENT: issue with function pointers on CI
DONTRUN:
*/
/* run.config_ci
COMMENT: addrOf COMMENT: addrOf
*/ */
......
...@@ -19,7 +19,7 @@ void f(void) ...@@ -19,7 +19,7 @@ void f(void)
int __gen_e_acsl_initialized; int __gen_e_acsl_initialized;
__gen_e_acsl_initialized = __e_acsl_initialized((void *)p,sizeof(int)); __gen_e_acsl_initialized = __e_acsl_initialized((void *)p,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",(char *)"f", __e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",(char *)"f",
(char *)"\\initialized(p)",10); (char *)"\\initialized(p)",14);
} }
/*@ assert \initialized(p); */ ; /*@ assert \initialized(p); */ ;
__e_acsl_delete_block((void *)(& p)); __e_acsl_delete_block((void *)(& p));
...@@ -68,7 +68,7 @@ int main(void) ...@@ -68,7 +68,7 @@ int main(void)
__e_acsl_full_init((void *)(& x)); __e_acsl_full_init((void *)(& x));
f(); f();
__e_acsl_assert(& x == & x,(char *)"Assertion",(char *)"main", __e_acsl_assert(& x == & x,(char *)"Assertion",(char *)"main",
(char *)"&x == &x",16); (char *)"&x == &x",20);
/*@ assert &x ≡ &x; */ ; /*@ assert &x ≡ &x; */ ;
__e_acsl_full_init((void *)(& __retres)); __e_acsl_full_init((void *)(& __retres));
__retres = 0; __retres = 0;
......
/* run.config /* run.config_dev
COMMENT: issue with printf on CI
DONTRUN:
*/
/* run.config_ci
COMMENT: bts #2405. Memory not initialized for code executed before main. COMMENT: bts #2405. Memory not initialized for code executed before main.
*/ */
...@@ -15,4 +19,4 @@ void f() { ...@@ -15,4 +19,4 @@ void f() {
int main() { int main() {
printf("main\n"); printf("main\n");
return 0; return 0;
} }
\ No newline at end of file
/* run.config /* run.config_dev
COMMENT: issue on CI
DONTRUN:
*/
/* run.config_ci
COMMENT: Malloc executed by a library function COMMENT: Malloc executed by a library function
*/ */
......
/* run.config /* run.config_dev
COMMENT: issue with printf on CI
DONTRUN:
*/
/* run.config_ci
COMMENT: Check that deleting statements before goto jumps takes into COMMENT: Check that deleting statements before goto jumps takes into
COMMENT: account variable declarations given via local inits COMMENT: account variable declarations given via local inits
*/ */
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[kernel:annot:missing-spec] tests/memory/constructor.c:16: Warning: [kernel:annot:missing-spec] tests/memory/constructor.c:20: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype Neither code nor specification for function printf, generating default assigns from the prototype
...@@ -54,7 +54,7 @@ int main(int argc, char const **argv) ...@@ -54,7 +54,7 @@ int main(int argc, char const **argv)
__gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int), __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int),
(void *)(& a),(void *)0); (void *)(& a),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main", __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&a)",25); (char *)"\\valid(&a)",29);
} }
/*@ assert \valid(&a); */ ; /*@ assert \valid(&a); */ ;
if (t == 2) { if (t == 2) {
...@@ -71,7 +71,7 @@ int main(int argc, char const **argv) ...@@ -71,7 +71,7 @@ int main(int argc, char const **argv)
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int), __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int),
(void *)(& b),(void *)0); (void *)(& b),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",
(char *)"main",(char *)"\\valid(&b)",36); (char *)"main",(char *)"\\valid(&b)",40);
} }
/*@ assert \valid(&b); */ ; /*@ assert \valid(&b); */ ;
printf(__gen_e_acsl_literal_string_2,t,__gen_e_acsl_literal_string_4); printf(__gen_e_acsl_literal_string_2,t,__gen_e_acsl_literal_string_4);
......
[kernel:typing:implicit-function-declaration] tests/memory/hidden_malloc.c:11: Warning: [kernel:typing:implicit-function-declaration] tests/memory/hidden_malloc.c:15: Warning:
Calling undeclared function realpath. Old style K&R code? Calling undeclared function realpath. Old style K&R code?
[e-acsl] beginning translation. [e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[kernel:annot:missing-spec] tests/memory/hidden_malloc.c:11: Warning: [kernel:annot:missing-spec] tests/memory/hidden_malloc.c:15: Warning:
Neither code nor specification for function realpath, generating default assigns from the prototype Neither code nor specification for function realpath, generating default assigns from the prototype
[eva:invalid-assigns] tests/memory/hidden_malloc.c:11: [eva:invalid-assigns] tests/memory/hidden_malloc.c:15:
Completely invalid destination for assigns clause *((char *)x_1 + (0 ..)). Completely invalid destination for assigns clause *((char *)x_1 + (0 ..)).
Ignoring. Ignoring.
[e-acsl] beginning translation. [e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[kernel:annot:missing-spec] tests/memory/local_goto.c:37: Warning: [kernel:annot:missing-spec] tests/memory/local_goto.c:41: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype Neither code nor specification for function printf, generating default assigns from the prototype
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment