multidim.3.res.oracle

[kernel] Parsing multidim.c (with preprocessing)
[eva:experimental] Warning: The multidim domain is experimental.
[eva] Analyzing a complete application starting at main4
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  z[0..3] ∈ {0}
  nondet ∈ [--..--]
[eva:loop-unroll:partial] multidim.c:83: loop not completely unrolled
[eva] multidim.c:83: starting to merge loop iterations
[eva] multidim.c:85: starting to merge loop iterations
[eva] multidim.c:89: 
  Frama_C_domain_show_each:
  t : # cvalue: {42}
      # multidim: { [0] = {42}, [1] = {42}, [2] = {42}, [3] = {42} }
[eva] Recording results for main4
[eva] done for function main4
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main4:
  t[0..3] ∈ {42}
[from] Computing for function main4
[from] Done for function main4
[from] ====== DEPENDENCIES COMPUTED ======
  These dependencies hold at termination for the executions that terminate:
[from] Function main4:
  NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main4:
    t[0..3]; i; j
[inout] Inputs for function main4:
    \nothing