Commit 416b510d authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl:tests] Reactivate `temporal` tests

parent 48609795
......@@ -107,7 +107,7 @@ int main(int argc, char const **argv)
}
__e_acsl_assert(__gen_e_acsl_or,"Assertion","main",
"g1 == \\null || \\valid(g1)",
"tests/temporal/t_getenv.c",13);
"tests/temporal/t_getenv.c",14);
}
/*@ assert g1 ≡ \null ∨ \valid(g1); */ ;
{
......@@ -132,7 +132,7 @@ int main(int argc, char const **argv)
}
__e_acsl_assert(__gen_e_acsl_or_2,"Assertion","main",
"g2 == \\null || \\valid(g2)",
"tests/temporal/t_getenv.c",14);
"tests/temporal/t_getenv.c",15);
}
/*@ assert g2 ≡ \null ∨ \valid(g2); */ ;
__retres = 0;
......
......@@ -39,7 +39,7 @@ int main(void)
}
else __gen_e_acsl_and = 0;
__e_acsl_assert(! __gen_e_acsl_and,"Assertion","main","!\\valid(p)",
"tests/temporal/t_scope.c",15);
"tests/temporal/t_scope.c",16);
}
/*@ assert ¬\valid(p); */ ;
{
......@@ -55,7 +55,7 @@ int main(void)
}
else __gen_e_acsl_and_2 = 0;
__e_acsl_assert(! __gen_e_acsl_and_2,"Assertion","main","!\\valid(q)",
"tests/temporal/t_scope.c",16);
"tests/temporal/t_scope.c",17);
}
/*@ assert ¬\valid(q); */ ;
{
......@@ -78,7 +78,7 @@ int main(void)
}
else __gen_e_acsl_and_3 = 0;
__e_acsl_assert(__gen_e_acsl_and_3,"Assertion","main","\\valid(p)",
"tests/temporal/t_scope.c",21);
"tests/temporal/t_scope.c",22);
}
/*@ assert \valid(p); */ ;
__e_acsl_initialize((void *)p,sizeof(int));
......@@ -96,7 +96,7 @@ int main(void)
}
else __gen_e_acsl_and_4 = 0;
__e_acsl_assert(! __gen_e_acsl_and_4,"Assertion","main","!\\valid(q)",
"tests/temporal/t_scope.c",24);
"tests/temporal/t_scope.c",25);
}
/*@ assert ¬\valid(q); */ ;
{
......@@ -104,7 +104,7 @@ int main(void)
__gen_e_acsl_valid_5 = __e_acsl_valid((void *)(& j),sizeof(int),
(void *)(& j),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_5,"Assertion","main","\\valid(&j)",
"tests/temporal/t_scope.c",25);
"tests/temporal/t_scope.c",26);
}
/*@ assert \valid(&j); */ ;
__e_acsl_delete_block((void *)(& j));
......@@ -132,7 +132,7 @@ int main(void)
}
else __gen_e_acsl_and_5 = 0;
__e_acsl_assert(! __gen_e_acsl_and_5,"Assertion","main","!\\valid(p)",
"tests/temporal/t_scope.c",34);
"tests/temporal/t_scope.c",35);
}
/*@ assert ¬\valid(p); */ ;
__e_acsl_full_init((void *)(& q));
......@@ -154,7 +154,7 @@ int main(void)
}
else __gen_e_acsl_and_6 = 0;
__e_acsl_assert(__gen_e_acsl_and_6,"Assertion","main","\\valid(p)",
"tests/temporal/t_scope.c",37);
"tests/temporal/t_scope.c",38);
}
/*@ assert \valid(p); */ ;
len --;
......
......@@ -15,13 +15,13 @@
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:488: Warning:
function __gen_e_acsl_getenv: postcondition 'null_or_valid_result' got status unknown.
[eva:alarm] tests/temporal/t_getenv.c:13: Warning:
pointer comparison. assert \pointer_comparable((void *)g1, (void *)0);
[eva:alarm] tests/temporal/t_getenv.c:13: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/temporal/t_getenv.c:13: Warning: assertion got status unknown.
[eva:alarm] tests/temporal/t_getenv.c:14: Warning:
pointer comparison. assert \pointer_comparable((void *)g2, (void *)0);
pointer comparison. assert \pointer_comparable((void *)g1, (void *)0);
[eva:alarm] tests/temporal/t_getenv.c:14: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/temporal/t_getenv.c:14: Warning: assertion got status unknown.
[eva:alarm] tests/temporal/t_getenv.c:15: Warning:
pointer comparison. assert \pointer_comparable((void *)g2, (void *)0);
[eva:alarm] tests/temporal/t_getenv.c:15: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/temporal/t_getenv.c:15: Warning: assertion got status unknown.
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[eva:locals-escaping] tests/temporal/t_scope.c:10: Warning:
[eva:locals-escaping] tests/temporal/t_scope.c:11: Warning:
locals {i} escaping the scope of a block of main through p
[eva:locals-escaping] tests/temporal/t_scope.c:10: Warning:
[eva:locals-escaping] tests/temporal/t_scope.c:11: Warning:
locals {i} escaping the scope of a block of main through q
[eva:alarm] tests/temporal/t_scope.c:15: Warning:
[eva:alarm] tests/temporal/t_scope.c:16: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&p);
[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/temporal/t_dpointer.c (with preprocessing)
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