Commit 48609795 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl:tests] Reactivate `special` tests

parent 75b7205a
/* run.config_ci
/* run.config_ci, run.config_dev
COMMENT: -e-acsl-builtins
LOG: gen_builtin.c
STDOPT: #"-e-acsl-builtins incr"
MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -e-acsl-builtins incr
*/
int incr(int);
......
/* run.config_ci
/* run.config_ci, run.config_dev
COMMENT: test option -e-acsl-functions
LOG: gen_@PTEST_NAME@.c
STDOPT: #"-e-acsl-functions f"
MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -e-acsl-functions f
*/
/*@ requires \initialized(p);
......
/* run.config_ci
/* run.config_ci, run.config_dev
COMMENT: test option -e-acsl-instrument; cannot run Eva on this example
LOG: gen_@PTEST_NAME@.c
STDOPT:#"-e-acsl-instrument='@@all,-uninstrument1,-uninstrument2'"
MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -e-acsl-instrument @@@@all,-uninstrument1,-uninstrument2
*/
#include <stdarg.h>
......@@ -43,7 +43,7 @@ int vol(int n, ...) {
va_start(vl, n);
int r = va_arg(vl, int);
va_end(vl);
return 1;
return 0;
}
int main(void) {
......
/* run.config_ci
/* run.config_ci, run.config_dev
COMMENT: test option -e-acsl-no-valid
DONTRUN:
LOG: gen_@PTEST_NAME@.c
STDOPT: #"-e-acsl-prepare -e-acsl-share ./share/e-acsl -eva -eva-verbose 0 -then -e-acsl-no-valid"
MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -eva -eva-verbose 0
MACRO: ROOT_EACSL_GCC_OPTS_EXT --then --e-acsl-extra -e-acsl-no-valid
*/
#include <stdlib.h>
......
[eva:alarm] tests/special/e-acsl-valid.c:36: Warning:
[eva:alarm] tests/special/e-acsl-valid.c:37: Warning:
function f: precondition \valid(y) got status unknown.
[eva:alarm] tests/special/e-acsl-valid.c:37: Warning:
function f: precondition \valid(y) got status unknown.
[e-acsl] beginning translation.
[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:165: Warning:
Neither code nor specification for function aligned_alloc, generating default assigns from the prototype
[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:181: Warning:
Neither code nor specification for function __e_acsl_mspaces_init, generating default assigns from the prototype
[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:446: Warning:
Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:450: Warning:
Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype
[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:454: Warning:
Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype
[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:458: Warning:
Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:462: Warning:
Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:467: Warning:
Neither code nor specification for function __e_acsl_builtin_syslog, generating default assigns from the prototype
[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:488: Warning:
Neither code nor specification for function __e_acsl_floating_point_exception, generating default assigns from the prototype
[kernel] Current source was: tests/special/e-acsl-valid.c:33
The full backtrace is:
Raised at file "src/libraries/project/project.ml", line 405, characters 59-66
Called from file "src/main.ml", line 155, characters 14-1023
Called from file "src/main.ml", line 121, characters 12-34
Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from file "src/main.ml", line 258, characters 11-56
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 807, characters 30-76
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
Unexpected error (E_ACSL.Misc.Unregistered_library_function("__e_acsl_store_block")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is 19.0+dev (Potassium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
[e-acsl] tests/special/e-acsl-valid.c:25: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] tests/special/e-acsl-valid.c:26: Warning:
E-ACSL construct `variant' is not yet supported. Ignoring annotation.
[e-acsl] tests/special/e-acsl-valid.c:26: Warning:
E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
[e-acsl] tests/special/e-acsl-valid.c:26: Warning:
E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
[e-acsl] tests/special/e-acsl-valid.c:10: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
......@@ -78,7 +78,7 @@ int vol(int n , ...)
/*@ assert Eva: initialization: \initialized(&tmp); */
int r = tmp;
__builtin_va_end(vl);
__retres = 1;
__retres = 0;
return __retres;
}
......
......@@ -25,58 +25,35 @@ void __gen_e_acsl_f(int *x, int *y);
void f(int *x, int *y)
{
{
int __gen_e_acsl_valid_read;
__e_acsl_store_block((void *)(& y),(size_t)8);
__e_acsl_store_block((void *)(& x),(size_t)8);
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)x,sizeof(int),
(void *)x,(void *)(& x));
__e_acsl_assert(__gen_e_acsl_valid_read,"RTE","f",
"mem_access: \\valid_read(x)",
"tests/special/e-acsl-valid.c",25);
__e_acsl_assert(*x >= 0,"Precondition","f","*x >= 0",
"tests/special/e-acsl-valid.c",25);
}
/*@ requires *x ≥ 0;
ensures 2 ≥ 1;
assigns *x; */
{
{
int __gen_e_acsl_valid_read;
__e_acsl_store_block((void *)(& y),(size_t)8);
__e_acsl_store_block((void *)(& x),(size_t)8);
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)x,sizeof(int),
(void *)x,(void *)(& x));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"f",
(char *)"mem_access: \\valid_read(x)",27);
__e_acsl_assert(*x >= 0,(char *)"Precondition",(char *)"f",
(char *)"*x >= 0",27);
}
__e_acsl_initialize((void *)x,sizeof(int));
(*x) ++;
__e_acsl_assert(1,(char *)"Postcondition",(char *)"f",(char *)"2 >= 1",
28);
}
__e_acsl_assert(1,"Postcondition","f","2 >= 1",
"tests/special/e-acsl-valid.c",26);
{
int i = 0;
/*@ loop variant 2 - i; */
{
{
int __gen_e_acsl_and;
if (0 <= i) __gen_e_acsl_and = i <= 1; else __gen_e_acsl_and = 0;
__e_acsl_assert(__gen_e_acsl_and,(char *)"Invariant",(char *)"f",
(char *)"0 <= i <= 1",31);
}
/*@ loop invariant 0 ≤ i ≤ 1; */
while (i < 1) {
/*@ assert 1 ≡ 1; */
__e_acsl_assert(1,(char *)"Assertion",(char *)"f",(char *)"1 == 1",
33);
/*@ assert \valid(y); */
{
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)y,sizeof(int),
(void *)y,(void *)(& y));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"f",
(char *)"\\valid(y)",33);
}
{
int __gen_e_acsl_and_2;
i ++;
if (0 <= i) __gen_e_acsl_and_2 = i <= 1;
else __gen_e_acsl_and_2 = 0;
__e_acsl_assert(__gen_e_acsl_and_2,(char *)"Invariant",(char *)"f",
(char *)"0 <= i <= 1",31);
}
}
/*@ loop invariant 0 ≤ i ≤ 1;
loop variant 2 - i; */
while (i < 1) {
/*@ assert 1 ≡ 1; */ ;
/*@ assert \valid(y); */ ;
i ++;
}
}
__e_acsl_delete_block((void *)(& y));
......@@ -122,90 +99,19 @@ int main(void)
*/
void __gen_e_acsl_f(int *x, int *y)
{
long __gen_e_acsl_at_6;
int *__gen_e_acsl_at_5;
int *__gen_e_acsl_at_4;
int __gen_e_acsl_at_3;
int *__gen_e_acsl_at_2;
int __gen_e_acsl_at;
{
int __gen_e_acsl_valid_read_5;
__gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)x,sizeof(int),
(void *)x,(void *)(& x));
__e_acsl_assert(__gen_e_acsl_valid_read_5,(char *)"RTE",(char *)"f",
(char *)"mem_access: \\valid_read(x)",14);
__gen_e_acsl_at_6 = (long)*x;
}
__gen_e_acsl_at_5 = x;
__gen_e_acsl_at_4 = x;
{
int __gen_e_acsl_valid_read_3;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)x,sizeof(int),
(void *)x,(void *)(& x));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"f",
(char *)"mem_access: \\valid_read(x)",21);
__gen_e_acsl_at_3 = *x == 0;
}
__gen_e_acsl_at_2 = x;
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)x,sizeof(int),
(void *)x,(void *)(& x));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"f",
(char *)"mem_access: \\valid_read(x)",17);
__gen_e_acsl_at = *x == 1;
}
{
int __gen_e_acsl_valid;
__e_acsl_store_block((void *)(& y),(size_t)8);
__e_acsl_store_block((void *)(& x),(size_t)8);
__gen_e_acsl_valid = __e_acsl_valid((void *)y,sizeof(int),(void *)y,
(void *)(& y));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"f",
(char *)"\\valid(y)",12);
__e_acsl_assert(*x >= 0,(char *)"Precondition",(char *)"f",
(char *)"*x >= 0",13);
__e_acsl_assert(__gen_e_acsl_valid,"Precondition","f","\\valid(y)",
"tests/special/e-acsl-valid.c",10);
}
f(x,y);
{
int __gen_e_acsl_implies;
int __gen_e_acsl_implies_2;
if (! __gen_e_acsl_at) __gen_e_acsl_implies = 1;
else {
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
sizeof(int),
(void *)__gen_e_acsl_at_2,
(void *)(& __gen_e_acsl_at_2));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"f",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_2)",
19);
__gen_e_acsl_implies = *__gen_e_acsl_at_2 < 0;
}
__e_acsl_assert(__gen_e_acsl_implies,(char *)"Postcondition",(char *)"f",
(char *)"\\old(*x == 1) ==> *\\old(x) < 0",19);
if (! __gen_e_acsl_at_3) __gen_e_acsl_implies_2 = 1;
else {
int __gen_e_acsl_valid_read_4;
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)__gen_e_acsl_at_4,
sizeof(int),
(void *)__gen_e_acsl_at_4,
(void *)(& __gen_e_acsl_at_4));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"f",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_4)",
22);
__gen_e_acsl_implies_2 = *__gen_e_acsl_at_4 == 1;
}
__e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Postcondition",
(char *)"f",(char *)"\\old(*x == 0) ==> *\\old(x) == 1",
22);
__e_acsl_assert((long)*__gen_e_acsl_at_5 == __gen_e_acsl_at_6 + 1L,
(char *)"Postcondition",(char *)"f",
(char *)"*\\old(x) == \\old(*x) + 1",14);
__e_acsl_delete_block((void *)(& y));
__e_acsl_delete_block((void *)(& x));
return;
}
__e_acsl_delete_block((void *)(& y));
__e_acsl_delete_block((void *)(& x));
return;
}
[kernel] Parsing tests/special/builtin.i (no preprocessing)
[kernel:annot-error] tests/special/builtin.i:9: Warning:
unbound function incr. Ignoring logic specification of function f
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "tests/special/builtin.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
[kernel] User Error: cannot load plug-in 'frama-c-e_acsl': cannot load module
Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"./top/E_ACSL.cmxs: cannot open shared object file: No such file or directory\")")
[kernel] User Error: compilation of './tests/print.ml' failed
[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
[kernel] Parsing tests/special/e-acsl-functions.c (with preprocessing)
tests/special/e-acsl-instrument.c: In function 'instrument2'
tests/special/e-acsl-instrument.c:29: Warning: no sound verdict for Precondition (guess: ok).
the considered predicate is:
\valid(p)
tests/special/e-acsl-instrument.c: In function 'uninstrument2'
tests/special/e-acsl-instrument.c:14: Warning: no sound verdict for Precondition (guess: ok).
the considered predicate is:
\valid(p)
tests/special/e-acsl-instrument.c: In function 'main'
tests/special/e-acsl-instrument.c:56: Warning: no sound verdict for Assertion (guess: ok).
the considered predicate is:
\initialized(&x)
tests/special/e-acsl-instrument.c: In function 'main'
tests/special/e-acsl-instrument.c:57: Warning: no sound verdict for Assertion (guess: ok).
the considered predicate is:
\initialized(&y)
[kernel] User Error: cannot load plug-in 'frama-c-e_acsl': cannot load module
Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"./top/E_ACSL.cmxs: cannot open shared object file: No such file or directory\")")
[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
[kernel] Parsing tests/special/e-acsl-instrument.c (with preprocessing)
[kernel] Parsing share/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing share/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing tests/special/e-acsl-valid.c (with preprocessing)
[eva:alarm] tests/special/e-acsl-valid.c:37: Warning:
function f: precondition \valid(y) got status unknown.
Supports Markdown
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