Skip to content
Snippets Groups Projects
Commit b3f03461 authored by Boris Yakobowski's avatar Boris Yakobowski
Browse files

Update w.r.t. trunk changes (changes in stdlib.{c,h} for dynamic allocation)

parent 674dab3d
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 103 additions and 103 deletions
src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
+ 13
− 13
View file @ b3f03461
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:175:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/bts/bts1399.c:17:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. tests/bts/bts1399.c:17:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/bts/bts1399.c:17:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. tests/bts/bts1399.c:17:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/bts/bts1399.c:17:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/bts/bts1399.c:17:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
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.
FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown. FRAMAC_SHARE/libc/stdlib.h:181:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown.
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/base_addr.res.oracle
+ 6
− 6
View file @ b3f03461
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/base_addr.c:10:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. tests/e-acsl-runtime/base_addr.c:10:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/base_addr.c:10:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. tests/e-acsl-runtime/base_addr.c:10:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/base_addr.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/base_addr.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/base_addr.c:44:[value] warning: assertion got status unknown. tests/e-acsl-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.
tests/e-acsl-runtime/base_addr.c:45:[value] warning: assertion got status unknown. tests/e-acsl-runtime/base_addr.c:45:[value] warning: assertion got status unknown.
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/block_length.res.oracle
+ 6
− 6
View file @ b3f03461
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/block_length.c:12:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. tests/e-acsl-runtime/block_length.c:12:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/block_length.c:12:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. tests/e-acsl-runtime/block_length.c:12:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/block_length.c:12:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/block_length.c:12:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
[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.
FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/block_length.c:45:[value] warning: assertion got status unknown. tests/e-acsl-runtime/block_length.c:45:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/block_length.c:46:[value] warning: assertion got status unknown. tests/e-acsl-runtime/block_length.c:46:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/block_length.c:48:[value] warning: assertion got status unknown. tests/e-acsl-runtime/block_length.c:48:[value] warning: assertion got status unknown.
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
+ 6
− 6
View file @ b3f03461
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/call.c:16:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. tests/e-acsl-runtime/call.c:16:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/call.c:16:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. tests/e-acsl-runtime/call.c:16:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/call.c:16:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/call.c:16:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
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.
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle
+ 9
− 9
View file @ b3f03461
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:175:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
tests/e-acsl-runtime/freeable.c:15:[value] warning: assertion got status unknown. tests/e-acsl-runtime/freeable.c:15:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/freeable.c:15:[kernel] warning: accessing uninitialized left-value. assert \initialized(&p); tests/e-acsl-runtime/freeable.c:15:[kernel] warning: accessing uninitialized left-value. assert \initialized(&p);
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init_function.res.oracle
+ 6
− 6
View file @ b3f03461
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/init_function.c:9:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. tests/e-acsl-runtime/init_function.c:9:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/init_function.c:9:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. tests/e-acsl-runtime/init_function.c:9:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/init_function.c:9:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/init_function.c:9:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
+ 6
− 6
View file @ b3f03461
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/localvar.c:24:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. tests/e-acsl-runtime/localvar.c:24:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/localvar.c:24:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. tests/e-acsl-runtime/localvar.c:24:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/localvar.c:24:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/localvar.c:24:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
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.
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/offset.res.oracle
+ 6
− 6
View file @ b3f03461
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/offset.c:10:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. tests/e-acsl-runtime/offset.c:10:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/offset.c:10:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. tests/e-acsl-runtime/offset.c:10:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/offset.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/offset.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/offset.c:39:[value] warning: assertion got status unknown. tests/e-acsl-runtime/offset.c:39:[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.
tests/e-acsl-runtime/offset.c:40:[value] warning: assertion got status unknown. tests/e-acsl-runtime/offset.c:40:[value] warning: assertion got status unknown.
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
+ 6
− 6
View file @ b3f03461
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/ptr_init.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. tests/e-acsl-runtime/ptr_init.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/ptr_init.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. tests/e-acsl-runtime/ptr_init.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/ptr_init.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/ptr_init.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
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.
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+ 13
− 13
View file @ b3f03461
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:175:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid.c:31:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. tests/e-acsl-runtime/valid.c:31:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/valid.c:31:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. tests/e-acsl-runtime/valid.c:31:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/valid.c:31:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/valid.c:31:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
[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.
FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown. FRAMAC_SHARE/libc/stdlib.h:181:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid.c:47:[kernel] warning: accessing left-value that contains escaping addresses. tests/e-acsl-runtime/valid.c:47:[kernel] warning: accessing left-value that contains escaping addresses.
assert ¬\dangling(&a); assert ¬\dangling(&a);
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
+ 13
− 13
View file @ b3f03461
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:175:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:8:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. tests/e-acsl-runtime/valid_alias.c:8:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:8:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. tests/e-acsl-runtime/valid_alias.c:8:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:8:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/valid_alias.c:8:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
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.
FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown. FRAMAC_SHARE/libc/stdlib.h:181:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid_alias.c:17:[kernel] warning: accessing left-value that contains escaping addresses. tests/e-acsl-runtime/valid_alias.c:17:[kernel] warning: accessing left-value that contains escaping addresses.
assert ¬\dangling(&a); assert ¬\dangling(&a);
tests/e-acsl-runtime/valid_alias.c:17:[kernel] warning: accessing left-value that contains escaping addresses. tests/e-acsl-runtime/valid_alias.c:17:[kernel] warning: accessing left-value that contains escaping addresses.
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
+ 13
− 13
View file @ b3f03461
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:175:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/vector.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. tests/e-acsl-runtime/vector.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/vector.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. tests/e-acsl-runtime/vector.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
tests/e-acsl-runtime/vector.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. tests/e-acsl-runtime/vector.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported. FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation. FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
[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.
FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/vector.c:27:[value] warning: assertion got status unknown. tests/e-acsl-runtime/vector.c:27:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/vector.c:28:[value] warning: assertion got status unknown. tests/e-acsl-runtime/vector.c:28:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/vector.c:28:[kernel] warning: accessing uninitialized left-value. assert \initialized(&LAST); tests/e-acsl-runtime/vector.c:28:[kernel] warning: accessing uninitialized left-value. assert \initialized(&LAST);
FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown. FRAMAC_SHARE/libc/stdlib.h:181:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown.
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