taint.res.oracle

[kernel] Parsing tests/value/taint.c (with preprocessing)
[eva:experimental] Warning: The taint domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  undet ∈ [--..--]
  tainted ∈ {0}
[eva] computing for function taint_basic <- main.
  Called from tests/value/taint.c:143.
[eva] tests/value/taint.c:34: 
  Frama_C_dump_each:
  # taint:
  Locations (data):
    tainted; t; u; x; buf[0]
  Locations (control):
    w
  ==END OF DUMP==
[eva] Recording results for taint_basic
[eva] Done for function taint_basic
[eva] computing for function taint_assume_1 <- main.
  Called from tests/value/taint.c:146.
[eva:loop-unroll] tests/value/taint.c:47: Automatic loop unrolling.
[eva] tests/value/taint.c:48: 
  Frama_C_dump_each:
  # taint:
  Locations (data):
    \nothing
  Locations (control):
    \nothing
  ==END OF DUMP==
[eva] tests/value/taint.c:51: 
  Frama_C_dump_each:
  # taint:
  Locations (data):
    \nothing
  Locations (control):
    \nothing
  ==END OF DUMP==
[eva] tests/value/taint.c:48: 
  Frama_C_dump_each:
  # taint:
  Locations (data):
    x
  Locations (control):
    \nothing
  ==END OF DUMP==
[eva] tests/value/taint.c:51: 
  Frama_C_dump_each:
  # taint:
  Locations (data):
    x; y
  Locations (control):
    y
  ==END OF DUMP==
[eva] tests/value/taint.c:48: 
  Frama_C_dump_each:
  # taint:
  Locations (data):
    x; y
  Locations (control):
    x; y
  ==END OF DUMP==
[eva] tests/value/taint.c:51: 
  Frama_C_dump_each:
  # taint:
  Locations (data):
    x; y
  Locations (control):
    x; y
  ==END OF DUMP==
[eva] tests/value/taint.c:61: 
  Frama_C_dump_each:
  # taint:
  Locations (data):
    x; y
  Locations (control):
    x; y
  ==END OF DUMP==
[eva] Recording results for taint_assume_1
[eva] Done for function taint_assume_1
[eva] computing for function taint_assume_2 <- main.
  Called from tests/value/taint.c:147.
[eva] tests/value/taint.c:76: 
  Frama_C_dump_each:
  # taint:
  Locations (data):
    x; y
  Locations (control):
    x; y
  ==END OF DUMP==
[eva] Recording results for taint_assume_2
[eva] Done for function taint_assume_2
[eva] computing for function taint_undet_locs <- main.
  Called from tests/value/taint.c:149.
[eva] tests/value/taint.c:88: 
  Frama_C_dump_each:
  # taint:
  Locations (data):
    x; y; t
  Locations (control):
    \nothing
  ==END OF DUMP==
[eva] Recording results for taint_undet_locs
[eva] Done for function taint_undet_locs
[eva] computing for function taint_spec_assigns <- main.
  Called from tests/value/taint.c:152.
[eva] using specification for function taint_spec_assigns
[eva] Done for function taint_spec_assigns
[eva] tests/value/taint.c:154: 
  Frama_C_domain_show_each:
  l : # taint: false
[eva] computing for function taint_goto_1 <- main.
  Called from tests/value/taint.c:156.
[eva] tests/value/taint.c:107: 
  Frama_C_dump_each:
  # taint:
  Locations (data):
    t
  Locations (control):
    x
  ==END OF DUMP==
[eva] Recording results for taint_goto_1
[eva] Done for function taint_goto_1
[eva] computing for function taint_goto_2 <- main.
  Called from tests/value/taint.c:157.
[eva] tests/value/taint.c:127: 
  Frama_C_dump_each:
  # taint:
  Locations (data):
    t
  Locations (control):
    x; y
  ==END OF DUMP==
[eva] Recording results for taint_goto_2
[eva] Done for function taint_goto_2
[eva] computing for function taint_call <- main.
  Called from tests/value/taint.c:160.
[eva] computing for function taint_basic <- taint_call <- main.
  Called from tests/value/taint.c:135.
[eva] tests/value/taint.c:34: 
  Frama_C_dump_each:
  # taint:
  Locations (data):
    tainted; t; u; x; buf[0]; t
  Locations (control):
    u; w; x; y; buf[0..1]
  ==END OF DUMP==
[eva] Recording results for taint_basic
[eva] Done for function taint_basic
[eva] tests/value/taint.c:138: 
  Frama_C_domain_show_each:
  x : # taint: false
[eva] Recording results for taint_call
[eva] Done for function taint_call
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function taint_assume_1:
  x ∈ {3}
  y ∈ {6}
  z ∈ {1}
[eva:final-states] Values at end of function taint_assume_2:
  x ∈ {11}
  y ∈ {10}
[eva:final-states] Values at end of function taint_basic:
  u ∈ {0; 1}
  w ∈ {2}
  x ∈ {1}
  y ∈ {0}
  buf[0] ∈ {2}
     [1] ∈ {1}
[eva:final-states] Values at end of function taint_call:
  x ∈ {0}
[eva:final-states] Values at end of function taint_goto_1:
  x ∈ {1} or UNINITIALIZED
  y ∈ {0}
  z ∈ {1}
  t ∈ [--..--]
[eva:final-states] Values at end of function taint_goto_2:
  x ∈ [--..--]
  y ∈ {0} or UNINITIALIZED
  z ∈ {1} or UNINITIALIZED
  t ∈ [--..--]
[eva:final-states] Values at end of function taint_undet_locs:
  x ∈ {0}
  y ∈ {0}
  t ∈ {0}
  p ∈ {{ &x ; &y }}
[eva:final-states] Values at end of function main:
  tainted ∈ {0}
  l ∈ [--..--] or UNINITIALIZED
  __retres ∈ {0}
[from] Computing for function taint_assume_1
[from] Done for function taint_assume_1
[from] Computing for function taint_assume_2
[from] Done for function taint_assume_2
[from] Computing for function taint_basic
[from] Done for function taint_basic
[from] Computing for function taint_call
[from] Done for function taint_call
[from] Computing for function taint_goto_1
[from] Done for function taint_goto_1
[from] Computing for function taint_goto_2
[from] Done for function taint_goto_2
[from] Computing for function taint_undet_locs
[from] Done for function taint_undet_locs
[from] Computing for function main
[from] Computing for function taint_spec_assigns <-main
[from] Done for function taint_spec_assigns
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
  These dependencies hold at termination for the executions that terminate:
[from] Function taint_assume_1:
  NO EFFECTS
[from] Function taint_assume_2:
  NO EFFECTS
[from] Function taint_basic:
  NO EFFECTS
[from] Function taint_call:
  NO EFFECTS
[from] Function taint_goto_1:
  NO EFFECTS
[from] Function taint_goto_2:
  NO EFFECTS
[from] Function taint_spec_assigns:
  l FROM t
[from] Function taint_undet_locs:
  NO EFFECTS
[from] Function main:
  tainted FROM \nothing
  \result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function taint_assume_1:
    x; y; z
[inout] Inputs for function taint_assume_1:
    \nothing
[inout] Out (internal) for function taint_assume_2:
    x; y
[inout] Inputs for function taint_assume_2:
    \nothing
[inout] Out (internal) for function taint_basic:
    u; w; x; y; buf[0..1]
[inout] Inputs for function taint_basic:
    undet
[inout] Out (internal) for function taint_call:
    x
[inout] Inputs for function taint_call:
    undet
[inout] Out (internal) for function taint_goto_1:
    x; y; z; t
[inout] Inputs for function taint_goto_1:
    undet
[inout] Out (internal) for function taint_goto_2:
    x; y; z; t
[inout] Inputs for function taint_goto_2:
    undet
[inout] Out (internal) for function taint_undet_locs:
    x; y; t; p; tmp
[inout] Inputs for function taint_undet_locs:
    undet
[inout] Out (internal) for function main:
    tainted; l; __retres
[inout] Inputs for function main:
    undet; tainted