Commit 6b8742b1 authored by Valentin Perrelle's avatar Valentin Perrelle
Browse files

Merge branch 'fix/andre/libc-popen-pipe' into 'master'

synchronize with frama-c/frama-c!1730

See merge request frama-c/e-acsl!202
parents 69f803b6 20db51ab
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdio.h:156:[kernel] warning: Neither code nor specification for function printf, 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
[e-acsl] translation done in project "e-acsl".
......@@ -10,11 +10,11 @@ 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:152:[kernel] warning: Neither code nor specification for function fprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:156:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:158:[kernel] warning: Neither code nor specification for function snprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:160:[kernel] warning: Neither code nor specification for function sprintf, generating default assigns from the prototype
FRAMAC_SHARE/libc/stdio.h:349:[kernel] warning: Neither code nor specification for function dprintf, generating default assigns from the prototype
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:93:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
......
......@@ -15,7 +15,7 @@ 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:156:[kernel] warning: Neither code nor specification for function printf, 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/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
......
......@@ -83,6 +83,14 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& extra_lbits));
__e_acsl_store_block((void *)(strings),(size_t)32);
__e_acsl_full_init((void *)(& strings));
__e_acsl_temporal_store_nblock((void *)(& strings[0][0]),
(void *)__gen_e_acsl_literal_string_4);
__e_acsl_temporal_store_nblock((void *)(& strings[0][1]),
(void *)__gen_e_acsl_literal_string_3);
__e_acsl_temporal_store_nblock((void *)(& strings[1][0]),
(void *)__gen_e_acsl_literal_string_2);
__e_acsl_temporal_store_nblock((void *)(& strings[1][1]),
(void *)__gen_e_acsl_literal_string);
__e_acsl_temporal_store_nblock((void *)(& descs2[0].desc.extra_bits),
(void *)(extra_lbits));
__e_acsl_temporal_store_nblock((void *)(& descs2[1].desc.extra_bits),
......@@ -95,14 +103,6 @@ void __e_acsl_globals_init(void)
(void *)(extra_lbits));
__e_acsl_temporal_store_nblock((void *)(& l_desc.extra_bits),
(void *)(extra_lbits));
__e_acsl_temporal_store_nblock((void *)(& strings[0][0]),
(void *)__gen_e_acsl_literal_string_4);
__e_acsl_temporal_store_nblock((void *)(& strings[0][1]),
(void *)__gen_e_acsl_literal_string_3);
__e_acsl_temporal_store_nblock((void *)(& strings[1][0]),
(void *)__gen_e_acsl_literal_string_2);
__e_acsl_temporal_store_nblock((void *)(& strings[1][1]),
(void *)__gen_e_acsl_literal_string);
return;
}
......
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