[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/behaviors1.i (no preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
  nondet ∈ [--..--]
  T[0..9] ∈ {0}
[value] computing for function test_none <- main.
        Called from tests/value/behaviors1.i:623.
[value] computing for function f_none <- test_none <- main.
        Called from tests/value/behaviors1.i:328.
[value] using specification for function f_none
tests/value/behaviors1.i:328:[value] function f_none, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:328:[value] function f_none, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:328:[value] function f_none, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_none
[value] computing for function f_none <- test_none <- main.
        Called from tests/value/behaviors1.i:329.
tests/value/behaviors1.i:329:[value] function f_none, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:329:[value] function f_none, behavior b3: assumes got status invalid; behavior not evaluated.
[value] Done for function f_none
[value] computing for function f_none <- test_none <- main.
        Called from tests/value/behaviors1.i:330.
tests/value/behaviors1.i:330:[value] function f_none, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:330:[value] function f_none, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_none
[value] computing for function f_none <- test_none <- main.
        Called from tests/value/behaviors1.i:331.
[value] Done for function f_none
[value] Recording results for test_none
[value] Done for function test_none
[value] computing for function test_comp_disj <- main.
        Called from tests/value/behaviors1.i:624.
[value] computing for function f_comp_disj <- test_comp_disj <- main.
        Called from tests/value/behaviors1.i:342.
[value] using specification for function f_comp_disj
tests/value/behaviors1.i:342:[value] function f_comp_disj, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:342:[value] function f_comp_disj, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:342:[value] function f_comp_disj, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_comp_disj
[value] computing for function f_comp_disj <- test_comp_disj <- main.
        Called from tests/value/behaviors1.i:350.
tests/value/behaviors1.i:350:[value] function f_comp_disj, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:350:[value] function f_comp_disj, behavior b3: assumes got status invalid; behavior not evaluated.
[value] Done for function f_comp_disj
[value] computing for function f_comp_disj <- test_comp_disj <- main.
        Called from tests/value/behaviors1.i:358.
tests/value/behaviors1.i:358:[value] function f_comp_disj, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:358:[value] function f_comp_disj, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_comp_disj
[value] computing for function f_comp_disj <- test_comp_disj <- main.
        Called from tests/value/behaviors1.i:366.
[value] Done for function f_comp_disj
[value] Recording results for test_comp_disj
[value] Done for function test_comp_disj
[value] computing for function test_comp <- main.
        Called from tests/value/behaviors1.i:625.
[value] computing for function f_comp <- test_comp <- main.
        Called from tests/value/behaviors1.i:388.
[value] using specification for function f_comp
tests/value/behaviors1.i:388:[value] function f_comp, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:388:[value] function f_comp, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:388:[value] function f_comp, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_comp
[value] computing for function f_comp <- test_comp <- main.
        Called from tests/value/behaviors1.i:389.
tests/value/behaviors1.i:389:[value] function f_comp, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:389:[value] function f_comp, behavior b3: assumes got status invalid; behavior not evaluated.
[value] Done for function f_comp
[value] computing for function f_comp <- test_comp <- main.
        Called from tests/value/behaviors1.i:390.
tests/value/behaviors1.i:390:[value] function f_comp, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:390:[value] function f_comp, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_comp
[value] computing for function f_comp <- test_comp <- main.
        Called from tests/value/behaviors1.i:391.
[value] Done for function f_comp
[value] Recording results for test_comp
[value] Done for function test_comp
[value] computing for function test_disj <- main.
        Called from tests/value/behaviors1.i:626.
[value] computing for function f_disj <- test_disj <- main.
        Called from tests/value/behaviors1.i:377.
[value] using specification for function f_disj
tests/value/behaviors1.i:377:[value] function f_disj, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:377:[value] function f_disj, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:377:[value] function f_disj, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_disj
[value] computing for function f_disj <- test_disj <- main.
        Called from tests/value/behaviors1.i:378.
tests/value/behaviors1.i:378:[value] function f_disj, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:378:[value] function f_disj, behavior b3: assumes got status invalid; behavior not evaluated.
[value] Done for function f_disj
[value] computing for function f_disj <- test_disj <- main.
        Called from tests/value/behaviors1.i:379.
tests/value/behaviors1.i:379:[value] function f_disj, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:379:[value] function f_disj, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_disj
[value] computing for function f_disj <- test_disj <- main.
        Called from tests/value/behaviors1.i:380.
[value] Done for function f_disj
[value] Recording results for test_disj
[value] Done for function test_disj
[value] computing for function test_123_comp_disj <- main.
        Called from tests/value/behaviors1.i:627.
[value] computing for function f_123_comp_disj <- test_123_comp_disj <- main.
        Called from tests/value/behaviors1.i:399.
[value] using specification for function f_123_comp_disj
tests/value/behaviors1.i:399:[value] function f_123_comp_disj, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:399:[value] function f_123_comp_disj, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:399:[value] function f_123_comp_disj, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_123_comp_disj
[value] computing for function f_123_comp_disj <- test_123_comp_disj <- main.
        Called from tests/value/behaviors1.i:400.
tests/value/behaviors1.i:400:[value] function f_123_comp_disj, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:400:[value] function f_123_comp_disj, behavior b3: assumes got status invalid; behavior not evaluated.
[value] Done for function f_123_comp_disj
[value] computing for function f_123_comp_disj <- test_123_comp_disj <- main.
        Called from tests/value/behaviors1.i:401.
tests/value/behaviors1.i:401:[value] function f_123_comp_disj, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:401:[value] function f_123_comp_disj, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_123_comp_disj
[value] computing for function f_123_comp_disj <- test_123_comp_disj <- main.
        Called from tests/value/behaviors1.i:402.
[value] Done for function f_123_comp_disj
[value] Recording results for test_123_comp_disj
[value] Done for function test_123_comp_disj
[value] computing for function test_123_comp_disj_2345_disj <- main.
        Called from tests/value/behaviors1.i:628.
[value] computing for function f_123_comp_disj_2345_disj <- 
                                test_123_comp_disj_2345_disj <- main.
        Called from tests/value/behaviors1.i:410.
[value] using specification for function f_123_comp_disj_2345_disj
tests/value/behaviors1.i:410:[value] function f_123_comp_disj_2345_disj, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:410:[value] function f_123_comp_disj_2345_disj, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:410:[value] function f_123_comp_disj_2345_disj, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_123_comp_disj_2345_disj
[value] computing for function f_123_comp_disj_2345_disj <- 
                                test_123_comp_disj_2345_disj <- main.
        Called from tests/value/behaviors1.i:411.
tests/value/behaviors1.i:411:[value] function f_123_comp_disj_2345_disj, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:411:[value] function f_123_comp_disj_2345_disj, behavior b3: assumes got status invalid; behavior not evaluated.
[value] Done for function f_123_comp_disj_2345_disj
[value] computing for function f_123_comp_disj_2345_disj <- 
                                test_123_comp_disj_2345_disj <- main.
        Called from tests/value/behaviors1.i:412.
tests/value/behaviors1.i:412:[value] function f_123_comp_disj_2345_disj, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:412:[value] function f_123_comp_disj_2345_disj, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_123_comp_disj_2345_disj
[value] computing for function f_123_comp_disj_2345_disj <- 
                                test_123_comp_disj_2345_disj <- main.
        Called from tests/value/behaviors1.i:413.
[value] Done for function f_123_comp_disj_2345_disj
[value] Recording results for test_123_comp_disj_2345_disj
[value] Done for function test_123_comp_disj_2345_disj
[value] computing for function test_123_comp_disj_2345_comp <- main.
        Called from tests/value/behaviors1.i:629.
[value] computing for function f_123_comp_disj_2345_comp <- 
                                test_123_comp_disj_2345_comp <- main.
        Called from tests/value/behaviors1.i:421.
[value] using specification for function f_123_comp_disj_2345_comp
tests/value/behaviors1.i:421:[value] function f_123_comp_disj_2345_comp, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:421:[value] function f_123_comp_disj_2345_comp, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:421:[value] function f_123_comp_disj_2345_comp, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_123_comp_disj_2345_comp
[value] computing for function f_123_comp_disj_2345_comp <- 
                                test_123_comp_disj_2345_comp <- main.
        Called from tests/value/behaviors1.i:422.
tests/value/behaviors1.i:422:[value] function f_123_comp_disj_2345_comp, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:422:[value] function f_123_comp_disj_2345_comp, behavior b3: assumes got status invalid; behavior not evaluated.
[value] Done for function f_123_comp_disj_2345_comp
[value] computing for function f_123_comp_disj_2345_comp <- 
                                test_123_comp_disj_2345_comp <- main.
        Called from tests/value/behaviors1.i:423.
tests/value/behaviors1.i:423:[value] function f_123_comp_disj_2345_comp, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:423:[value] function f_123_comp_disj_2345_comp, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_123_comp_disj_2345_comp
[value] computing for function f_123_comp_disj_2345_comp <- 
                                test_123_comp_disj_2345_comp <- main.
        Called from tests/value/behaviors1.i:424.
[value] Done for function f_123_comp_disj_2345_comp
[value] Recording results for test_123_comp_disj_2345_comp
[value] Done for function test_123_comp_disj_2345_comp
[value] computing for function test_123_disj_2345_comp_disj <- main.
        Called from tests/value/behaviors1.i:630.
[value] computing for function f_123_disj_2345_comp_disj <- 
                                test_123_disj_2345_comp_disj <- main.
        Called from tests/value/behaviors1.i:432.
[value] using specification for function f_123_disj_2345_comp_disj
tests/value/behaviors1.i:432:[value] function f_123_disj_2345_comp_disj, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:432:[value] function f_123_disj_2345_comp_disj, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:432:[value] function f_123_disj_2345_comp_disj, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_123_disj_2345_comp_disj
[value] computing for function f_123_disj_2345_comp_disj <- 
                                test_123_disj_2345_comp_disj <- main.
        Called from tests/value/behaviors1.i:433.
tests/value/behaviors1.i:433:[value] function f_123_disj_2345_comp_disj, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:433:[value] function f_123_disj_2345_comp_disj, behavior b3: assumes got status invalid; behavior not evaluated.
[value] Done for function f_123_disj_2345_comp_disj
[value] computing for function f_123_disj_2345_comp_disj <- 
                                test_123_disj_2345_comp_disj <- main.
        Called from tests/value/behaviors1.i:434.
tests/value/behaviors1.i:434:[value] function f_123_disj_2345_comp_disj, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:434:[value] function f_123_disj_2345_comp_disj, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_123_disj_2345_comp_disj
[value] computing for function f_123_disj_2345_comp_disj <- 
                                test_123_disj_2345_comp_disj <- main.
        Called from tests/value/behaviors1.i:435.
[value] Done for function f_123_disj_2345_comp_disj
[value] Recording results for test_123_disj_2345_comp_disj
[value] Done for function test_123_disj_2345_comp_disj
[value] computing for function test_123_comp_2345_comp_disj <- main.
        Called from tests/value/behaviors1.i:631.
[value] computing for function f_123_comp_2345_comp_disj <- 
                                test_123_comp_2345_comp_disj <- main.
        Called from tests/value/behaviors1.i:443.
[value] using specification for function f_123_comp_2345_comp_disj
tests/value/behaviors1.i:443:[value] function f_123_comp_2345_comp_disj, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:443:[value] function f_123_comp_2345_comp_disj, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:443:[value] function f_123_comp_2345_comp_disj, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_123_comp_2345_comp_disj
[value] computing for function f_123_comp_2345_comp_disj <- 
                                test_123_comp_2345_comp_disj <- main.
        Called from tests/value/behaviors1.i:444.
tests/value/behaviors1.i:444:[value] function f_123_comp_2345_comp_disj, behavior b2: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:444:[value] function f_123_comp_2345_comp_disj, behavior b3: assumes got status invalid; behavior not evaluated.
[value] Done for function f_123_comp_2345_comp_disj
[value] computing for function f_123_comp_2345_comp_disj <- 
                                test_123_comp_2345_comp_disj <- main.
        Called from tests/value/behaviors1.i:445.
tests/value/behaviors1.i:445:[value] function f_123_comp_2345_comp_disj, behavior b3: assumes got status invalid; behavior not evaluated.
tests/value/behaviors1.i:445:[value] function f_123_comp_2345_comp_disj, behavior b5: assumes got status invalid; behavior not evaluated.
[value] Done for function f_123_comp_2345_comp_disj
[value] computing for function f_123_comp_2345_comp_disj <- 
                                test_123_comp_2345_comp_disj <- main.
        Called from tests/value/behaviors1.i:446.
[value] Done for function f_123_comp_2345_comp_disj
[value] Recording results for test_123_comp_2345_comp_disj
[value] Done for function test_123_comp_2345_comp_disj
[value] computing for function test_assigns <- main.
        Called from tests/value/behaviors1.i:632.
[value] computing for function f <- test_assigns <- main.
        Called from tests/value/behaviors1.i:473.
[value] using specification for function f
[value] Done for function f
tests/value/behaviors1.i:473:[value] Assigning imprecise value to p1.
        The imprecision originates from Library function
        {tests/value/behaviors1.i:473}
[value] computing for function f <- test_assigns <- main.
        Called from tests/value/behaviors1.i:474.
[value] Done for function f
tests/value/behaviors1.i:474:[value] Assigning imprecise value to p2.
        The imprecision originates from Library function
        {tests/value/behaviors1.i:474}
[value] computing for function f <- test_assigns <- main.
        Called from tests/value/behaviors1.i:475.
[value] Done for function f
[value] Recording results for test_assigns
[value] Done for function test_assigns
[value] computing for function test_assigns2 <- main.
        Called from tests/value/behaviors1.i:633.
[value] computing for function f2 <- test_assigns2 <- main.
        Called from tests/value/behaviors1.i:490.
[value] using specification for function f2
tests/value/behaviors1.i:480:[value] function f2: precondition got status valid.
[value] Done for function f2
[value] Recording results for test_assigns2
[value] Done for function test_assigns2
[value] computing for function test_small1 <- main.
        Called from tests/value/behaviors1.i:634.
[value] computing for function f3 <- test_small1 <- main.
        Called from tests/value/behaviors1.i:506.
tests/value/behaviors1.i:506:[kernel] warning: No code nor implicit assigns clause for function f3, generating default assigns from the prototype
[value] using specification for function f3
tests/value/behaviors1.i:494:[value] warning: function f3: precondition got status unknown.
tests/value/behaviors1.i:497:[value] warning: function f3, behavior b1: precondition got status invalid.
[value] Done for function f3
[value] Recording results for test_small1
[value] Done for function test_small1
[value] computing for function test_small2 <- main.
        Called from tests/value/behaviors1.i:635.
[value] computing for function f4 <- test_small2 <- main.
        Called from tests/value/behaviors1.i:521.
tests/value/behaviors1.i:521:[kernel] warning: No code nor implicit assigns clause for function f4, generating default assigns from the prototype
[value] using specification for function f4
tests/value/behaviors1.i:510:[value] warning: function f4: precondition got status unknown.
tests/value/behaviors1.i:513:[value] warning: function f4, behavior b1: precondition got status invalid.
tests/value/behaviors1.i:513:[value] function f4, behavior b1: no state left in which to evaluate precondition, status not computed.
tests/value/behaviors1.i:521:[value] function f4, behavior b1: requires got status invalid; postconditions not evaluated.
[value] Done for function f4
[value] Recording results for test_small2
[value] Done for function test_small2
[value] computing for function test_small3 <- main.
        Called from tests/value/behaviors1.i:636.
[value] computing for function f5 <- test_small3 <- main.
        Called from tests/value/behaviors1.i:534.
tests/value/behaviors1.i:534:[kernel] warning: No code nor implicit assigns clause for function f5, generating default assigns from the prototype
[value] using specification for function f5
[value] Done for function f5
[value] Recording results for test_small3
[value] Done for function test_small3
[value] computing for function test_small4 <- main.
        Called from tests/value/behaviors1.i:637.
[value] computing for function f6 <- test_small4 <- main.
        Called from tests/value/behaviors1.i:548.
tests/value/behaviors1.i:548:[kernel] warning: No code nor implicit assigns clause for function f6, generating default assigns from the prototype
[value] using specification for function f6
[value] Done for function f6
[value] Recording results for test_small4
[value] Done for function test_small4
[value] computing for function test_small5 <- main.
        Called from tests/value/behaviors1.i:638.
[value] computing for function f7 <- test_small5 <- main.
        Called from tests/value/behaviors1.i:561.
tests/value/behaviors1.i:561:[kernel] warning: No code nor implicit assigns clause for function f7, generating default assigns from the prototype
[value] using specification for function f7
tests/value/behaviors1.i:552:[value] warning: function f7: precondition got status unknown.
[value] Done for function f7
[value] Recording results for test_small5
[value] Done for function test_small5
[value] computing for function test_small6 <- main.
        Called from tests/value/behaviors1.i:639.
[value] computing for function f8 <- test_small6 <- main.
        Called from tests/value/behaviors1.i:576.
[value] using specification for function f8
tests/value/behaviors1.i:565:[value] function f8: precondition got status valid.
[value] Done for function f8
[value] Recording results for test_small6
[value] Done for function test_small6
[value] computing for function test_promote <- main.
        Called from tests/value/behaviors1.i:640.
[value] computing for function f9 <- test_promote <- main.
        Called from tests/value/behaviors1.i:594.
[value] using specification for function f9
tests/value/behaviors1.i:594:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
tests/value/behaviors1.i:594:[value] function f9, behavior b1: assumes got status invalid; behavior not evaluated.
[value] Done for function f9
[value] Recording results for test_promote
[value] Done for function test_promote
[value] computing for function test_narrow <- main.
        Called from tests/value/behaviors1.i:641.
[value] computing for function f10 <- test_narrow <- main.
        Called from tests/value/behaviors1.i:619.
[value] using specification for function f10
tests/value/behaviors1.i:619:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] Done for function f10
[value] Recording results for test_narrow
[value] Done for function test_narrow
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function test_123_comp_2345_comp_disj:
  a ∈ [--..--]
  b ∈ [--..--]
  c1 ∈ {4} or UNINITIALIZED
  c2 ∈ {4; 5} or UNINITIALIZED
  c3 ∈ {2; 4} or UNINITIALIZED
  c4 ∈ {2; 3; 4; 5} or UNINITIALIZED
[value:final-states] Values at end of function test_123_comp_disj:
  a ∈ [--..--]
  b ∈ [--..--]
  c1 ∈ {4} or UNINITIALIZED
  c2 ∈ {4; 5} or UNINITIALIZED
  c3 ∈ {2; 4; 5} or UNINITIALIZED
  c4 ∈ {2; 3; 4; 5} or UNINITIALIZED
[value:final-states] Values at end of function test_123_comp_disj_2345_comp:
  a ∈ [--..--]
  b ∈ [--..--]
  c1 ∈ {4} or UNINITIALIZED
  c2 ∈ {4; 5} or UNINITIALIZED
  c3 ∈ {2; 4} or UNINITIALIZED
  c4 ∈ {2; 3; 4; 5} or UNINITIALIZED
[value:final-states] Values at end of function test_123_comp_disj_2345_disj:
  a ∈ [--..--]
  b ∈ [--..--]
  c1 ∈ {4} or UNINITIALIZED
  c2 ∈ {4; 5} or UNINITIALIZED
  c3 ∈ {2; 4; 5} or UNINITIALIZED
  c4 ∈ {2; 3; 4; 5} or UNINITIALIZED
[value:final-states] Values at end of function test_123_disj_2345_comp_disj:
  a ∈ [--..--]
  b ∈ [--..--]
  c1 ∈ {4} or UNINITIALIZED
  c2 ∈ {4; 5} or UNINITIALIZED
  c3 ∈ {2; 4} or UNINITIALIZED
  c4 ∈ {2; 3; 4; 5} or UNINITIALIZED
[value:final-states] Values at end of function test_assigns:
  p1 ∈
    {{ garbled mix of &{a}
     (origin: Library function {tests/value/behaviors1.i:473}) }}
  p2 ∈
    {{ garbled mix of &{b}
     (origin: Library function {tests/value/behaviors1.i:474}) }}
  p3 ∈ [--..--]
[value:final-states] Values at end of function test_assigns2:
  T[0..4] ∈ [--..--]
   [5..9] ∈ {0}
  p ∈ {{ &T[0] }}
[value:final-states] Values at end of function test_comp:
  a ∈ [--..--]
  b ∈ [--..--]
  c1 ∈ {4} or UNINITIALIZED
  c2 ∈ {4; 5} or UNINITIALIZED
  c3 ∈ {2; 4} or UNINITIALIZED
  c4 ∈ {2; 3; 4; 5} or UNINITIALIZED
[value:final-states] Values at end of function test_comp_disj:
  a ∈ [--..--]
  b ∈ [--..--]
  c1 ∈ {4} or UNINITIALIZED
  c2 ∈ {4; 5} or UNINITIALIZED
  c3 ∈ {2; 4} or UNINITIALIZED
  c4 ∈ {2; 3; 4; 5} or UNINITIALIZED
[value:final-states] Values at end of function test_disj:
  a ∈ [--..--]
  b ∈ [--..--]
  c1 ∈ {4} or UNINITIALIZED
  c2 ∈ {4; 5} or UNINITIALIZED
  c3 ∈ [1..2147483647] or UNINITIALIZED
  c4 ∈ [1..2147483647] or UNINITIALIZED
[value:final-states] Values at end of function test_narrow:
  r ∈ {100; 200; 300}
[value:final-states] Values at end of function test_none:
  a ∈ [--..--]
  b ∈ [--..--]
  c1 ∈ {4} or UNINITIALIZED
  c2 ∈ {4; 5} or UNINITIALIZED
  c3 ∈ [1..2147483647] or UNINITIALIZED
  c4 ∈ [1..2147483647] or UNINITIALIZED
[value:final-states] Values at end of function test_promote:
  x ∈ [--..--]
  r ∈ {1}
[value:final-states] Values at end of function test_small1:
  x ∈ {4}
[value:final-states] Values at end of function test_small2:
  x ∈ {2; 4}
[value:final-states] Values at end of function test_small3:
  r ∈ [0..1000]
[value:final-states] Values at end of function test_small4:
  r ∈ [0..1000]
[value:final-states] Values at end of function test_small5:
  r ∈ [--..--]
[value:final-states] Values at end of function test_small6:
  a ∈ [--..--]
  p ∈ {{ &a }}
[value:final-states] Values at end of function main:
  T[0..4] ∈ [--..--]
   [5..9] ∈ {0}
  __retres ∈ {0}
[from] Computing for function test_123_comp_2345_comp_disj
[from] Computing for function f_123_comp_2345_comp_disj <-test_123_comp_2345_comp_disj
[from] Done for function f_123_comp_2345_comp_disj
[from] Done for function test_123_comp_2345_comp_disj
[from] Computing for function test_123_comp_disj
[from] Computing for function f_123_comp_disj <-test_123_comp_disj
[from] Done for function f_123_comp_disj
[from] Done for function test_123_comp_disj
[from] Computing for function test_123_comp_disj_2345_comp
[from] Computing for function f_123_comp_disj_2345_comp <-test_123_comp_disj_2345_comp
[from] Done for function f_123_comp_disj_2345_comp
[from] Done for function test_123_comp_disj_2345_comp
[from] Computing for function test_123_comp_disj_2345_disj
[from] Computing for function f_123_comp_disj_2345_disj <-test_123_comp_disj_2345_disj
[from] Done for function f_123_comp_disj_2345_disj
[from] Done for function test_123_comp_disj_2345_disj
[from] Computing for function test_123_disj_2345_comp_disj
[from] Computing for function f_123_disj_2345_comp_disj <-test_123_disj_2345_comp_disj
[from] Done for function f_123_disj_2345_comp_disj
[from] Done for function test_123_disj_2345_comp_disj
[from] Computing for function test_assigns
[from] Computing for function f <-test_assigns
[from] Done for function f
[from] Done for function test_assigns
[from] Computing for function test_assigns2
[from] Computing for function f2 <-test_assigns2
[from] Done for function f2
[from] Done for function test_assigns2
[from] Computing for function test_comp
[from] Computing for function f_comp <-test_comp
[from] Done for function f_comp
[from] Done for function test_comp
[from] Computing for function test_comp_disj
[from] Computing for function f_comp_disj <-test_comp_disj
[from] Done for function f_comp_disj
[from] Done for function test_comp_disj
[from] Computing for function test_disj
[from] Computing for function f_disj <-test_disj
[from] Done for function f_disj
[from] Done for function test_disj
[from] Computing for function test_narrow
[from] Computing for function f10 <-test_narrow
[from] Done for function f10
[from] Done for function test_narrow
[from] Computing for function test_none
[from] Computing for function f_none <-test_none
[from] Done for function f_none
[from] Done for function test_none
[from] Computing for function test_promote
[from] Computing for function f9 <-test_promote
[from] Done for function f9
[from] Done for function test_promote
[from] Computing for function test_small1
[from] Computing for function f3 <-test_small1
[from] Done for function f3
[from] Done for function test_small1
[from] Computing for function test_small2
[from] Computing for function f4 <-test_small2
[from] Done for function f4
[from] Done for function test_small2
[from] Computing for function test_small3
[from] Computing for function f5 <-test_small3
[from] Done for function f5
[from] Done for function test_small3
[from] Computing for function test_small4
[from] Computing for function f6 <-test_small4
[from] Done for function f6
[from] Done for function test_small4
[from] Computing for function test_small5
[from] Computing for function f7 <-test_small5
[from] Done for function f7
[from] Done for function test_small5
[from] Computing for function test_small6
[from] Computing for function f8 <-test_small6
[from] Done for function f8
[from] Done for function test_small6
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
       These dependencies hold at termination for the executions that terminate:
[from] Function f:
  \result FROM p; q
[from] Function f10:
  \result FROM x
[from] Function f2:
  T[0..4] FROM \nothing
[from] Function f3:
  \result FROM x
[from] Function f4:
  \result FROM x
[from] Function f5:
  \result FROM x
[from] Function f6:
  \result FROM x
[from] Function f7:
  \result FROM x
[from] Function f8:
  a FROM \nothing
  \result FROM p
[from] Function f9:
  \result FROM n; "a"[bits 0 to 7]
[from] Function f_123_comp_2345_comp_disj:
  \result FROM a; b
[from] Function f_123_comp_disj:
  \result FROM a; b
[from] Function f_123_comp_disj_2345_comp:
  \result FROM a; b
[from] Function f_123_comp_disj_2345_disj:
  \result FROM a; b
[from] Function f_123_disj_2345_comp_disj:
  \result FROM a; b
[from] Function f_comp:
  \result FROM a; b
[from] Function f_comp_disj:
  \result FROM a; b
[from] Function f_disj:
  \result FROM a; b
[from] Function f_none:
  \result FROM a; b
[from] Function test_123_comp_2345_comp_disj:
  NO EFFECTS
[from] Function test_123_comp_disj:
  NO EFFECTS
[from] Function test_123_comp_disj_2345_comp:
  NO EFFECTS
[from] Function test_123_comp_disj_2345_disj:
  NO EFFECTS
[from] Function test_123_disj_2345_comp_disj:
  NO EFFECTS
[from] Function test_assigns:
  NO EFFECTS
[from] Function test_assigns2:
  T[0..4] FROM \nothing
[from] Function test_comp:
  NO EFFECTS
[from] Function test_comp_disj:
  NO EFFECTS
[from] Function test_disj:
  NO EFFECTS
[from] Function test_narrow:
  NO EFFECTS
[from] Function test_none:
  NO EFFECTS
[from] Function test_promote:
  NO EFFECTS
[from] Function test_small1:
  NO EFFECTS
[from] Function test_small2:
  NO EFFECTS
[from] Function test_small3:
  NO EFFECTS
[from] Function test_small4:
  NO EFFECTS
[from] Function test_small5:
  NO EFFECTS
[from] Function test_small6:
  NO EFFECTS
[from] Function main:
  T[0..4] FROM \nothing
  \result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function test_123_comp_2345_comp_disj:
          a; b; c1; c2; c3; c4
[inout] Inputs for function test_123_comp_2345_comp_disj:
          nondet
[inout] Out (internal) for function test_123_comp_disj:
          a; b; c1; c2; c3; c4
[inout] Inputs for function test_123_comp_disj:
          nondet
[inout] Out (internal) for function test_123_comp_disj_2345_comp:
          a; b; c1; c2; c3; c4
[inout] Inputs for function test_123_comp_disj_2345_comp:
          nondet
[inout] Out (internal) for function test_123_comp_disj_2345_disj:
          a; b; c1; c2; c3; c4
[inout] Inputs for function test_123_comp_disj_2345_disj:
          nondet
[inout] Out (internal) for function test_123_disj_2345_comp_disj:
          a; b; c1; c2; c3; c4
[inout] Inputs for function test_123_disj_2345_comp_disj:
          nondet
[inout] Out (internal) for function test_assigns:
          p1; p2; p3; tmp; tmp_0; tmp_1
[inout] Inputs for function test_assigns:
          \nothing
[inout] Out (internal) for function test_assigns2:
          T[0..4]; p
[inout] Inputs for function test_assigns2:
          \nothing
[inout] Out (internal) for function test_comp:
          a; b; c1; c2; c3; c4
[inout] Inputs for function test_comp:
          nondet
[inout] Out (internal) for function test_comp_disj:
          a; b; c1; c2; c3; c4
[inout] Inputs for function test_comp_disj:
          nondet
[inout] Out (internal) for function test_disj:
          a; b; c1; c2; c3; c4
[inout] Inputs for function test_disj:
          nondet
[inout] Out (internal) for function test_narrow:
          r
[inout] Inputs for function test_narrow:
          nondet
[inout] Out (internal) for function test_none:
          a; b; c1; c2; c3; c4
[inout] Inputs for function test_none:
          nondet
[inout] Out (internal) for function test_promote:
          x; r
[inout] Inputs for function test_promote:
          nondet; "a"[bits 0 to 7]
[inout] Out (internal) for function test_small1:
          x
[inout] Inputs for function test_small1:
          nondet
[inout] Out (internal) for function test_small2:
          x
[inout] Inputs for function test_small2:
          nondet
[inout] Out (internal) for function test_small3:
          r
[inout] Inputs for function test_small3:
          nondet
[inout] Out (internal) for function test_small4:
          r
[inout] Inputs for function test_small4:
          nondet
[inout] Out (internal) for function test_small5:
          r
[inout] Inputs for function test_small5:
          nondet
[inout] Out (internal) for function test_small6:
          a; p
[inout] Inputs for function test_small6:
          \nothing
[inout] Out (internal) for function main:
          T[0..4]; __retres
[inout] Inputs for function main:
          nondet; "a"[bits 0 to 7]