Skip to content
Snippets Groups Projects
Commit 82d0fbc7 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[tests] update oracles from frama-c (stdio.h and stdlib.h)

parent a944637e
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] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main [value] Analyzing a complete application starting at main
[value] Computing initial state [value] Computing initial state
......
...@@ -9,5 +9,5 @@ ...@@ -9,5 +9,5 @@
Please use option `-main' for specifying a valid entry point. Please use option `-main' for specifying a valid entry point.
The generated program may miss memory instrumentation The generated program may miss memory instrumentation
if there are memory-related annotations. if there are memory-related annotations.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing) [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h (with preprocessing) [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing tests/reject/quantif.i (no preprocessing) [kernel] Parsing tests/reject/quantif.i (no preprocessing)
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
tests/reject/quantif.i:6:[e-acsl] warning: E-ACSL construct `unguarded \forall quantification' is not yet supported. tests/reject/quantif.i:6:[e-acsl] warning: E-ACSL construct `unguarded \forall quantification' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/reject/quantif.i:7:[e-acsl] warning: invalid E-ACSL construct tests/reject/quantif.i:7:[e-acsl] warning: invalid E-ACSL construct
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
tests/runtime/base_addr.c:44:[value] warning: assertion got status unknown. tests/runtime/base_addr.c:44:[value] warning: assertion got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
tests/runtime/block_length.c:45:[value] warning: assertion got status unknown. tests/runtime/block_length.c:45:[value] warning: assertion got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
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