[kernel] Parsing tests/builtins/alloc_weak.c (with preprocessing)
[kernel:typing:int-conversion] tests/builtins/alloc_weak.c:37: Warning: 
  Conversion from a pointer to an integer without an explicit cast
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  v ∈ [--..--]
[eva] computing for function main1 <- main.
  Called from tests/builtins/alloc_weak.c:72.
[eva] tests/builtins/alloc_weak.c:23: Call to builtin malloc
[eva] tests/builtins/alloc_weak.c:23: allocating variable __malloc_main1_l23
[eva] tests/builtins/alloc_weak.c:23: Call to builtin malloc
[eva:malloc:weak] tests/builtins/alloc_weak.c:23: 
  marking variable `__malloc_main1_l23' as weak
[eva] computing for function copy <- main1 <- main.
  Called from tests/builtins/alloc_weak.c:27.
[eva] tests/builtins/alloc_weak.c:14: Call to builtin memcpy
[eva] tests/builtins/alloc_weak.c:14: 
  function memcpy: precondition 'valid_dest' got status valid.
[eva] tests/builtins/alloc_weak.c:14: 
  function memcpy: precondition 'valid_src' got status valid.
[eva] tests/builtins/alloc_weak.c:14: 
  function memcpy: precondition 'separation' got status valid.
[eva] share/libc/string.h:98: 
  cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
[eva] Recording results for copy
[eva] Done for function copy
[eva] computing for function copy <- main1 <- main.
  Called from tests/builtins/alloc_weak.c:28.
[eva] tests/builtins/alloc_weak.c:14: Call to builtin memcpy
[eva] Recording results for copy
[eva] Done for function copy
[eva:alarm] tests/builtins/alloc_weak.c:29: Warning: 
  out of bounds write. assert \valid(p);
[eva:alarm] tests/builtins/alloc_weak.c:30: Warning: 
  accessing uninitialized left-value. assert \initialized(p);
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
  Called from tests/builtins/alloc_weak.c:73.
[eva] tests/builtins/alloc_weak.c:37: Call to builtin malloc
[eva] tests/builtins/alloc_weak.c:37: allocating variable __malloc_main2_l37
[eva] Semantic level unrolling superposing up to 100 states
[eva] Semantic level unrolling superposing up to 200 states
[eva] Semantic level unrolling superposing up to 300 states
[eva] Semantic level unrolling superposing up to 400 states
[eva] Semantic level unrolling superposing up to 500 states
[eva] Semantic level unrolling superposing up to 600 states
[eva] Semantic level unrolling superposing up to 700 states
[eva] Semantic level unrolling superposing up to 800 states
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
  Called from tests/builtins/alloc_weak.c:74.
[eva] tests/builtins/alloc_weak.c:51: Call to builtin malloc
[eva] tests/builtins/alloc_weak.c:51: allocating variable __malloc_main3_l51
[eva] tests/builtins/alloc_weak.c:50: starting to merge loop iterations
[eva] tests/builtins/alloc_weak.c:51: Call to builtin malloc
[eva:malloc:weak] tests/builtins/alloc_weak.c:51: 
  marking variable `__malloc_main3_l51' as weak
[eva] tests/builtins/alloc_weak.c:51: Call to builtin malloc
[eva] tests/builtins/alloc_weak.c:51: Call to builtin malloc
[eva:alarm] tests/builtins/alloc_weak.c:62: Warning: 
  accessing uninitialized left-value. assert \initialized(&q);
[eva:alarm] tests/builtins/alloc_weak.c:62: Warning: 
  accessing uninitialized left-value. assert \initialized(&r);
[eva:alarm] tests/builtins/alloc_weak.c:62: Warning: 
  pointer subtraction. assert \base_addr(q) ≡ \base_addr(r);
[eva:alarm] tests/builtins/alloc_weak.c:63: Warning: 
  pointer comparison. assert \pointer_comparable((void *)q, (void *)r);
[eva] Recording results for main3
[eva] Done for function main3
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main2:
  __fc_heap_status ∈ [--..--]
  t[0] ∈ {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}
   [256] ∈ {256}
   [257] ∈ {257}
   [258] ∈ {258}
   [259] ∈ {259}
   [260] ∈ {260}
   [261] ∈ {261}
   [262] ∈ {262}
   [263] ∈ {263}
   [264] ∈ {264}
   [265] ∈ {265}
   [266] ∈ {266}
   [267] ∈ {267}
   [268] ∈ {268}
   [269] ∈ {269}
   [270] ∈ {270}
   [271] ∈ {271}
   [272] ∈ {272}
   [273] ∈ {273}
   [274] ∈ {274}
   [275] ∈ {275}
   [276] ∈ {276}
   [277] ∈ {277}
   [278] ∈ {278}
   [279] ∈ {279}
   [280] ∈ {280}
   [281] ∈ {281}
   [282] ∈ {282}
   [283] ∈ {283}
   [284] ∈ {284}
   [285] ∈ {285}
   [286] ∈ {286}
   [287] ∈ {287}
   [288] ∈ {288}
   [289] ∈ {289}
   [290] ∈ {290}
   [291] ∈ {291}
   [292] ∈ {292}
   [293] ∈ {293}
   [294] ∈ {294}
   [295] ∈ {295}
   [296] ∈ {296}
   [297] ∈ {297}
   [298] ∈ {298}
   [299] ∈ {299}
   [300] ∈ {300}
   [301] ∈ {301}
   [302] ∈ {302}
   [303] ∈ {303}
   [304] ∈ {304}
   [305] ∈ {305}
   [306] ∈ {306}
   [307] ∈ {307}
   [308] ∈ {308}
   [309] ∈ {309}
   [310] ∈ {310}
   [311] ∈ {311}
   [312] ∈ {312}
   [313] ∈ {313}
   [314] ∈ {314}
   [315] ∈ {315}
   [316] ∈ {316}
   [317] ∈ {317}
   [318] ∈ {318}
   [319] ∈ {319}
   [320] ∈ {320}
   [321] ∈ {321}
   [322] ∈ {322}
   [323] ∈ {323}
   [324] ∈ {324}
   [325] ∈ {325}
   [326] ∈ {326}
   [327] ∈ {327}
   [328] ∈ {328}
   [329] ∈ {329}
   [330] ∈ {330}
   [331] ∈ {331}
   [332] ∈ {332}
   [333] ∈ {333}
   [334] ∈ {334}
   [335] ∈ {335}
   [336] ∈ {336}
   [337] ∈ {337}
   [338] ∈ {338}
   [339] ∈ {339}
   [340] ∈ {340}
   [341] ∈ {341}
   [342] ∈ {342}
   [343] ∈ {343}
   [344] ∈ {344}
   [345] ∈ {345}
   [346] ∈ {346}
   [347] ∈ {347}
   [348] ∈ {348}
   [349] ∈ {349}
   [350] ∈ {350}
   [351] ∈ {351}
   [352] ∈ {352}
   [353] ∈ {353}
   [354] ∈ {354}
   [355] ∈ {355}
   [356] ∈ {356}
   [357] ∈ {357}
   [358] ∈ {358}
   [359] ∈ {359}
   [360] ∈ {360}
   [361] ∈ {361}
   [362] ∈ {362}
   [363] ∈ {363}
   [364] ∈ {364}
   [365] ∈ {365}
   [366] ∈ {366}
   [367] ∈ {367}
   [368] ∈ {368}
   [369] ∈ {369}
   [370] ∈ {370}
   [371] ∈ {371}
   [372] ∈ {372}
   [373] ∈ {373}
   [374] ∈ {374}
   [375] ∈ {375}
   [376] ∈ {376}
   [377] ∈ {377}
   [378] ∈ {378}
   [379] ∈ {379}
   [380] ∈ {380}
   [381] ∈ {381}
   [382] ∈ {382}
   [383] ∈ {383}
   [384] ∈ {384}
   [385] ∈ {385}
   [386] ∈ {386}
   [387] ∈ {387}
   [388] ∈ {388}
   [389] ∈ {389}
   [390] ∈ {390}
   [391] ∈ {391}
   [392] ∈ {392}
   [393] ∈ {393}
   [394] ∈ {394}
   [395] ∈ {395}
   [396] ∈ {396}
   [397] ∈ {397}
   [398] ∈ {398}
   [399] ∈ {399}
   [400] ∈ {400}
   [401] ∈ {401}
   [402] ∈ {402}
   [403] ∈ {403}
   [404] ∈ {404}
   [405] ∈ {405}
   [406] ∈ {406}
   [407] ∈ {407}
   [408] ∈ {408}
   [409] ∈ {409}
   [410] ∈ {410}
   [411] ∈ {411}
   [412] ∈ {412}
   [413] ∈ {413}
   [414] ∈ {414}
   [415] ∈ {415}
   [416] ∈ {416}
   [417] ∈ {417}
   [418] ∈ {418}
   [419] ∈ {419}
   [420] ∈ {420}
   [421] ∈ {421}
   [422] ∈ {422}
   [423] ∈ {423}
   [424] ∈ {424}
   [425] ∈ {425}
   [426] ∈ {426}
   [427] ∈ {427}
   [428] ∈ {428}
   [429] ∈ {429}
   [430] ∈ {430}
   [431] ∈ {431}
   [432] ∈ {432}
   [433] ∈ {433}
   [434] ∈ {434}
   [435] ∈ {435}
   [436] ∈ {436}
   [437] ∈ {437}
   [438] ∈ {438}
   [439] ∈ {439}
   [440] ∈ {440}
   [441] ∈ {441}
   [442] ∈ {442}
   [443] ∈ {443}
   [444] ∈ {444}
   [445] ∈ {445}
   [446] ∈ {446}
   [447] ∈ {447}
   [448] ∈ {448}
   [449] ∈ {449}
   [450] ∈ {450}
   [451] ∈ {451}
   [452] ∈ {452}
   [453] ∈ {453}
   [454] ∈ {454}
   [455] ∈ {455}
   [456] ∈ {456}
   [457] ∈ {457}
   [458] ∈ {458}
   [459] ∈ {459}
   [460] ∈ {460}
   [461] ∈ {461}
   [462] ∈ {462}
   [463] ∈ {463}
   [464] ∈ {464}
   [465] ∈ {465}
   [466] ∈ {466}
   [467] ∈ {467}
   [468] ∈ {468}
   [469] ∈ {469}
   [470] ∈ {470}
   [471] ∈ {471}
   [472] ∈ {472}
   [473] ∈ {473}
   [474] ∈ {474}
   [475] ∈ {475}
   [476] ∈ {476}
   [477] ∈ {477}
   [478] ∈ {478}
   [479] ∈ {479}
   [480] ∈ {480}
   [481] ∈ {481}
   [482] ∈ {482}
   [483] ∈ {483}
   [484] ∈ {484}
   [485] ∈ {485}
   [486] ∈ {486}
   [487] ∈ {487}
   [488] ∈ {488}
   [489] ∈ {489}
   [490] ∈ {490}
   [491] ∈ {491}
   [492] ∈ {492}
   [493] ∈ {493}
   [494] ∈ {494}
   [495] ∈ {495}
   [496] ∈ {496}
   [497] ∈ {497}
   [498] ∈ {498}
   [499] ∈ {499}
   [500] ∈ {500}
   [501] ∈ {501}
   [502] ∈ {502}
   [503] ∈ {503}
   [504] ∈ {504}
   [505] ∈ {505}
   [506] ∈ {506}
   [507] ∈ {507}
   [508] ∈ {508}
   [509] ∈ {509}
   [510] ∈ {510}
   [511] ∈ {511}
   [512] ∈ {512}
   [513] ∈ {513}
   [514] ∈ {514}
   [515] ∈ {515}
   [516] ∈ {516}
   [517] ∈ {517}
   [518] ∈ {518}
   [519] ∈ {519}
   [520] ∈ {520}
   [521] ∈ {521}
   [522] ∈ {522}
   [523] ∈ {523}
   [524] ∈ {524}
   [525] ∈ {525}
   [526] ∈ {526}
   [527] ∈ {527}
   [528] ∈ {528}
   [529] ∈ {529}
   [530] ∈ {530}
   [531] ∈ {531}
   [532] ∈ {532}
   [533] ∈ {533}
   [534] ∈ {534}
   [535] ∈ {535}
   [536] ∈ {536}
   [537] ∈ {537}
   [538] ∈ {538}
   [539] ∈ {539}
   [540] ∈ {540}
   [541] ∈ {541}
   [542] ∈ {542}
   [543] ∈ {543}
   [544] ∈ {544}
   [545] ∈ {545}
   [546] ∈ {546}
   [547] ∈ {547}
   [548] ∈ {548}
   [549] ∈ {549}
   [550] ∈ {550}
   [551] ∈ {551}
   [552] ∈ {552}
   [553] ∈ {553}
   [554] ∈ {554}
   [555] ∈ {555}
   [556] ∈ {556}
   [557] ∈ {557}
   [558] ∈ {558}
   [559] ∈ {559}
   [560] ∈ {560}
   [561] ∈ {561}
   [562] ∈ {562}
   [563] ∈ {563}
   [564] ∈ {564}
   [565] ∈ {565}
   [566] ∈ {566}
   [567] ∈ {567}
   [568] ∈ {568}
   [569] ∈ {569}
   [570] ∈ {570}
   [571] ∈ {571}
   [572] ∈ {572}
   [573] ∈ {573}
   [574] ∈ {574}
   [575] ∈ {575}
   [576] ∈ {576}
   [577] ∈ {577}
   [578] ∈ {578}
   [579] ∈ {579}
   [580] ∈ {580}
   [581] ∈ {581}
   [582] ∈ {582}
   [583] ∈ {583}
   [584] ∈ {584}
   [585] ∈ {585}
   [586] ∈ {586}
   [587] ∈ {587}
   [588] ∈ {588}
   [589] ∈ {589}
   [590] ∈ {590}
   [591] ∈ {591}
   [592] ∈ {592}
   [593] ∈ {593}
   [594] ∈ {594}
   [595] ∈ {595}
   [596] ∈ {596}
   [597] ∈ {597}
   [598] ∈ {598}
   [599] ∈ {599}
   [600] ∈ {600}
   [601] ∈ {601}
   [602] ∈ {602}
   [603] ∈ {603}
   [604] ∈ {604}
   [605] ∈ {605}
   [606] ∈ {606}
   [607] ∈ {607}
   [608] ∈ {608}
   [609] ∈ {609}
   [610] ∈ {610}
   [611] ∈ {611}
   [612] ∈ {612}
   [613] ∈ {613}
   [614] ∈ {614}
   [615] ∈ {615}
   [616] ∈ {616}
   [617] ∈ {617}
   [618] ∈ {618}
   [619] ∈ {619}
   [620] ∈ {620}
   [621] ∈ {621}
   [622] ∈ {622}
   [623] ∈ {623}
   [624] ∈ {624}
   [625] ∈ {625}
   [626] ∈ {626}
   [627] ∈ {627}
   [628] ∈ {628}
   [629] ∈ {629}
   [630] ∈ {630}
   [631] ∈ {631}
   [632] ∈ {632}
   [633] ∈ {633}
   [634] ∈ {634}
   [635] ∈ {635}
   [636] ∈ {636}
   [637] ∈ {637}
   [638] ∈ {638}
   [639] ∈ {639}
   [640] ∈ {640}
   [641] ∈ {641}
   [642] ∈ {642}
   [643] ∈ {643}
   [644] ∈ {644}
   [645] ∈ {645}
   [646] ∈ {646}
   [647] ∈ {647}
   [648] ∈ {648}
   [649] ∈ {649}
   [650] ∈ {650}
   [651] ∈ {651}
   [652] ∈ {652}
   [653] ∈ {653}
   [654] ∈ {654}
   [655] ∈ {655}
   [656] ∈ {656}
   [657] ∈ {657}
   [658] ∈ {658}
   [659] ∈ {659}
   [660] ∈ {660}
   [661] ∈ {661}
   [662] ∈ {662}
   [663] ∈ {663}
   [664] ∈ {664}
   [665] ∈ {665}
   [666] ∈ {666}
   [667] ∈ {667}
   [668] ∈ {668}
   [669] ∈ {669}
   [670] ∈ {670}
   [671] ∈ {671}
   [672] ∈ {672}
   [673] ∈ {673}
   [674] ∈ {674}
   [675] ∈ {675}
   [676] ∈ {676}
   [677] ∈ {677}
   [678] ∈ {678}
   [679] ∈ {679}
   [680] ∈ {680}
   [681] ∈ {681}
   [682] ∈ {682}
   [683] ∈ {683}
   [684] ∈ {684}
   [685] ∈ {685}
   [686] ∈ {686}
   [687] ∈ {687}
   [688] ∈ {688}
   [689] ∈ {689}
   [690] ∈ {690}
   [691] ∈ {691}
   [692] ∈ {692}
   [693] ∈ {693}
   [694] ∈ {694}
   [695] ∈ {695}
   [696] ∈ {696}
   [697] ∈ {697}
   [698] ∈ {698}
   [699] ∈ {699}
   [700] ∈ {700}
   [701] ∈ {701}
   [702] ∈ {702}
   [703] ∈ {703}
   [704] ∈ {704}
   [705] ∈ {705}
   [706] ∈ {706}
   [707] ∈ {707}
   [708] ∈ {708}
   [709] ∈ {709}
   [710] ∈ {710}
   [711] ∈ {711}
   [712] ∈ {712}
   [713] ∈ {713}
   [714] ∈ {714}
   [715] ∈ {715}
   [716] ∈ {716}
   [717] ∈ {717}
   [718] ∈ {718}
   [719] ∈ {719}
   [720] ∈ {720}
   [721] ∈ {721}
   [722] ∈ {722}
   [723] ∈ {723}
   [724] ∈ {724}
   [725] ∈ {725}
   [726] ∈ {726}
   [727] ∈ {727}
   [728] ∈ {728}
   [729] ∈ {729}
   [730] ∈ {730}
   [731] ∈ {731}
   [732] ∈ {732}
   [733] ∈ {733}
   [734] ∈ {734}
   [735] ∈ {735}
   [736] ∈ {736}
   [737] ∈ {737}
   [738] ∈ {738}
   [739] ∈ {739}
   [740] ∈ {740}
   [741] ∈ {741}
   [742] ∈ {742}
   [743] ∈ {743}
   [744] ∈ {744}
   [745] ∈ {745}
   [746] ∈ {746}
   [747] ∈ {747}
   [748] ∈ {748}
   [749] ∈ {749}
   [750] ∈ {750}
   [751] ∈ {751}
   [752] ∈ {752}
   [753] ∈ {753}
   [754] ∈ {754}
   [755] ∈ {755}
   [756] ∈ {756}
   [757] ∈ {757}
   [758] ∈ {758}
   [759] ∈ {759}
   [760] ∈ {760}
   [761] ∈ {761}
   [762] ∈ {762}
   [763] ∈ {763}
   [764] ∈ {764}
   [765] ∈ {765}
   [766] ∈ {766}
   [767] ∈ {767}
   [768] ∈ {768}
   [769] ∈ {769}
   [770] ∈ {770}
   [771] ∈ {771}
   [772] ∈ {772}
   [773] ∈ {773}
   [774] ∈ {774}
   [775] ∈ {775}
   [776] ∈ {776}
   [777] ∈ {777}
   [778] ∈ {778}
   [779] ∈ {779}
   [780] ∈ {780}
   [781] ∈ {781}
   [782] ∈ {782}
   [783] ∈ {783}
   [784] ∈ {784}
   [785] ∈ {785}
   [786] ∈ {786}
   [787] ∈ {787}
   [788] ∈ {788}
   [789] ∈ {789}
   [790] ∈ {790}
   [791] ∈ {791}
   [792] ∈ {792}
   [793] ∈ {793}
   [794] ∈ {794}
   [795] ∈ {795}
   [796] ∈ {796}
   [797] ∈ {797}
   [798] ∈ {798}
   [799] ∈ {799}
   [800..999] ∈ UNINITIALIZED
  i ∈ {800}
[eva:final-states] Values at end of function main3:
  __fc_heap_status ∈ [--..--]
  p ∈ {{ &__malloc_w_main3_l51 }} or UNINITIALIZED
  q ∈ {{ &__malloc_w_main3_l51 }}
  r ∈ {{ &__malloc_w_main3_l51 }}
  d ∈ {0}
  cmp ∈ {0; 1}
  eq ∈ {0; 1}
[eva:final-states] Values at end of function copy:
  dst ∈ {{ (char *)&p }}
  src ∈ {{ (char *)&t{[0], [1]} }}
  p[bits 0 to 7]# ∈ {{ (? *)&__malloc_w_main1_l23 }}%32, bits 0 to 7 
   [bits 8 to 31]# ∈
   {{ (? *)&__malloc_w_main1_l23 }} or UNINITIALIZED%32, bits 8 to 31 
[eva:final-states] Values at end of function main1:
  __fc_heap_status ∈ [--..--]
  t[0..1] ∈ {{ &__malloc_w_main1_l23[0] }}
  p ∈ {{ &__malloc_w_main1_l23 + [0..124] }}
  n ∈ {4}
  r ∈ [--..--]
  __malloc_w_main1_l23[0..31] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function main:
  __fc_heap_status ∈ [--..--]
  __malloc_w_main1_l23[0..31] ∈ [--..--] or UNINITIALIZED
[from] Computing for function main2
[from] Computing for function malloc <-main2
[from] Done for function malloc
[from] Done for function main2
[from] Computing for function main3
[from] Done for function main3
[from] Computing for function copy
[from] Computing for function memcpy <-copy
[from] Done for function memcpy
[from] Done for function copy
[from] Computing for function main1
[from] Done for function main1
[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 malloc:
  __fc_heap_status FROM __fc_heap_status; size (and SELF)
  \result FROM __fc_heap_status; size
[from] Function main2:
  __fc_heap_status FROM __fc_heap_status (and SELF)
[from] Function main3:
  __fc_heap_status FROM __fc_heap_status (and SELF)
[from] Function memcpy:
  p FROM t{[0][bits 8 to 31]; [1][bits 0 to 23]} (and SELF)
  \result FROM dest
[from] Function copy:
  p FROM t{[0][bits 8 to 31]; [1][bits 0 to 23]} (and SELF)
[from] Function main1:
  __fc_heap_status FROM __fc_heap_status (and SELF)
  __malloc_w_main1_l23[0..31] FROM __fc_heap_status (and SELF)
  \result FROM __fc_heap_status; __malloc_w_main1_l23[0..31]
[from] Function main:
  __fc_heap_status FROM __fc_heap_status (and SELF)
  __malloc_w_main1_l23[0..31] FROM __fc_heap_status (and SELF)
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main2:
    __fc_heap_status; t[0..799]; i; tmp
[inout] Inputs for function main2:
    __fc_heap_status
[inout] Out (internal) for function main3:
    __fc_heap_status; p; q; r; i; d; cmp; eq
[inout] Inputs for function main3:
    __fc_heap_status
[inout] Out (internal) for function copy:
    dst; src; p
[inout] Inputs for function copy:
    t[0..1]
[inout] Out (internal) for function main1:
    __fc_heap_status; t[0..1]; i; p; n; r; __malloc_w_main1_l23[0..31]
[inout] Inputs for function main1:
    __fc_heap_status; __malloc_w_main1_l23[0..31]
[inout] Out (internal) for function main:
    __fc_heap_status; __malloc_w_main1_l23[0..31]
[inout] Inputs for function main:
    __fc_heap_status; __malloc_w_main1_l23[0..31]