Skip to content
Snippets Groups Projects
Commit 6306695f authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Update test oracle output as per renamed files in RTL

parent b832f69c
No related branches found
No related tags found
No related merge requests found
Showing
with 20 additions and 20 deletions
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/bts/bts1304.i:23:[value] warning: assertion got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
......@@ -4,5 +4,5 @@ tests/bts/bts1307.i:23:[e-acsl] warning: approximating a real number by a float
tests/bts/bts1307.i:23:[e-acsl] warning: approximating a real number by a float
tests/bts/bts1307.i:11:[e-acsl] warning: approximating a real number by a float
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] user error: type long double not implemented. Using double instead
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1390.c:13:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/bts/bts1390.c:13:[value] warning: function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/bts/bts1390.c:18:[value] warning: out of bounds read. assert \valid_read(s);
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1740.i:12:[value] warning: locals {a} escaping the scope of a block of main through p
tests/bts/bts1740.i:16:[value] warning: accessing left-value that contains escaping addresses.
assert ¬\dangling(&p);
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1837.i:18:[value] warning: signed overflow. assert -2147483648 ≤ i - 1;
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
......@@ -3,4 +3,4 @@
the generated program may miss memory instrumentation
if there are memory-related annotations.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/bts/bts2231.i:8:[value] warning: signed overflow. assert -9223372036854775808 ≤ __gen_e_acsl__2 - 1;
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
......@@ -2,5 +2,5 @@ tests/bts/bts2252.c:22:[kernel] warning: Calling undeclared function strncpy. Ol
[e-acsl] beginning translation.
tests/bts/bts2252.c:22:[kernel] warning: Neither code nor specification for function strncpy, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts2252.c:17:[value] warning: out of bounds read. assert \valid_read(srcbuf + i);
......@@ -21,7 +21,7 @@
[value] using specification for function __e_acsl_full_init
[value] using specification for function __e_acsl_initialized
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __e_acsl_delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
......@@ -21,7 +21,7 @@
[value] using specification for function __e_acsl_full_init
[value] using specification for function __e_acsl_initialized
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __e_acsl_delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
......@@ -22,7 +22,7 @@
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_cmp
[value] using specification for function __gmpz_init
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_q
[value] using specification for function __gmpz_get_si
[value] using specification for function __gmpz_clear
......
......@@ -22,7 +22,7 @@
[value] using specification for function __gmpz_neg
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
[value] using specification for function __gmpz_com
[value] using specification for function __gmpz_add
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment