Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • stable/zinc
  • 2699-wp-region-plugin-division-by-0-with-empty-region-node
  • stable/copper
  • stable/nickel
  • stable/cobalt
  • stable/iron
  • stable/manganese
  • stable/chromium
  • stable/vanadium
  • stable/titanium-backport
  • stable/titanium
  • stable/scandium
  • 30.0 protected
  • 30.0-beta protected
  • MIEL-2024-10 protected
  • 29.0 protected
  • 29.0-beta protected
  • 28.1 protected
  • 28.0 protected
  • MIEL-2023-10 protected
  • 28.0-beta protected
  • 27.1 protected
  • 27.0 protected
  • 27.0-beta protected
  • 26.1 protected
  • 26.0 protected
  • 26.0-beta protected
  • 25.0-r1 protected
  • pre-dune protected
  • 25.0 protected
  • 25.0-beta protected
  • 2022-03-23 protected
33 results
Blame Permalink
issue-eacsl-40.res.oracle 6.01 KiB 
[e-acsl] beginning translation.
[e-acsl] Warning: annotating undefined function `fclose':
  the generated program may miss memory instrumentation
  if there are memory-related annotations.
[e-acsl] Warning: annotating undefined function `fopen':
  the generated program may miss memory instrumentation
  if there are memory-related annotations.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:350: Warning: 
  E-ACSL construct `assigns clause in behavior' is not yet supported.
  Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:150: Warning: 
  E-ACSL construct `predicates with labels' is not yet supported.
  Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:151: Warning: 
  E-ACSL construct `predicates with labels' is not yet supported.
  Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:149: Warning: 
  E-ACSL construct `assigns clause in behavior' is not yet supported.
  Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:155: Warning: 
  E-ACSL construct
  `logic functions or predicates with no definition nor reads clause'
  is not yet supported.
  Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:118: Warning: 
  E-ACSL construct `assigns clause in behavior' is not yet supported.
  Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning: 
  function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning: 
  function __e_acsl_assert_register_int: precondition data->values == \null ||
                                                      \valid(data->values) got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning: 
  function __e_acsl_assert_register_ulong: precondition data->values == \null ||
                                                        \valid(data->values) got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning: 
  function __e_acsl_assert_register_ulong: precondition data->values == \null ||
                                                        \valid(data->values) got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning: 
  function __e_acsl_assert_register_mpz: precondition data->values == \null ||
                                                      \valid(data->values) got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning: 
  function __e_acsl_assert_register_ulong: precondition data->values == \null ||
                                                        \valid(data->values) got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning: 
  function __e_acsl_assert_register_int: precondition data->values == \null ||
                                                      \valid(data->values) got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning: 
  function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:350: Warning: 
  function __e_acsl_assert_register_ulong: precondition data->values == \null ||
                                                        \valid(data->values) got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:350: Warning: 
  function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:356: Warning: 
  function __e_acsl_assert_register_ulong: precondition data->values == \null ||
                                                        \valid(data->values) got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning: 
  function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning: 
  function __e_acsl_assert_register_int: precondition data->values == \null ||
                                                      \valid(data->values) got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning: 
  function __e_acsl_assert_register_ulong: precondition data->values == \null ||
                                                        \valid(data->values) got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning: 
  function __e_acsl_assert_register_mpz: precondition data->values == \null ||
                                                      \valid(data->values) got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning: 
  function __e_acsl_assert_register_mpz: precondition data->values == \null ||
                                                      \valid(data->values) got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning: 
  function __gen_e_acsl_fread: postcondition 'initialization' got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:120: Warning: 
  function __e_acsl_assert_register_ulong: precondition data->values == \null ||
                                                        \valid(data->values) got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:120: Warning: 
  function __e_acsl_assert_register_int: precondition data->values == \null ||
                                                      \valid(data->values) got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:120: Warning: 
  function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:122: Warning: 
  function __e_acsl_assert_register_int: precondition data->values == \null ||
                                                      \valid(data->values) got status unknown.
[eva:alarm] issue-eacsl-40.c:16: Warning: 
  function __e_acsl_assert_register_ulong: precondition data->values == \null ||
                                                        \valid(data->values) got status unknown.
[eva:alarm] issue-eacsl-40.c:16: Warning: 
  function __e_acsl_assert_register_int: precondition data->values == \null ||
                                                      \valid(data->values) got status unknown.
[eva:alarm] issue-eacsl-40.c:16: Warning: 
  function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] issue-eacsl-40.c:16: Warning: assertion got status unknown.