Commit b7d5394b authored by Andre Maroneze's avatar Andre Maroneze
Browse files

synchronize with frama-c/frama-c!1723

parent 6b8742b1
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdio.h:157:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:157:[kernel:annot:missing-spec] warning: Neither code nor specification for function printf, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/bts/bts2252.c:22:[kernel:typing:implicit-function-declaration] warning: Calling undeclared function strncpy. Old style K&R code?
[e-acsl] beginning translation.
tests/bts/bts2252.c:22:[kernel] warning: Neither code nor specification for function strncpy, generating default assigns from the prototype
tests/bts/bts2252.c:22:[kernel:annot:missing-spec] warning: Neither code nor specification for function strncpy, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/bts/bts2252.c:17:[value:alarm] warning: out of bounds read. assert \valid_read(srcbuf + i);
......@@ -10,13 +10,13 @@ tests/format/fprintf.c:22:[kernel:typing:incompatible-types-call] warning: expec
[e-acsl] warning: annotating undefined function `fclose':
the generated program may miss memory instrumentation
if there are memory-related annotations.
FRAMAC_SHARE/libc/stdio.h:153:[kernel] warning: Neither code nor specification for function fprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:157:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:159:[kernel] warning: Neither code nor specification for function snprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:161:[kernel] warning: Neither code nor specification for function sprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:353:[kernel] warning: Neither code nor specification for function dprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/sys/wait.h:60:[kernel] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
tests/format/fprintf.c:15:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:153:[kernel:annot:missing-spec] warning: Neither code nor specification for function fprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:157:[kernel:annot:missing-spec] warning: Neither code nor specification for function printf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:159:[kernel:annot:missing-spec] warning: Neither code nor specification for function snprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:161:[kernel:annot:missing-spec] warning: Neither code nor specification for function sprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:353:[kernel:annot:missing-spec] warning: Neither code nor specification for function dprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/sys/wait.h:60:[kernel:annot:missing-spec] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
tests/format/fprintf.c:15:[kernel:annot:missing-spec] warning: Neither code nor specification for function fork, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:93:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdio.h:95:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
......@@ -79,12 +79,12 @@ FRAMAC_SHARE/libc/stdio.h:81:[e-acsl] warning: E-ACSL construct `assigns clause
[value] using specification for function __e_acsl_full_init
[value] using specification for function __e_acsl_mark_readonly
[value] using specification for function fork
tests/format/fprintf.c:15:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype
tests/format/fprintf.c:15:[kernel:annot:missing-spec] warning: Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype
[value] using specification for function __e_acsl_builtin_fprintf
[value] using specification for function exit
[value] using specification for function waitpid
tests/format/fprintf.c:15:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status);
tests/format/signalled.h:12:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
tests/format/signalled.h:12:[kernel:annot:missing-spec] warning: Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
[value] using specification for function __e_acsl_builtin_printf
[value] using specification for function __e_acsl_delete_block
tests/format/fprintf.c:16:[value] warning: Completely invalid destination for assigns clause *stream. Ignoring.
......@@ -98,11 +98,11 @@ FRAMAC_SHARE/libc/stdio.h:93:[value:alarm] warning: function __e_acsl_assert: pr
tests/format/fprintf.c:21:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_2);
tests/format/fprintf.c:22:[value] warning: Completely invalid destination for assigns clause *stream. Ignoring.
tests/format/fprintf.c:22:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_3);
tests/format/fprintf.c:27:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype
tests/format/fprintf.c:27:[kernel:annot:missing-spec] warning: Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype
[value] using specification for function __e_acsl_builtin_dprintf
tests/format/fprintf.c:27:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_4);
tests/format/fprintf.c:28:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_5);
tests/format/fprintf.c:34:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
tests/format/fprintf.c:34:[kernel:annot:missing-spec] warning: Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
[value] using specification for function __e_acsl_builtin_sprintf
tests/format/fprintf.c:34:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_6);
tests/format/fprintf.c:35:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_7);
......@@ -111,7 +111,7 @@ tests/format/fprintf.c:37:[value] warning: Completely invalid destination for as
tests/format/fprintf.c:37:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_9);
tests/format/fprintf.c:38:[value] warning: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
tests/format/fprintf.c:38:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_10);
tests/format/fprintf.c:41:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
tests/format/fprintf.c:41:[kernel:annot:missing-spec] warning: Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
[value] using specification for function __e_acsl_builtin_snprintf
tests/format/fprintf.c:41:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_11);
tests/format/fprintf.c:42:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_12);
......
......@@ -15,11 +15,11 @@ tests/format/printf.c:88:[kernel] warning: Floating-point constant 0.2 is not re
[e-acsl] warning: annotating undefined function `strcpy':
the generated program may miss memory instrumentation
if there are memory-related annotations.
FRAMAC_SHARE/libc/stdio.h:157:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
FRAMAC_SHARE/libc/unistd.h:781:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
FRAMAC_SHARE/libc/sys/wait.h:60:[kernel] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
:0:[kernel] warning: Neither code nor specification for function __fc_vla_free, generating default assigns from the prototype
:0:[kernel] warning: Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:157:[kernel:annot:missing-spec] warning: Neither code nor specification for function printf, generating default assigns from the prototype
FRAMAC_SHARE/libc/unistd.h:781:[kernel:annot:missing-spec] warning: Neither code nor specification for function fork, generating default assigns from the prototype
FRAMAC_SHARE/libc/sys/wait.h:60:[kernel:annot:missing-spec] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
:0:[kernel:annot:missing-spec] warning: Neither code nor specification for function __fc_vla_free, generating default assigns from the prototype
:0:[kernel:annot:missing-spec] warning: Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype
FRAMAC_SHARE/libc/string.h:319:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:320:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
......@@ -413,7 +413,7 @@ FRAMAC_SHARE/libc/stdlib.h:406:[e-acsl] warning: E-ACSL construct `assigns claus
[value] using specification for function __e_acsl_full_init
[value] using specification for function __e_acsl_mark_readonly
[value] using specification for function fork
tests/format/printf.c:179:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
tests/format/printf.c:179:[kernel:annot:missing-spec] warning: Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
[value] using specification for function __e_acsl_builtin_printf
[value] using specification for function exit
[value] using specification for function waitpid
......
tests/runtime/hidden_malloc.c:11:[kernel:typing:implicit-function-declaration] warning: Calling undeclared function realpath. Old style K&R code?
[e-acsl] beginning translation.
tests/runtime/hidden_malloc.c:11:[kernel] warning: Neither code nor specification for function realpath, generating default assigns from the prototype
tests/runtime/hidden_malloc.c:11:[kernel:annot:missing-spec] warning: Neither code nor specification for function realpath, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/runtime/hidden_malloc.c:11:[value] warning: Completely invalid destination for assigns clause *((char *)x_1 + (0 ..)).
Ignoring.
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/runtime/memalign.c:12:[kernel] warning: Neither code nor specification for function posix_memalign, generating default assigns from the prototype
tests/runtime/memalign.c:12:[kernel:annot:missing-spec] warning: Neither code nor specification for function posix_memalign, generating default assigns from the prototype
tests/runtime/memalign.c:14:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(memptr);
tests/runtime/memalign.c:14:[value:alarm] warning: out of bounds read. assert \valid_read(memptr);
[scope:rm_asserts] removing 2 assertion(s)
[e-acsl] beginning translation.
:0:[kernel] warning: Neither code nor specification for function __fc_vla_free, generating default assigns from the prototype
:0:[kernel] warning: Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype
:0:[kernel:annot:missing-spec] warning: Neither code nor specification for function __fc_vla_free, generating default assigns from the prototype
:0:[kernel:annot:missing-spec] warning: Neither code nor specification for function __fc_vla_alloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/runtime/vla.c:8:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/vla.c:12:[value:alarm] warning: assertion got status invalid (stopping propagation).
tests/temporal/t_fun_lib.c:20:[kernel:typing:implicit-function-declaration] warning: Calling undeclared function realpath. Old style K&R code?
[e-acsl] beginning translation.
tests/temporal/t_fun_lib.c:20:[kernel] warning: Neither code nor specification for function realpath, generating default assigns from the prototype
tests/temporal/t_fun_lib.c:20:[kernel:annot:missing-spec] warning: Neither code nor specification for function realpath, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/temporal/t_fun_lib.c:20:[value] warning: Completely invalid destination for assigns clause *(x_0 + (0 ..)). Ignoring.
tests/temporal/t_fun_lib.c:21:[value] warning: Completely invalid destination for assigns clause *(x_0 + (0 ..)). Ignoring.
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