string_c_strchr.res.oracle

[kernel] Parsing tests/libc/string_c_strchr.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  
[eva] Semantic level unrolling superposing up to 100 states
[eva] Semantic level unrolling superposing up to 200 states
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:62.
[eva] tests/libc/string_c_strchr.c:62: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] share/libc/string.h:168: 
  function strchr, behavior not_found: postcondition 'result_null' got status valid.
[eva] share/libc/string.h:171: 
  function strchr, behavior default: postcondition 'result_null_or_same_base' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:63.
[eva] tests/libc/string_c_strchr.c:63: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:64.
[eva] tests/libc/string_c_strchr.c:64: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:65.
[eva] tests/libc/string_c_strchr.c:65: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:66.
[eva] tests/libc/string_c_strchr.c:66: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:67.
[eva] tests/libc/string_c_strchr.c:67: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:68.
[eva] tests/libc/string_c_strchr.c:68: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:70.
[eva] tests/libc/string_c_strchr.c:70: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] share/libc/string.h:161: 
  function strchr, behavior found: postcondition 'result_char' got status valid.
[eva] share/libc/string.h:162: 
  function strchr, behavior found: postcondition 'result_same_base' got status valid.
[eva] share/libc/string.h:163: 
  function strchr, behavior found: postcondition 'result_in_length' got status valid.
[eva] share/libc/string.h:164: 
  function strchr, behavior found: postcondition 'result_valid_string' got status valid.
[eva:alarm] share/libc/string.h:165: Warning: 
  function strchr, behavior found: postcondition 'result_first_occur' got status unknown.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:71.
[eva] tests/libc/string_c_strchr.c:71: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:72.
[eva] tests/libc/string_c_strchr.c:72: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:73.
[eva] tests/libc/string_c_strchr.c:73: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:74.
[eva] tests/libc/string_c_strchr.c:74: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:75.
[eva] tests/libc/string_c_strchr.c:75: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:76.
[eva] tests/libc/string_c_strchr.c:76: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:77.
[eva] tests/libc/string_c_strchr.c:77: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:78.
[eva] tests/libc/string_c_strchr.c:78: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:79.
[eva] tests/libc/string_c_strchr.c:79: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:80.
[eva] tests/libc/string_c_strchr.c:80: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:81.
[eva] tests/libc/string_c_strchr.c:81: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:82.
[eva] tests/libc/string_c_strchr.c:82: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:83.
[eva] tests/libc/string_c_strchr.c:83: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:84.
[eva] tests/libc/string_c_strchr.c:84: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:85.
[eva] tests/libc/string_c_strchr.c:85: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:86.
[eva] tests/libc/string_c_strchr.c:86: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:87.
[eva] tests/libc/string_c_strchr.c:87: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] computing for function strchr <- main.
  Called from tests/libc/string_c_strchr.c:88.
[eva] tests/libc/string_c_strchr.c:88: 
  function strchr: precondition 'valid_string_s' got status valid.
[eva] Recording results for strchr
[eva] Done for function strchr
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function strchr:
  ch ∈ [--..--]
  i ∈ [0..255]
  __retres ∈
          {{ NULL ; &s{[0], [1], [9], [10], [126], [127], [254], [255]} ;
             "" ; "a" ; "a" ; "a" + {1} ; "abb" + {1} ; "aabb" + {2} ;
             "aaabb" + {3} ; "aaaabb" + {4} ; "aaaaabb" + {5} ;
             "aaaaaabb" + {6} ; "abc abc" + {2} }}
[eva:final-states] Values at end of function main:
  i ∈ {256}
  a[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {3}
   [3] ∈ {4}
   [4] ∈ {5}
   [5] ∈ {6}
   [6] ∈ {7}
   [7] ∈ {8}
   [8] ∈ {9}
   [9] ∈ {10}
   [10] ∈ {11}
   [11] ∈ {12}
   [12] ∈ {13}
   [13] ∈ {14}
   [14] ∈ {15}
   [15] ∈ {16}
   [16] ∈ {17}
   [17] ∈ {18}
   [18] ∈ {19}
   [19] ∈ {20}
   [20] ∈ {21}
   [21] ∈ {22}
   [22] ∈ {23}
   [23] ∈ {24}
   [24] ∈ {25}
   [25] ∈ {26}
   [26] ∈ {27}
   [27] ∈ {28}
   [28] ∈ {29}
   [29] ∈ {30}
   [30] ∈ {31}
   [31] ∈ {32}
   [32] ∈ {33}
   [33] ∈ {34}
   [34] ∈ {35}
   [35] ∈ {36}
   [36] ∈ {37}
   [37] ∈ {38}
   [38] ∈ {39}
   [39] ∈ {40}
   [40] ∈ {41}
   [41] ∈ {42}
   [42] ∈ {43}
   [43] ∈ {44}
   [44] ∈ {45}
   [45] ∈ {46}
   [46] ∈ {47}
   [47] ∈ {48}
   [48] ∈ {49}
   [49] ∈ {50}
   [50] ∈ {51}
   [51] ∈ {52}
   [52] ∈ {53}
   [53] ∈ {54}
   [54] ∈ {55}
   [55] ∈ {56}
   [56] ∈ {57}
   [57] ∈ {58}
   [58] ∈ {59}
   [59] ∈ {60}
   [60] ∈ {61}
   [61] ∈ {62}
   [62] ∈ {63}
   [63] ∈ {64}
   [64] ∈ {65}
   [65] ∈ {66}
   [66] ∈ {67}
   [67] ∈ {68}
   [68] ∈ {69}
   [69] ∈ {70}
   [70] ∈ {71}
   [71] ∈ {72}
   [72] ∈ {73}
   [73] ∈ {74}
   [74] ∈ {75}
   [75] ∈ {76}
   [76] ∈ {77}
   [77] ∈ {78}
   [78] ∈ {79}
   [79] ∈ {80}
   [80] ∈ {81}
   [81] ∈ {82}
   [82] ∈ {83}
   [83] ∈ {84}
   [84] ∈ {85}
   [85] ∈ {86}
   [86] ∈ {87}
   [87] ∈ {88}
   [88] ∈ {89}
   [89] ∈ {90}
   [90] ∈ {91}
   [91] ∈ {92}
   [92] ∈ {93}
   [93] ∈ {94}
   [94] ∈ {95}
   [95] ∈ {96}
   [96] ∈ {97}
   [97] ∈ {98}
   [98] ∈ {99}
   [99] ∈ {100}
   [100] ∈ {101}
   [101] ∈ {102}
   [102] ∈ {103}
   [103] ∈ {104}
   [104] ∈ {105}
   [105] ∈ {106}
   [106] ∈ {107}
   [107] ∈ {108}
   [108] ∈ {109}
   [109] ∈ {110}
   [110] ∈ {111}
   [111] ∈ {112}
   [112] ∈ {113}
   [113] ∈ {114}
   [114] ∈ {115}
   [115] ∈ {116}
   [116] ∈ {117}
   [117] ∈ {118}
   [118] ∈ {119}
   [119] ∈ {120}
   [120] ∈ {121}
   [121] ∈ {122}
   [122] ∈ {123}
   [123] ∈ {124}
   [124] ∈ {125}
   [125] ∈ {126}
   [126] ∈ {127}
   [127] ∈ {0}
  s[0] ∈ {1}
   [1] ∈ {2}
   [2] ∈ {3}
   [3] ∈ {4}
   [4] ∈ {5}
   [5] ∈ {6}
   [6] ∈ {7}
   [7] ∈ {8}
   [8] ∈ {9}
   [9] ∈ {10}
   [10] ∈ {11}
   [11] ∈ {12}
   [12] ∈ {13}
   [13] ∈ {14}
   [14] ∈ {15}
   [15] ∈ {16}
   [16] ∈ {17}
   [17] ∈ {18}
   [18] ∈ {19}
   [19] ∈ {20}
   [20] ∈ {21}
   [21] ∈ {22}
   [22] ∈ {23}
   [23] ∈ {24}
   [24] ∈ {25}
   [25] ∈ {26}
   [26] ∈ {27}
   [27] ∈ {28}
   [28] ∈ {29}
   [29] ∈ {30}
   [30] ∈ {31}
   [31] ∈ {32}
   [32] ∈ {33}
   [33] ∈ {34}
   [34] ∈ {35}
   [35] ∈ {36}
   [36] ∈ {37}
   [37] ∈ {38}
   [38] ∈ {39}
   [39] ∈ {40}
   [40] ∈ {41}
   [41] ∈ {42}
   [42] ∈ {43}
   [43] ∈ {44}
   [44] ∈ {45}
   [45] ∈ {46}
   [46] ∈ {47}
   [47] ∈ {48}
   [48] ∈ {49}
   [49] ∈ {50}
   [50] ∈ {51}
   [51] ∈ {52}
   [52] ∈ {53}
   [53] ∈ {54}
   [54] ∈ {55}
   [55] ∈ {56}
   [56] ∈ {57}
   [57] ∈ {58}
   [58] ∈ {59}
   [59] ∈ {60}
   [60] ∈ {61}
   [61] ∈ {62}
   [62] ∈ {63}
   [63] ∈ {64}
   [64] ∈ {65}
   [65] ∈ {66}
   [66] ∈ {67}
   [67] ∈ {68}
   [68] ∈ {69}
   [69] ∈ {70}
   [70] ∈ {71}
   [71] ∈ {72}
   [72] ∈ {73}
   [73] ∈ {74}
   [74] ∈ {75}
   [75] ∈ {76}
   [76] ∈ {77}
   [77] ∈ {78}
   [78] ∈ {79}
   [79] ∈ {80}
   [80] ∈ {81}
   [81] ∈ {82}
   [82] ∈ {83}
   [83] ∈ {84}
   [84] ∈ {85}
   [85] ∈ {86}
   [86] ∈ {87}
   [87] ∈ {88}
   [88] ∈ {89}
   [89] ∈ {90}
   [90] ∈ {91}
   [91] ∈ {92}
   [92] ∈ {93}
   [93] ∈ {94}
   [94] ∈ {95}
   [95] ∈ {96}
   [96] ∈ {97}
   [97] ∈ {98}
   [98] ∈ {99}
   [99] ∈ {100}
   [100] ∈ {101}
   [101] ∈ {102}
   [102] ∈ {103}
   [103] ∈ {104}
   [104] ∈ {105}
   [105] ∈ {106}
   [106] ∈ {107}
   [107] ∈ {108}
   [108] ∈ {109}
   [109] ∈ {110}
   [110] ∈ {111}
   [111] ∈ {112}
   [112] ∈ {113}
   [113] ∈ {114}
   [114] ∈ {115}
   [115] ∈ {116}
   [116] ∈ {117}
   [117] ∈ {118}
   [118] ∈ {119}
   [119] ∈ {120}
   [120] ∈ {121}
   [121] ∈ {122}
   [122] ∈ {123}
   [123] ∈ {124}
   [124] ∈ {125}
   [125] ∈ {126}
   [126] ∈ {127}
   [127] ∈ {128}
   [128] ∈ {129}
   [129] ∈ {130}
   [130] ∈ {131}
   [131] ∈ {132}
   [132] ∈ {133}
   [133] ∈ {134}
   [134] ∈ {135}
   [135] ∈ {136}
   [136] ∈ {137}
   [137] ∈ {138}
   [138] ∈ {139}
   [139] ∈ {140}
   [140] ∈ {141}
   [141] ∈ {142}
   [142] ∈ {143}
   [143] ∈ {144}
   [144] ∈ {145}
   [145] ∈ {146}
   [146] ∈ {147}
   [147] ∈ {148}
   [148] ∈ {149}
   [149] ∈ {150}
   [150] ∈ {151}
   [151] ∈ {152}
   [152] ∈ {153}
   [153] ∈ {154}
   [154] ∈ {155}
   [155] ∈ {156}
   [156] ∈ {157}
   [157] ∈ {158}
   [158] ∈ {159}
   [159] ∈ {160}
   [160] ∈ {161}
   [161] ∈ {162}
   [162] ∈ {163}
   [163] ∈ {164}
   [164] ∈ {165}
   [165] ∈ {166}
   [166] ∈ {167}
   [167] ∈ {168}
   [168] ∈ {169}
   [169] ∈ {170}
   [170] ∈ {171}
   [171] ∈ {172}
   [172] ∈ {173}
   [173] ∈ {174}
   [174] ∈ {175}
   [175] ∈ {176}
   [176] ∈ {177}
   [177] ∈ {178}
   [178] ∈ {179}
   [179] ∈ {180}
   [180] ∈ {181}
   [181] ∈ {182}
   [182] ∈ {183}
   [183] ∈ {184}
   [184] ∈ {185}
   [185] ∈ {186}
   [186] ∈ {187}
   [187] ∈ {188}
   [188] ∈ {189}
   [189] ∈ {190}
   [190] ∈ {191}
   [191] ∈ {192}
   [192] ∈ {193}
   [193] ∈ {194}
   [194] ∈ {195}
   [195] ∈ {196}
   [196] ∈ {197}
   [197] ∈ {198}
   [198] ∈ {199}
   [199] ∈ {200}
   [200] ∈ {201}
   [201] ∈ {202}
   [202] ∈ {203}
   [203] ∈ {204}
   [204] ∈ {205}
   [205] ∈ {206}
   [206] ∈ {207}
   [207] ∈ {208}
   [208] ∈ {209}
   [209] ∈ {210}
   [210] ∈ {211}
   [211] ∈ {212}
   [212] ∈ {213}
   [213] ∈ {214}
   [214] ∈ {215}
   [215] ∈ {216}
   [216] ∈ {217}
   [217] ∈ {218}
   [218] ∈ {219}
   [219] ∈ {220}
   [220] ∈ {221}
   [221] ∈ {222}
   [222] ∈ {223}
   [223] ∈ {224}
   [224] ∈ {225}
   [225] ∈ {226}
   [226] ∈ {227}
   [227] ∈ {228}
   [228] ∈ {229}
   [229] ∈ {230}
   [230] ∈ {231}
   [231] ∈ {232}
   [232] ∈ {233}
   [233] ∈ {234}
   [234] ∈ {235}
   [235] ∈ {236}
   [236] ∈ {237}
   [237] ∈ {238}
   [238] ∈ {239}
   [239] ∈ {240}
   [240] ∈ {241}
   [241] ∈ {242}
   [242] ∈ {243}
   [243] ∈ {244}
   [244] ∈ {245}
   [245] ∈ {246}
   [246] ∈ {247}
   [247] ∈ {248}
   [248] ∈ {249}
   [249] ∈ {250}
   [250] ∈ {251}
   [251] ∈ {252}
   [252] ∈ {253}
   [253] ∈ {254}
   [254] ∈ {255}
   [255] ∈ {0}
  __retres ∈ {0}