array.res.oracle

[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
[e-acsl] beginning translation.
[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
  __fc_random_counter ∈ {0}
  __fc_rand_max ∈ {32767}
  __fc_heap_status ∈ [--..--]
  __memory_size ∈ [--..--]
  T1[0..2] ∈ {0}
  T2[0..3] ∈ {0}
tests/e-acsl-runtime/array.i:12:[value] entering loop for the first time
tests/e-acsl-runtime/array.i:13:[value] entering loop for the first time
tests/e-acsl-runtime/array.i:15:[value] Assertion got status unknown.
[value] using specification for function __gmpz_init_set_si
share/e-acsl/e_acsl_gmp.h:61:[value] Function __gmpz_init_set_si: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:63:[value] Function __gmpz_init_set_si: postcondition got status valid.
share/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: postcondition got status unknown.
[value] using specification for function __gmpz_cmp
share/e-acsl/e_acsl_gmp.h:115:[value] Function __gmpz_cmp: precondition got status valid.
share/e-acsl/e_acsl_gmp.h:116:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
tests/e-acsl-runtime/array.i:16:[value] Assertion got status unknown.
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
  T1[0] ∈ {0; 2}
    [1..2] ∈ {0; 1; 2}
  T2[0] ∈ {0; 2}
    [1..3] ∈ {0; 2; 4; 6}
  __retres ∈ {0}