array.1.res.oracle

[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:initial-state] Values of globals at initialization
  __fc_rand_max ∈ {32767}
  __fc_heap_status ∈ [--..--]
  __e_acsl_init ∈ [--..--]
  __e_acsl_internal_heap ∈ [--..--]
  __e_acsl_heap_allocation_size ∈ [--..--]
  __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
  __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
  __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
  T1[0..2] ∈ {0}
  T2[0..3] ∈ {0}
[value] using specification for function __e_acsl_memory_init
tests/gmp/array.i:10:[value] entering loop for the first time
tests/gmp/array.i:11:[value] entering loop for the first time
tests/gmp/array.i:13:[value] warning: assertion got status unknown.
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
tests/gmp/array.i:14:[value] warning: assertion got status unknown.
[value] done for function main