valid.res.oracle

[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/valid.c"
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:185:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:169:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                  Ignoring annotation.
tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                  Ignoring annotation.
tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                  Ignoring annotation.
tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                  Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                  Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
  random_counter ∈ {0}
  rand_max ∈ {32767}
  __fc_heap_status ∈ [--..--]
  __e_acsl_init ∈ [--..--]
  __e_acsl_internal_heap ∈ [--..--]
  __memory_size ∈ [--..--]
  X ∈ {0}
  Z ∈ {0}
[value] using specification for function __store_block
[value] using specification for function __full_init
tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
FRAMAC_SHARE/libc/stdlib.h:160:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:165:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/valid.c:37:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:39:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:15:[value] Function __e_acsl_f: precondition got status valid.
tests/e-acsl-runtime/valid.c:15:[value] Function f: precondition got status valid.
tests/e-acsl-runtime/valid.c:19:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
tests/e-acsl-runtime/valid.c:21:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:16:[value] Function f: postcondition got status valid.
tests/e-acsl-runtime/valid.c:16:[value] Function __e_acsl_f: postcondition got status valid.
tests/e-acsl-runtime/valid.c:41:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:43:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:46:[value] Assertion got status valid.
[value] using specification for function __valid_read
tests/e-acsl-runtime/valid.c:47:[value] Assertion got status valid.
FRAMAC_SHARE/libc/stdlib.h:175:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses: assert \specified(&a);
tests/e-acsl-runtime/valid.c:49:[kernel] warning: completely indeterminate value in a.
tests/e-acsl-runtime/valid.c:49:[value] all evaluations are invalid for function call argument
        (void *)a
tests/e-acsl-runtime/valid.c:50:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:30:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======