diff --git a/tests/builtins/oracle/linked_list.0.res.oracle b/tests/builtins/oracle/linked_list.0.res.oracle
index 7edb0dc61aa38f4ca9fa5dd58d0b5404bc3a30ec..e93e16fb0462e8714990747c055dcaae844688bf 100644
--- a/tests/builtins/oracle/linked_list.0.res.oracle
+++ b/tests/builtins/oracle/linked_list.0.res.oracle
@@ -468,7 +468,7 @@
curr ∈ {{ &MEMORY + [0..1016],0%8 }} or UNINITIALIZED
head ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
i ∈ [1..10]
- malloc_next_free ∈ [0..2147483640],0%8
+ malloc_next_free ∈ [0..1016],0%8
S_0___fc_env[0..1] ∈ [--..--]
S_1___fc_env[0..1] ∈ [--..--]
==END OF DUMP==
@@ -515,10 +515,10 @@
__fc_initial_stderr.__fc_FILE_id ∈ {2}
.__fc_FILE_data ∈ {0}
__fc_initial_stdin ∈ {0}
- curr ∈ {{ NULL ; &MEMORY + [0..4294967288],0%8 }}
+ curr ∈ {{ NULL ; &MEMORY + [0..1008],0%8 }}
head ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
i ∈ [1..10]
- malloc_next_free ∈ [-2147483648..2147483640],0%8
+ malloc_next_free ∈ [8..1024],0%8
S_0___fc_env[0..1] ∈ [--..--]
S_1___fc_env[0..1] ∈ [--..--]
==END OF DUMP==
@@ -781,6 +781,1174 @@
[bits 8032 to 8063] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
[bits 8064 to 8095] ∈ [0..10]
[bits 8096 to 8127] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [1016..1023] ∈ {0}
+ __fc_errno ∈ [--..--]
+ __fc_stderr ∈ {{ &__fc_initial_stderr }}
+ __fc_stdin ∈ {{ &__fc_initial_stdin }}
+ __fc_stdout ∈ {{ &__fc_initial_stdout }}
+ __fc_fopen[0..15] ∈ {0}
+ __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
+ __fc_heap_status ∈ [--..--]
+ __fc_random_counter ∈ [--..--]
+ __fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
+ __fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
+ [1] ∈ {{ NULL ; &S_1___fc_env[0] }}
+ [2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
+ __fc_mblen_state ∈ [--..--]
+ __fc_mbtowc_state ∈ [--..--]
+ __fc_wctomb_state ∈ [--..--]
+ __fc_initial_stdout.__fc_FILE_id ∈ {1}
+ .__fc_FILE_data ∈ {0}
+ __fc_initial_stderr.__fc_FILE_id ∈ {2}
+ .__fc_FILE_data ∈ {0}
+ __fc_initial_stdin ∈ {0}
+ curr ∈ {{ &MEMORY + [0..1016],0%8 }} or UNINITIALIZED
+ head ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ i ∈ [1..10]
+ malloc_next_free ∈ [0..1024],0%8
+ S_0___fc_env[0..1] ∈ [--..--]
+ S_1___fc_env[0..1] ∈ [--..--]
+ ==END OF DUMP==
+[eva] computing for function malloc <- main.
+ Called from tests/builtins/linked_list.c:41.
+[eva] Recording results for malloc
+[eva] Done for function malloc
+[eva] tests/builtins/linked_list.c:42:
+ Frama_C_dump_each:
+ # Cvalue domain:
+ MEMORY[bits 0 to 31] ∈ [0..10]
+ [bits 32 to 63] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 64 to 95] ∈ [0..10]
+ [bits 96 to 127] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 128 to 159] ∈ [0..10]
+ [bits 160 to 191] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 192 to 223] ∈ [0..10]
+ [bits 224 to 255] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 256 to 287] ∈ [0..10]
+ [bits 288 to 319] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 320 to 351] ∈ [0..10]
+ [bits 352 to 383] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 384 to 415] ∈ [0..10]
+ [bits 416 to 447] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 448 to 479] ∈ [0..10]
+ [bits 480 to 511] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 512 to 543] ∈ [0..10]
+ [bits 544 to 575] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 576 to 607] ∈ [0..10]
+ [bits 608 to 639] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 640 to 671] ∈ [0..10]
+ [bits 672 to 703] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 704 to 735] ∈ [0..10]
+ [bits 736 to 767] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 768 to 799] ∈ [0..10]
+ [bits 800 to 831] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 832 to 863] ∈ [0..10]
+ [bits 864 to 895] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 896 to 927] ∈ [0..10]
+ [bits 928 to 959] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 960 to 991] ∈ [0..10]
+ [bits 992 to 1023] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1024 to 1055] ∈ [0..10]
+ [bits 1056 to 1087] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1088 to 1119] ∈ [0..10]
+ [bits 1120 to 1151] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1152 to 1183] ∈ [0..10]
+ [bits 1184 to 1215] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1216 to 1247] ∈ [0..10]
+ [bits 1248 to 1279] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1280 to 1311] ∈ [0..10]
+ [bits 1312 to 1343] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1344 to 1375] ∈ [0..10]
+ [bits 1376 to 1407] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1408 to 1439] ∈ [0..10]
+ [bits 1440 to 1471] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1472 to 1503] ∈ [0..10]
+ [bits 1504 to 1535] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1536 to 1567] ∈ [0..10]
+ [bits 1568 to 1599] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1600 to 1631] ∈ [0..10]
+ [bits 1632 to 1663] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1664 to 1695] ∈ [0..10]
+ [bits 1696 to 1727] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1728 to 1759] ∈ [0..10]
+ [bits 1760 to 1791] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1792 to 1823] ∈ [0..10]
+ [bits 1824 to 1855] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1856 to 1887] ∈ [0..10]
+ [bits 1888 to 1919] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1920 to 1951] ∈ [0..10]
+ [bits 1952 to 1983] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1984 to 2015] ∈ [0..10]
+ [bits 2016 to 2047] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2048 to 2079] ∈ [0..10]
+ [bits 2080 to 2111] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2112 to 2143] ∈ [0..10]
+ [bits 2144 to 2175] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2176 to 2207] ∈ [0..10]
+ [bits 2208 to 2239] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2240 to 2271] ∈ [0..10]
+ [bits 2272 to 2303] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2304 to 2335] ∈ [0..10]
+ [bits 2336 to 2367] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2368 to 2399] ∈ [0..10]
+ [bits 2400 to 2431] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2432 to 2463] ∈ [0..10]
+ [bits 2464 to 2495] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2496 to 2527] ∈ [0..10]
+ [bits 2528 to 2559] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2560 to 2591] ∈ [0..10]
+ [bits 2592 to 2623] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2624 to 2655] ∈ [0..10]
+ [bits 2656 to 2687] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2688 to 2719] ∈ [0..10]
+ [bits 2720 to 2751] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2752 to 2783] ∈ [0..10]
+ [bits 2784 to 2815] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2816 to 2847] ∈ [0..10]
+ [bits 2848 to 2879] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2880 to 2911] ∈ [0..10]
+ [bits 2912 to 2943] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2944 to 2975] ∈ [0..10]
+ [bits 2976 to 3007] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3008 to 3039] ∈ [0..10]
+ [bits 3040 to 3071] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3072 to 3103] ∈ [0..10]
+ [bits 3104 to 3135] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3136 to 3167] ∈ [0..10]
+ [bits 3168 to 3199] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3200 to 3231] ∈ [0..10]
+ [bits 3232 to 3263] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3264 to 3295] ∈ [0..10]
+ [bits 3296 to 3327] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3328 to 3359] ∈ [0..10]
+ [bits 3360 to 3391] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3392 to 3423] ∈ [0..10]
+ [bits 3424 to 3455] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3456 to 3487] ∈ [0..10]
+ [bits 3488 to 3519] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3520 to 3551] ∈ [0..10]
+ [bits 3552 to 3583] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3584 to 3615] ∈ [0..10]
+ [bits 3616 to 3647] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3648 to 3679] ∈ [0..10]
+ [bits 3680 to 3711] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3712 to 3743] ∈ [0..10]
+ [bits 3744 to 3775] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3776 to 3807] ∈ [0..10]
+ [bits 3808 to 3839] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3840 to 3871] ∈ [0..10]
+ [bits 3872 to 3903] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3904 to 3935] ∈ [0..10]
+ [bits 3936 to 3967] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3968 to 3999] ∈ [0..10]
+ [bits 4000 to 4031] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4032 to 4063] ∈ [0..10]
+ [bits 4064 to 4095] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4096 to 4127] ∈ [0..10]
+ [bits 4128 to 4159] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4160 to 4191] ∈ [0..10]
+ [bits 4192 to 4223] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4224 to 4255] ∈ [0..10]
+ [bits 4256 to 4287] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4288 to 4319] ∈ [0..10]
+ [bits 4320 to 4351] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4352 to 4383] ∈ [0..10]
+ [bits 4384 to 4415] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4416 to 4447] ∈ [0..10]
+ [bits 4448 to 4479] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4480 to 4511] ∈ [0..10]
+ [bits 4512 to 4543] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4544 to 4575] ∈ [0..10]
+ [bits 4576 to 4607] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4608 to 4639] ∈ [0..10]
+ [bits 4640 to 4671] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4672 to 4703] ∈ [0..10]
+ [bits 4704 to 4735] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4736 to 4767] ∈ [0..10]
+ [bits 4768 to 4799] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4800 to 4831] ∈ [0..10]
+ [bits 4832 to 4863] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4864 to 4895] ∈ [0..10]
+ [bits 4896 to 4927] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4928 to 4959] ∈ [0..10]
+ [bits 4960 to 4991] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4992 to 5023] ∈ [0..10]
+ [bits 5024 to 5055] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5056 to 5087] ∈ [0..10]
+ [bits 5088 to 5119] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5120 to 5151] ∈ [0..10]
+ [bits 5152 to 5183] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5184 to 5215] ∈ [0..10]
+ [bits 5216 to 5247] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5248 to 5279] ∈ [0..10]
+ [bits 5280 to 5311] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5312 to 5343] ∈ [0..10]
+ [bits 5344 to 5375] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5376 to 5407] ∈ [0..10]
+ [bits 5408 to 5439] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5440 to 5471] ∈ [0..10]
+ [bits 5472 to 5503] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5504 to 5535] ∈ [0..10]
+ [bits 5536 to 5567] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5568 to 5599] ∈ [0..10]
+ [bits 5600 to 5631] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5632 to 5663] ∈ [0..10]
+ [bits 5664 to 5695] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5696 to 5727] ∈ [0..10]
+ [bits 5728 to 5759] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5760 to 5791] ∈ [0..10]
+ [bits 5792 to 5823] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5824 to 5855] ∈ [0..10]
+ [bits 5856 to 5887] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5888 to 5919] ∈ [0..10]
+ [bits 5920 to 5951] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5952 to 5983] ∈ [0..10]
+ [bits 5984 to 6015] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6016 to 6047] ∈ [0..10]
+ [bits 6048 to 6079] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6080 to 6111] ∈ [0..10]
+ [bits 6112 to 6143] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6144 to 6175] ∈ [0..10]
+ [bits 6176 to 6207] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6208 to 6239] ∈ [0..10]
+ [bits 6240 to 6271] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6272 to 6303] ∈ [0..10]
+ [bits 6304 to 6335] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6336 to 6367] ∈ [0..10]
+ [bits 6368 to 6399] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6400 to 6431] ∈ [0..10]
+ [bits 6432 to 6463] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6464 to 6495] ∈ [0..10]
+ [bits 6496 to 6527] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6528 to 6559] ∈ [0..10]
+ [bits 6560 to 6591] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6592 to 6623] ∈ [0..10]
+ [bits 6624 to 6655] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6656 to 6687] ∈ [0..10]
+ [bits 6688 to 6719] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6720 to 6751] ∈ [0..10]
+ [bits 6752 to 6783] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6784 to 6815] ∈ [0..10]
+ [bits 6816 to 6847] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6848 to 6879] ∈ [0..10]
+ [bits 6880 to 6911] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6912 to 6943] ∈ [0..10]
+ [bits 6944 to 6975] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6976 to 7007] ∈ [0..10]
+ [bits 7008 to 7039] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7040 to 7071] ∈ [0..10]
+ [bits 7072 to 7103] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7104 to 7135] ∈ [0..10]
+ [bits 7136 to 7167] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7168 to 7199] ∈ [0..10]
+ [bits 7200 to 7231] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7232 to 7263] ∈ [0..10]
+ [bits 7264 to 7295] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7296 to 7327] ∈ [0..10]
+ [bits 7328 to 7359] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7360 to 7391] ∈ [0..10]
+ [bits 7392 to 7423] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7424 to 7455] ∈ [0..10]
+ [bits 7456 to 7487] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7488 to 7519] ∈ [0..10]
+ [bits 7520 to 7551] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7552 to 7583] ∈ [0..10]
+ [bits 7584 to 7615] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7616 to 7647] ∈ [0..10]
+ [bits 7648 to 7679] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7680 to 7711] ∈ [0..10]
+ [bits 7712 to 7743] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7744 to 7775] ∈ [0..10]
+ [bits 7776 to 7807] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7808 to 7839] ∈ [0..10]
+ [bits 7840 to 7871] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7872 to 7903] ∈ [0..10]
+ [bits 7904 to 7935] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7936 to 7967] ∈ [0..10]
+ [bits 7968 to 7999] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 8000 to 8031] ∈ [0..10]
+ [bits 8032 to 8063] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 8064 to 8095] ∈ [0..10]
+ [bits 8096 to 8127] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [1016..1023] ∈ {0}
+ __fc_errno ∈ [--..--]
+ __fc_stderr ∈ {{ &__fc_initial_stderr }}
+ __fc_stdin ∈ {{ &__fc_initial_stdin }}
+ __fc_stdout ∈ {{ &__fc_initial_stdout }}
+ __fc_fopen[0..15] ∈ {0}
+ __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
+ __fc_heap_status ∈ [--..--]
+ __fc_random_counter ∈ [--..--]
+ __fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
+ __fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
+ [1] ∈ {{ NULL ; &S_1___fc_env[0] }}
+ [2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
+ __fc_mblen_state ∈ [--..--]
+ __fc_mbtowc_state ∈ [--..--]
+ __fc_wctomb_state ∈ [--..--]
+ __fc_initial_stdout.__fc_FILE_id ∈ {1}
+ .__fc_FILE_data ∈ {0}
+ __fc_initial_stderr.__fc_FILE_id ∈ {2}
+ .__fc_FILE_data ∈ {0}
+ __fc_initial_stdin ∈ {0}
+ curr ∈ {{ NULL ; &MEMORY + [0..1008],0%8 }}
+ head ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ i ∈ [1..10]
+ malloc_next_free ∈ [8..1032],0%8
+ S_0___fc_env[0..1] ∈ [--..--]
+ S_1___fc_env[0..1] ∈ [--..--]
+ ==END OF DUMP==
+[eva] tests/builtins/linked_list.c:40:
+ Frama_C_dump_each:
+ # Cvalue domain:
+ MEMORY[bits 0 to 31] ∈ [0..10]
+ [bits 32 to 63] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 64 to 95] ∈ [0..10]
+ [bits 96 to 127] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 128 to 159] ∈ [0..10]
+ [bits 160 to 191] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 192 to 223] ∈ [0..10]
+ [bits 224 to 255] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 256 to 287] ∈ [0..10]
+ [bits 288 to 319] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 320 to 351] ∈ [0..10]
+ [bits 352 to 383] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 384 to 415] ∈ [0..10]
+ [bits 416 to 447] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 448 to 479] ∈ [0..10]
+ [bits 480 to 511] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 512 to 543] ∈ [0..10]
+ [bits 544 to 575] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 576 to 607] ∈ [0..10]
+ [bits 608 to 639] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 640 to 671] ∈ [0..10]
+ [bits 672 to 703] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 704 to 735] ∈ [0..10]
+ [bits 736 to 767] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 768 to 799] ∈ [0..10]
+ [bits 800 to 831] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 832 to 863] ∈ [0..10]
+ [bits 864 to 895] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 896 to 927] ∈ [0..10]
+ [bits 928 to 959] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 960 to 991] ∈ [0..10]
+ [bits 992 to 1023] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1024 to 1055] ∈ [0..10]
+ [bits 1056 to 1087] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1088 to 1119] ∈ [0..10]
+ [bits 1120 to 1151] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1152 to 1183] ∈ [0..10]
+ [bits 1184 to 1215] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1216 to 1247] ∈ [0..10]
+ [bits 1248 to 1279] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1280 to 1311] ∈ [0..10]
+ [bits 1312 to 1343] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1344 to 1375] ∈ [0..10]
+ [bits 1376 to 1407] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1408 to 1439] ∈ [0..10]
+ [bits 1440 to 1471] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1472 to 1503] ∈ [0..10]
+ [bits 1504 to 1535] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1536 to 1567] ∈ [0..10]
+ [bits 1568 to 1599] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1600 to 1631] ∈ [0..10]
+ [bits 1632 to 1663] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1664 to 1695] ∈ [0..10]
+ [bits 1696 to 1727] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1728 to 1759] ∈ [0..10]
+ [bits 1760 to 1791] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1792 to 1823] ∈ [0..10]
+ [bits 1824 to 1855] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1856 to 1887] ∈ [0..10]
+ [bits 1888 to 1919] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1920 to 1951] ∈ [0..10]
+ [bits 1952 to 1983] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1984 to 2015] ∈ [0..10]
+ [bits 2016 to 2047] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2048 to 2079] ∈ [0..10]
+ [bits 2080 to 2111] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2112 to 2143] ∈ [0..10]
+ [bits 2144 to 2175] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2176 to 2207] ∈ [0..10]
+ [bits 2208 to 2239] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2240 to 2271] ∈ [0..10]
+ [bits 2272 to 2303] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2304 to 2335] ∈ [0..10]
+ [bits 2336 to 2367] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2368 to 2399] ∈ [0..10]
+ [bits 2400 to 2431] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2432 to 2463] ∈ [0..10]
+ [bits 2464 to 2495] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2496 to 2527] ∈ [0..10]
+ [bits 2528 to 2559] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2560 to 2591] ∈ [0..10]
+ [bits 2592 to 2623] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2624 to 2655] ∈ [0..10]
+ [bits 2656 to 2687] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2688 to 2719] ∈ [0..10]
+ [bits 2720 to 2751] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2752 to 2783] ∈ [0..10]
+ [bits 2784 to 2815] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2816 to 2847] ∈ [0..10]
+ [bits 2848 to 2879] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2880 to 2911] ∈ [0..10]
+ [bits 2912 to 2943] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2944 to 2975] ∈ [0..10]
+ [bits 2976 to 3007] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3008 to 3039] ∈ [0..10]
+ [bits 3040 to 3071] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3072 to 3103] ∈ [0..10]
+ [bits 3104 to 3135] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3136 to 3167] ∈ [0..10]
+ [bits 3168 to 3199] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3200 to 3231] ∈ [0..10]
+ [bits 3232 to 3263] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3264 to 3295] ∈ [0..10]
+ [bits 3296 to 3327] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3328 to 3359] ∈ [0..10]
+ [bits 3360 to 3391] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3392 to 3423] ∈ [0..10]
+ [bits 3424 to 3455] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3456 to 3487] ∈ [0..10]
+ [bits 3488 to 3519] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3520 to 3551] ∈ [0..10]
+ [bits 3552 to 3583] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3584 to 3615] ∈ [0..10]
+ [bits 3616 to 3647] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3648 to 3679] ∈ [0..10]
+ [bits 3680 to 3711] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3712 to 3743] ∈ [0..10]
+ [bits 3744 to 3775] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3776 to 3807] ∈ [0..10]
+ [bits 3808 to 3839] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3840 to 3871] ∈ [0..10]
+ [bits 3872 to 3903] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3904 to 3935] ∈ [0..10]
+ [bits 3936 to 3967] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3968 to 3999] ∈ [0..10]
+ [bits 4000 to 4031] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4032 to 4063] ∈ [0..10]
+ [bits 4064 to 4095] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4096 to 4127] ∈ [0..10]
+ [bits 4128 to 4159] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4160 to 4191] ∈ [0..10]
+ [bits 4192 to 4223] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4224 to 4255] ∈ [0..10]
+ [bits 4256 to 4287] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4288 to 4319] ∈ [0..10]
+ [bits 4320 to 4351] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4352 to 4383] ∈ [0..10]
+ [bits 4384 to 4415] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4416 to 4447] ∈ [0..10]
+ [bits 4448 to 4479] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4480 to 4511] ∈ [0..10]
+ [bits 4512 to 4543] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4544 to 4575] ∈ [0..10]
+ [bits 4576 to 4607] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4608 to 4639] ∈ [0..10]
+ [bits 4640 to 4671] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4672 to 4703] ∈ [0..10]
+ [bits 4704 to 4735] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4736 to 4767] ∈ [0..10]
+ [bits 4768 to 4799] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4800 to 4831] ∈ [0..10]
+ [bits 4832 to 4863] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4864 to 4895] ∈ [0..10]
+ [bits 4896 to 4927] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4928 to 4959] ∈ [0..10]
+ [bits 4960 to 4991] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4992 to 5023] ∈ [0..10]
+ [bits 5024 to 5055] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5056 to 5087] ∈ [0..10]
+ [bits 5088 to 5119] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5120 to 5151] ∈ [0..10]
+ [bits 5152 to 5183] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5184 to 5215] ∈ [0..10]
+ [bits 5216 to 5247] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5248 to 5279] ∈ [0..10]
+ [bits 5280 to 5311] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5312 to 5343] ∈ [0..10]
+ [bits 5344 to 5375] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5376 to 5407] ∈ [0..10]
+ [bits 5408 to 5439] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5440 to 5471] ∈ [0..10]
+ [bits 5472 to 5503] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5504 to 5535] ∈ [0..10]
+ [bits 5536 to 5567] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5568 to 5599] ∈ [0..10]
+ [bits 5600 to 5631] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5632 to 5663] ∈ [0..10]
+ [bits 5664 to 5695] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5696 to 5727] ∈ [0..10]
+ [bits 5728 to 5759] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5760 to 5791] ∈ [0..10]
+ [bits 5792 to 5823] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5824 to 5855] ∈ [0..10]
+ [bits 5856 to 5887] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5888 to 5919] ∈ [0..10]
+ [bits 5920 to 5951] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5952 to 5983] ∈ [0..10]
+ [bits 5984 to 6015] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6016 to 6047] ∈ [0..10]
+ [bits 6048 to 6079] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6080 to 6111] ∈ [0..10]
+ [bits 6112 to 6143] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6144 to 6175] ∈ [0..10]
+ [bits 6176 to 6207] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6208 to 6239] ∈ [0..10]
+ [bits 6240 to 6271] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6272 to 6303] ∈ [0..10]
+ [bits 6304 to 6335] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6336 to 6367] ∈ [0..10]
+ [bits 6368 to 6399] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6400 to 6431] ∈ [0..10]
+ [bits 6432 to 6463] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6464 to 6495] ∈ [0..10]
+ [bits 6496 to 6527] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6528 to 6559] ∈ [0..10]
+ [bits 6560 to 6591] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6592 to 6623] ∈ [0..10]
+ [bits 6624 to 6655] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6656 to 6687] ∈ [0..10]
+ [bits 6688 to 6719] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6720 to 6751] ∈ [0..10]
+ [bits 6752 to 6783] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6784 to 6815] ∈ [0..10]
+ [bits 6816 to 6847] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6848 to 6879] ∈ [0..10]
+ [bits 6880 to 6911] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6912 to 6943] ∈ [0..10]
+ [bits 6944 to 6975] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6976 to 7007] ∈ [0..10]
+ [bits 7008 to 7039] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7040 to 7071] ∈ [0..10]
+ [bits 7072 to 7103] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7104 to 7135] ∈ [0..10]
+ [bits 7136 to 7167] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7168 to 7199] ∈ [0..10]
+ [bits 7200 to 7231] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7232 to 7263] ∈ [0..10]
+ [bits 7264 to 7295] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7296 to 7327] ∈ [0..10]
+ [bits 7328 to 7359] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7360 to 7391] ∈ [0..10]
+ [bits 7392 to 7423] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7424 to 7455] ∈ [0..10]
+ [bits 7456 to 7487] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7488 to 7519] ∈ [0..10]
+ [bits 7520 to 7551] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7552 to 7583] ∈ [0..10]
+ [bits 7584 to 7615] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7616 to 7647] ∈ [0..10]
+ [bits 7648 to 7679] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7680 to 7711] ∈ [0..10]
+ [bits 7712 to 7743] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7744 to 7775] ∈ [0..10]
+ [bits 7776 to 7807] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7808 to 7839] ∈ [0..10]
+ [bits 7840 to 7871] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7872 to 7903] ∈ [0..10]
+ [bits 7904 to 7935] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7936 to 7967] ∈ [0..10]
+ [bits 7968 to 7999] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 8000 to 8031] ∈ [0..10]
+ [bits 8032 to 8063] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 8064 to 8095] ∈ [0..10]
+ [bits 8096 to 8127] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [1016..1023] ∈ {0}
+ __fc_errno ∈ [--..--]
+ __fc_stderr ∈ {{ &__fc_initial_stderr }}
+ __fc_stdin ∈ {{ &__fc_initial_stdin }}
+ __fc_stdout ∈ {{ &__fc_initial_stdout }}
+ __fc_fopen[0..15] ∈ {0}
+ __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
+ __fc_heap_status ∈ [--..--]
+ __fc_random_counter ∈ [--..--]
+ __fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
+ __fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
+ [1] ∈ {{ NULL ; &S_1___fc_env[0] }}
+ [2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
+ __fc_mblen_state ∈ [--..--]
+ __fc_mbtowc_state ∈ [--..--]
+ __fc_wctomb_state ∈ [--..--]
+ __fc_initial_stdout.__fc_FILE_id ∈ {1}
+ .__fc_FILE_data ∈ {0}
+ __fc_initial_stderr.__fc_FILE_id ∈ {2}
+ .__fc_FILE_data ∈ {0}
+ __fc_initial_stdin ∈ {0}
+ curr ∈ {{ &MEMORY + [0..1016],0%8 }} or UNINITIALIZED
+ head ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ i ∈ [1..10]
+ malloc_next_free ∈ [0..2147483640],0%8
+ S_0___fc_env[0..1] ∈ [--..--]
+ S_1___fc_env[0..1] ∈ [--..--]
+ ==END OF DUMP==
+[eva] computing for function malloc <- main.
+ Called from tests/builtins/linked_list.c:41.
+[eva] Recording results for malloc
+[eva] Done for function malloc
+[eva] tests/builtins/linked_list.c:42:
+ Frama_C_dump_each:
+ # Cvalue domain:
+ MEMORY[bits 0 to 31] ∈ [0..10]
+ [bits 32 to 63] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 64 to 95] ∈ [0..10]
+ [bits 96 to 127] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 128 to 159] ∈ [0..10]
+ [bits 160 to 191] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 192 to 223] ∈ [0..10]
+ [bits 224 to 255] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 256 to 287] ∈ [0..10]
+ [bits 288 to 319] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 320 to 351] ∈ [0..10]
+ [bits 352 to 383] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 384 to 415] ∈ [0..10]
+ [bits 416 to 447] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 448 to 479] ∈ [0..10]
+ [bits 480 to 511] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 512 to 543] ∈ [0..10]
+ [bits 544 to 575] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 576 to 607] ∈ [0..10]
+ [bits 608 to 639] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 640 to 671] ∈ [0..10]
+ [bits 672 to 703] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 704 to 735] ∈ [0..10]
+ [bits 736 to 767] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 768 to 799] ∈ [0..10]
+ [bits 800 to 831] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 832 to 863] ∈ [0..10]
+ [bits 864 to 895] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 896 to 927] ∈ [0..10]
+ [bits 928 to 959] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 960 to 991] ∈ [0..10]
+ [bits 992 to 1023] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1024 to 1055] ∈ [0..10]
+ [bits 1056 to 1087] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1088 to 1119] ∈ [0..10]
+ [bits 1120 to 1151] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1152 to 1183] ∈ [0..10]
+ [bits 1184 to 1215] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1216 to 1247] ∈ [0..10]
+ [bits 1248 to 1279] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1280 to 1311] ∈ [0..10]
+ [bits 1312 to 1343] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1344 to 1375] ∈ [0..10]
+ [bits 1376 to 1407] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1408 to 1439] ∈ [0..10]
+ [bits 1440 to 1471] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1472 to 1503] ∈ [0..10]
+ [bits 1504 to 1535] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1536 to 1567] ∈ [0..10]
+ [bits 1568 to 1599] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1600 to 1631] ∈ [0..10]
+ [bits 1632 to 1663] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1664 to 1695] ∈ [0..10]
+ [bits 1696 to 1727] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1728 to 1759] ∈ [0..10]
+ [bits 1760 to 1791] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1792 to 1823] ∈ [0..10]
+ [bits 1824 to 1855] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1856 to 1887] ∈ [0..10]
+ [bits 1888 to 1919] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1920 to 1951] ∈ [0..10]
+ [bits 1952 to 1983] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1984 to 2015] ∈ [0..10]
+ [bits 2016 to 2047] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2048 to 2079] ∈ [0..10]
+ [bits 2080 to 2111] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2112 to 2143] ∈ [0..10]
+ [bits 2144 to 2175] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2176 to 2207] ∈ [0..10]
+ [bits 2208 to 2239] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2240 to 2271] ∈ [0..10]
+ [bits 2272 to 2303] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2304 to 2335] ∈ [0..10]
+ [bits 2336 to 2367] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2368 to 2399] ∈ [0..10]
+ [bits 2400 to 2431] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2432 to 2463] ∈ [0..10]
+ [bits 2464 to 2495] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2496 to 2527] ∈ [0..10]
+ [bits 2528 to 2559] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2560 to 2591] ∈ [0..10]
+ [bits 2592 to 2623] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2624 to 2655] ∈ [0..10]
+ [bits 2656 to 2687] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2688 to 2719] ∈ [0..10]
+ [bits 2720 to 2751] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2752 to 2783] ∈ [0..10]
+ [bits 2784 to 2815] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2816 to 2847] ∈ [0..10]
+ [bits 2848 to 2879] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2880 to 2911] ∈ [0..10]
+ [bits 2912 to 2943] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2944 to 2975] ∈ [0..10]
+ [bits 2976 to 3007] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3008 to 3039] ∈ [0..10]
+ [bits 3040 to 3071] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3072 to 3103] ∈ [0..10]
+ [bits 3104 to 3135] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3136 to 3167] ∈ [0..10]
+ [bits 3168 to 3199] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3200 to 3231] ∈ [0..10]
+ [bits 3232 to 3263] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3264 to 3295] ∈ [0..10]
+ [bits 3296 to 3327] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3328 to 3359] ∈ [0..10]
+ [bits 3360 to 3391] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3392 to 3423] ∈ [0..10]
+ [bits 3424 to 3455] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3456 to 3487] ∈ [0..10]
+ [bits 3488 to 3519] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3520 to 3551] ∈ [0..10]
+ [bits 3552 to 3583] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3584 to 3615] ∈ [0..10]
+ [bits 3616 to 3647] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3648 to 3679] ∈ [0..10]
+ [bits 3680 to 3711] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3712 to 3743] ∈ [0..10]
+ [bits 3744 to 3775] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3776 to 3807] ∈ [0..10]
+ [bits 3808 to 3839] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3840 to 3871] ∈ [0..10]
+ [bits 3872 to 3903] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3904 to 3935] ∈ [0..10]
+ [bits 3936 to 3967] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3968 to 3999] ∈ [0..10]
+ [bits 4000 to 4031] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4032 to 4063] ∈ [0..10]
+ [bits 4064 to 4095] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4096 to 4127] ∈ [0..10]
+ [bits 4128 to 4159] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4160 to 4191] ∈ [0..10]
+ [bits 4192 to 4223] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4224 to 4255] ∈ [0..10]
+ [bits 4256 to 4287] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4288 to 4319] ∈ [0..10]
+ [bits 4320 to 4351] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4352 to 4383] ∈ [0..10]
+ [bits 4384 to 4415] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4416 to 4447] ∈ [0..10]
+ [bits 4448 to 4479] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4480 to 4511] ∈ [0..10]
+ [bits 4512 to 4543] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4544 to 4575] ∈ [0..10]
+ [bits 4576 to 4607] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4608 to 4639] ∈ [0..10]
+ [bits 4640 to 4671] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4672 to 4703] ∈ [0..10]
+ [bits 4704 to 4735] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4736 to 4767] ∈ [0..10]
+ [bits 4768 to 4799] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4800 to 4831] ∈ [0..10]
+ [bits 4832 to 4863] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4864 to 4895] ∈ [0..10]
+ [bits 4896 to 4927] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4928 to 4959] ∈ [0..10]
+ [bits 4960 to 4991] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4992 to 5023] ∈ [0..10]
+ [bits 5024 to 5055] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5056 to 5087] ∈ [0..10]
+ [bits 5088 to 5119] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5120 to 5151] ∈ [0..10]
+ [bits 5152 to 5183] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5184 to 5215] ∈ [0..10]
+ [bits 5216 to 5247] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5248 to 5279] ∈ [0..10]
+ [bits 5280 to 5311] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5312 to 5343] ∈ [0..10]
+ [bits 5344 to 5375] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5376 to 5407] ∈ [0..10]
+ [bits 5408 to 5439] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5440 to 5471] ∈ [0..10]
+ [bits 5472 to 5503] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5504 to 5535] ∈ [0..10]
+ [bits 5536 to 5567] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5568 to 5599] ∈ [0..10]
+ [bits 5600 to 5631] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5632 to 5663] ∈ [0..10]
+ [bits 5664 to 5695] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5696 to 5727] ∈ [0..10]
+ [bits 5728 to 5759] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5760 to 5791] ∈ [0..10]
+ [bits 5792 to 5823] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5824 to 5855] ∈ [0..10]
+ [bits 5856 to 5887] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5888 to 5919] ∈ [0..10]
+ [bits 5920 to 5951] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5952 to 5983] ∈ [0..10]
+ [bits 5984 to 6015] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6016 to 6047] ∈ [0..10]
+ [bits 6048 to 6079] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6080 to 6111] ∈ [0..10]
+ [bits 6112 to 6143] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6144 to 6175] ∈ [0..10]
+ [bits 6176 to 6207] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6208 to 6239] ∈ [0..10]
+ [bits 6240 to 6271] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6272 to 6303] ∈ [0..10]
+ [bits 6304 to 6335] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6336 to 6367] ∈ [0..10]
+ [bits 6368 to 6399] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6400 to 6431] ∈ [0..10]
+ [bits 6432 to 6463] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6464 to 6495] ∈ [0..10]
+ [bits 6496 to 6527] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6528 to 6559] ∈ [0..10]
+ [bits 6560 to 6591] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6592 to 6623] ∈ [0..10]
+ [bits 6624 to 6655] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6656 to 6687] ∈ [0..10]
+ [bits 6688 to 6719] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6720 to 6751] ∈ [0..10]
+ [bits 6752 to 6783] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6784 to 6815] ∈ [0..10]
+ [bits 6816 to 6847] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6848 to 6879] ∈ [0..10]
+ [bits 6880 to 6911] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6912 to 6943] ∈ [0..10]
+ [bits 6944 to 6975] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6976 to 7007] ∈ [0..10]
+ [bits 7008 to 7039] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7040 to 7071] ∈ [0..10]
+ [bits 7072 to 7103] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7104 to 7135] ∈ [0..10]
+ [bits 7136 to 7167] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7168 to 7199] ∈ [0..10]
+ [bits 7200 to 7231] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7232 to 7263] ∈ [0..10]
+ [bits 7264 to 7295] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7296 to 7327] ∈ [0..10]
+ [bits 7328 to 7359] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7360 to 7391] ∈ [0..10]
+ [bits 7392 to 7423] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7424 to 7455] ∈ [0..10]
+ [bits 7456 to 7487] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7488 to 7519] ∈ [0..10]
+ [bits 7520 to 7551] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7552 to 7583] ∈ [0..10]
+ [bits 7584 to 7615] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7616 to 7647] ∈ [0..10]
+ [bits 7648 to 7679] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7680 to 7711] ∈ [0..10]
+ [bits 7712 to 7743] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7744 to 7775] ∈ [0..10]
+ [bits 7776 to 7807] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7808 to 7839] ∈ [0..10]
+ [bits 7840 to 7871] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7872 to 7903] ∈ [0..10]
+ [bits 7904 to 7935] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7936 to 7967] ∈ [0..10]
+ [bits 7968 to 7999] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 8000 to 8031] ∈ [0..10]
+ [bits 8032 to 8063] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 8064 to 8095] ∈ [0..10]
+ [bits 8096 to 8127] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [1016..1023] ∈ {0}
+ __fc_errno ∈ [--..--]
+ __fc_stderr ∈ {{ &__fc_initial_stderr }}
+ __fc_stdin ∈ {{ &__fc_initial_stdin }}
+ __fc_stdout ∈ {{ &__fc_initial_stdout }}
+ __fc_fopen[0..15] ∈ {0}
+ __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..2047] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
+ __fc_heap_status ∈ [--..--]
+ __fc_random_counter ∈ [--..--]
+ __fc_rand_max ∈ {32767}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
+ __fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
+ [1] ∈ {{ NULL ; &S_1___fc_env[0] }}
+ [2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
+ __fc_mblen_state ∈ [--..--]
+ __fc_mbtowc_state ∈ [--..--]
+ __fc_wctomb_state ∈ [--..--]
+ __fc_initial_stdout.__fc_FILE_id ∈ {1}
+ .__fc_FILE_data ∈ {0}
+ __fc_initial_stderr.__fc_FILE_id ∈ {2}
+ .__fc_FILE_data ∈ {0}
+ __fc_initial_stdin ∈ {0}
+ curr ∈ {{ NULL ; &MEMORY + [0..4294967288],0%8 }}
+ head ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ i ∈ [1..10]
+ malloc_next_free ∈ [-2147483648..2147483640],0%8
+ S_0___fc_env[0..1] ∈ [--..--]
+ S_1___fc_env[0..1] ∈ [--..--]
+ ==END OF DUMP==
+[eva] tests/builtins/linked_list.c:40:
+ Frama_C_dump_each:
+ # Cvalue domain:
+ MEMORY[bits 0 to 31] ∈ [0..10]
+ [bits 32 to 63] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 64 to 95] ∈ [0..10]
+ [bits 96 to 127] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 128 to 159] ∈ [0..10]
+ [bits 160 to 191] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 192 to 223] ∈ [0..10]
+ [bits 224 to 255] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 256 to 287] ∈ [0..10]
+ [bits 288 to 319] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 320 to 351] ∈ [0..10]
+ [bits 352 to 383] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 384 to 415] ∈ [0..10]
+ [bits 416 to 447] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 448 to 479] ∈ [0..10]
+ [bits 480 to 511] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 512 to 543] ∈ [0..10]
+ [bits 544 to 575] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 576 to 607] ∈ [0..10]
+ [bits 608 to 639] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 640 to 671] ∈ [0..10]
+ [bits 672 to 703] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 704 to 735] ∈ [0..10]
+ [bits 736 to 767] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 768 to 799] ∈ [0..10]
+ [bits 800 to 831] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 832 to 863] ∈ [0..10]
+ [bits 864 to 895] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 896 to 927] ∈ [0..10]
+ [bits 928 to 959] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 960 to 991] ∈ [0..10]
+ [bits 992 to 1023] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1024 to 1055] ∈ [0..10]
+ [bits 1056 to 1087] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1088 to 1119] ∈ [0..10]
+ [bits 1120 to 1151] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1152 to 1183] ∈ [0..10]
+ [bits 1184 to 1215] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1216 to 1247] ∈ [0..10]
+ [bits 1248 to 1279] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1280 to 1311] ∈ [0..10]
+ [bits 1312 to 1343] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1344 to 1375] ∈ [0..10]
+ [bits 1376 to 1407] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1408 to 1439] ∈ [0..10]
+ [bits 1440 to 1471] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1472 to 1503] ∈ [0..10]
+ [bits 1504 to 1535] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1536 to 1567] ∈ [0..10]
+ [bits 1568 to 1599] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1600 to 1631] ∈ [0..10]
+ [bits 1632 to 1663] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1664 to 1695] ∈ [0..10]
+ [bits 1696 to 1727] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1728 to 1759] ∈ [0..10]
+ [bits 1760 to 1791] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1792 to 1823] ∈ [0..10]
+ [bits 1824 to 1855] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1856 to 1887] ∈ [0..10]
+ [bits 1888 to 1919] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1920 to 1951] ∈ [0..10]
+ [bits 1952 to 1983] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 1984 to 2015] ∈ [0..10]
+ [bits 2016 to 2047] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2048 to 2079] ∈ [0..10]
+ [bits 2080 to 2111] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2112 to 2143] ∈ [0..10]
+ [bits 2144 to 2175] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2176 to 2207] ∈ [0..10]
+ [bits 2208 to 2239] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2240 to 2271] ∈ [0..10]
+ [bits 2272 to 2303] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2304 to 2335] ∈ [0..10]
+ [bits 2336 to 2367] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2368 to 2399] ∈ [0..10]
+ [bits 2400 to 2431] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2432 to 2463] ∈ [0..10]
+ [bits 2464 to 2495] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2496 to 2527] ∈ [0..10]
+ [bits 2528 to 2559] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2560 to 2591] ∈ [0..10]
+ [bits 2592 to 2623] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2624 to 2655] ∈ [0..10]
+ [bits 2656 to 2687] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2688 to 2719] ∈ [0..10]
+ [bits 2720 to 2751] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2752 to 2783] ∈ [0..10]
+ [bits 2784 to 2815] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2816 to 2847] ∈ [0..10]
+ [bits 2848 to 2879] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2880 to 2911] ∈ [0..10]
+ [bits 2912 to 2943] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 2944 to 2975] ∈ [0..10]
+ [bits 2976 to 3007] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3008 to 3039] ∈ [0..10]
+ [bits 3040 to 3071] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3072 to 3103] ∈ [0..10]
+ [bits 3104 to 3135] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3136 to 3167] ∈ [0..10]
+ [bits 3168 to 3199] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3200 to 3231] ∈ [0..10]
+ [bits 3232 to 3263] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3264 to 3295] ∈ [0..10]
+ [bits 3296 to 3327] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3328 to 3359] ∈ [0..10]
+ [bits 3360 to 3391] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3392 to 3423] ∈ [0..10]
+ [bits 3424 to 3455] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3456 to 3487] ∈ [0..10]
+ [bits 3488 to 3519] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3520 to 3551] ∈ [0..10]
+ [bits 3552 to 3583] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3584 to 3615] ∈ [0..10]
+ [bits 3616 to 3647] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3648 to 3679] ∈ [0..10]
+ [bits 3680 to 3711] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3712 to 3743] ∈ [0..10]
+ [bits 3744 to 3775] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3776 to 3807] ∈ [0..10]
+ [bits 3808 to 3839] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3840 to 3871] ∈ [0..10]
+ [bits 3872 to 3903] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3904 to 3935] ∈ [0..10]
+ [bits 3936 to 3967] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 3968 to 3999] ∈ [0..10]
+ [bits 4000 to 4031] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4032 to 4063] ∈ [0..10]
+ [bits 4064 to 4095] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4096 to 4127] ∈ [0..10]
+ [bits 4128 to 4159] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4160 to 4191] ∈ [0..10]
+ [bits 4192 to 4223] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4224 to 4255] ∈ [0..10]
+ [bits 4256 to 4287] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4288 to 4319] ∈ [0..10]
+ [bits 4320 to 4351] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4352 to 4383] ∈ [0..10]
+ [bits 4384 to 4415] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4416 to 4447] ∈ [0..10]
+ [bits 4448 to 4479] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4480 to 4511] ∈ [0..10]
+ [bits 4512 to 4543] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4544 to 4575] ∈ [0..10]
+ [bits 4576 to 4607] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4608 to 4639] ∈ [0..10]
+ [bits 4640 to 4671] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4672 to 4703] ∈ [0..10]
+ [bits 4704 to 4735] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4736 to 4767] ∈ [0..10]
+ [bits 4768 to 4799] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4800 to 4831] ∈ [0..10]
+ [bits 4832 to 4863] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4864 to 4895] ∈ [0..10]
+ [bits 4896 to 4927] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4928 to 4959] ∈ [0..10]
+ [bits 4960 to 4991] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 4992 to 5023] ∈ [0..10]
+ [bits 5024 to 5055] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5056 to 5087] ∈ [0..10]
+ [bits 5088 to 5119] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5120 to 5151] ∈ [0..10]
+ [bits 5152 to 5183] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5184 to 5215] ∈ [0..10]
+ [bits 5216 to 5247] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5248 to 5279] ∈ [0..10]
+ [bits 5280 to 5311] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5312 to 5343] ∈ [0..10]
+ [bits 5344 to 5375] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5376 to 5407] ∈ [0..10]
+ [bits 5408 to 5439] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5440 to 5471] ∈ [0..10]
+ [bits 5472 to 5503] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5504 to 5535] ∈ [0..10]
+ [bits 5536 to 5567] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5568 to 5599] ∈ [0..10]
+ [bits 5600 to 5631] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5632 to 5663] ∈ [0..10]
+ [bits 5664 to 5695] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5696 to 5727] ∈ [0..10]
+ [bits 5728 to 5759] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5760 to 5791] ∈ [0..10]
+ [bits 5792 to 5823] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5824 to 5855] ∈ [0..10]
+ [bits 5856 to 5887] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5888 to 5919] ∈ [0..10]
+ [bits 5920 to 5951] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 5952 to 5983] ∈ [0..10]
+ [bits 5984 to 6015] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6016 to 6047] ∈ [0..10]
+ [bits 6048 to 6079] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6080 to 6111] ∈ [0..10]
+ [bits 6112 to 6143] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6144 to 6175] ∈ [0..10]
+ [bits 6176 to 6207] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6208 to 6239] ∈ [0..10]
+ [bits 6240 to 6271] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6272 to 6303] ∈ [0..10]
+ [bits 6304 to 6335] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6336 to 6367] ∈ [0..10]
+ [bits 6368 to 6399] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6400 to 6431] ∈ [0..10]
+ [bits 6432 to 6463] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6464 to 6495] ∈ [0..10]
+ [bits 6496 to 6527] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6528 to 6559] ∈ [0..10]
+ [bits 6560 to 6591] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6592 to 6623] ∈ [0..10]
+ [bits 6624 to 6655] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6656 to 6687] ∈ [0..10]
+ [bits 6688 to 6719] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6720 to 6751] ∈ [0..10]
+ [bits 6752 to 6783] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6784 to 6815] ∈ [0..10]
+ [bits 6816 to 6847] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6848 to 6879] ∈ [0..10]
+ [bits 6880 to 6911] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6912 to 6943] ∈ [0..10]
+ [bits 6944 to 6975] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 6976 to 7007] ∈ [0..10]
+ [bits 7008 to 7039] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7040 to 7071] ∈ [0..10]
+ [bits 7072 to 7103] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7104 to 7135] ∈ [0..10]
+ [bits 7136 to 7167] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7168 to 7199] ∈ [0..10]
+ [bits 7200 to 7231] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7232 to 7263] ∈ [0..10]
+ [bits 7264 to 7295] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7296 to 7327] ∈ [0..10]
+ [bits 7328 to 7359] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7360 to 7391] ∈ [0..10]
+ [bits 7392 to 7423] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7424 to 7455] ∈ [0..10]
+ [bits 7456 to 7487] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7488 to 7519] ∈ [0..10]
+ [bits 7520 to 7551] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7552 to 7583] ∈ [0..10]
+ [bits 7584 to 7615] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7616 to 7647] ∈ [0..10]
+ [bits 7648 to 7679] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7680 to 7711] ∈ [0..10]
+ [bits 7712 to 7743] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7744 to 7775] ∈ [0..10]
+ [bits 7776 to 7807] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7808 to 7839] ∈ [0..10]
+ [bits 7840 to 7871] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7872 to 7903] ∈ [0..10]
+ [bits 7904 to 7935] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 7936 to 7967] ∈ [0..10]
+ [bits 7968 to 7999] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 8000 to 8031] ∈ [0..10]
+ [bits 8032 to 8063] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
+ [bits 8064 to 8095] ∈ [0..10]
+ [bits 8096 to 8127] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
[bits 8128 to 8159] ∈ [0..10]
[bits 8160 to 8191] ∈ {{ NULL ; &MEMORY + [0..1016],0%8 }}
__fc_errno ∈ [--..--]
diff --git a/tests/builtins/oracle/linked_list.1.res.oracle b/tests/builtins/oracle/linked_list.1.res.oracle
index 58a095a29ca9923f3349863a3f663a973737095e..394eac6fb30fc7d0981687ebce29e9fd510d7a60 100644
--- a/tests/builtins/oracle/linked_list.1.res.oracle
+++ b/tests/builtins/oracle/linked_list.1.res.oracle
@@ -469,7 +469,7 @@
curr ∈ {{ &MEMORY + [0..0x3F8],0%8 }} or UNINITIALIZED
head ∈ {{ NULL ; &MEMORY + [0..0x3F8],0%8 }}
i ∈ [1..10]
- malloc_next_free ∈ [0..0x7FFFFFF8],0%8
+ malloc_next_free ∈ [0..0x3F8],0%8
S_0___fc_env[0..1] ∈ [--..--]
S_1___fc_env[0..1] ∈ [--..--]
==END OF DUMP==
@@ -517,15 +517,187 @@
__fc_initial_stderr.__fc_FILE_id ∈ {2}
.__fc_FILE_data ∈ {0}
__fc_initial_stdin ∈ {0}
- curr ∈ {{ NULL ; &MEMORY + [0..0xFFFFFFF8],0%8 }}
+ curr ∈ {{ NULL ; &MEMORY + [0..0x3F0],0%8 }}
head ∈ {{ NULL ; &MEMORY + [0..0x3F8],0%8 }}
i ∈ [1..10]
- malloc_next_free ∈ [-0x80000000..0x7FFFFFF8],0%8
+ malloc_next_free ∈ [8..0x400],0%8
S_0___fc_env[0..1] ∈ [--..--]
S_1___fc_env[0..1] ∈ [--..--]
==END OF DUMP==
[eva:alarm] tests/builtins/linked_list.c:43: Warning:
out of bounds write. assert \valid(&curr->val);
+[kernel] tests/builtins/linked_list.c:43:
+ more than 100(127) locations to update in array. Approximating.
+[kernel] tests/builtins/linked_list.c:44:
+ more than 100(127) locations to update in array. Approximating.
+[eva] tests/builtins/linked_list.c:40:
+ Frama_C_dump_each:
+ # Cvalue domain:
+ MEMORY[bits 0 to 31] ∈ [0..10]
+ [bits 32 to 0x1F9F]# ∈
+ {{ NULL + [0..10] ; &MEMORY + [0..0x3F8],0%8 }} repeated %32
+ [bits 0x1FA0 to 0x1FBF] ∈ {{ NULL ; &MEMORY + [0..0x3F8],0%8 }}
+ [0x3F8..0x3FF] ∈ {0}
+ __fc_errno ∈ [--..--]
+ __fc_stderr ∈ {{ &__fc_initial_stderr }}
+ __fc_stdin ∈ {{ &__fc_initial_stdin }}
+ __fc_stdout ∈ {{ &__fc_initial_stdout }}
+ __fc_fopen[0..15] ∈ {0}
+ __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
+ __fc_heap_status ∈ [--..--]
+ __fc_random_counter ∈ [--..--]
+ __fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
+ __fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
+ [1] ∈ {{ NULL ; &S_1___fc_env[0] }}
+ [2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
+ __fc_mblen_state ∈ [--..--]
+ __fc_mbtowc_state ∈ [--..--]
+ __fc_wctomb_state ∈ [--..--]
+ __fc_initial_stdout.__fc_FILE_id ∈ {1}
+ .__fc_FILE_data ∈ {0}
+ __fc_initial_stderr.__fc_FILE_id ∈ {2}
+ .__fc_FILE_data ∈ {0}
+ __fc_initial_stdin ∈ {0}
+ curr ∈ {{ &MEMORY + [0..0x3F8],0%8 }} or UNINITIALIZED
+ head ∈ {{ NULL ; &MEMORY + [0..0x3F8],0%8 }}
+ i ∈ [1..10]
+ malloc_next_free ∈ [0..0x400],0%8
+ S_0___fc_env[0..1] ∈ [--..--]
+ S_1___fc_env[0..1] ∈ [--..--]
+ ==END OF DUMP==
+[eva] computing for function malloc <- main.
+ Called from tests/builtins/linked_list.c:41.
+[eva] Recording results for malloc
+[eva] Done for function malloc
+[eva] tests/builtins/linked_list.c:42:
+ Frama_C_dump_each:
+ # Cvalue domain:
+ MEMORY[bits 0 to 31] ∈ [0..10]
+ [bits 32 to 0x1F9F]# ∈
+ {{ NULL + [0..10] ; &MEMORY + [0..0x3F8],0%8 }} repeated %32
+ [bits 0x1FA0 to 0x1FBF] ∈ {{ NULL ; &MEMORY + [0..0x3F8],0%8 }}
+ [0x3F8..0x3FF] ∈ {0}
+ __fc_errno ∈ [--..--]
+ __fc_stderr ∈ {{ &__fc_initial_stderr }}
+ __fc_stdin ∈ {{ &__fc_initial_stdin }}
+ __fc_stdout ∈ {{ &__fc_initial_stdout }}
+ __fc_fopen[0..15] ∈ {0}
+ __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
+ __fc_heap_status ∈ [--..--]
+ __fc_random_counter ∈ [--..--]
+ __fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
+ __fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
+ [1] ∈ {{ NULL ; &S_1___fc_env[0] }}
+ [2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
+ __fc_mblen_state ∈ [--..--]
+ __fc_mbtowc_state ∈ [--..--]
+ __fc_wctomb_state ∈ [--..--]
+ __fc_initial_stdout.__fc_FILE_id ∈ {1}
+ .__fc_FILE_data ∈ {0}
+ __fc_initial_stderr.__fc_FILE_id ∈ {2}
+ .__fc_FILE_data ∈ {0}
+ __fc_initial_stdin ∈ {0}
+ curr ∈ {{ NULL ; &MEMORY + [0..0x3F0],0%8 }}
+ head ∈ {{ NULL ; &MEMORY + [0..0x3F8],0%8 }}
+ i ∈ [1..10]
+ malloc_next_free ∈ [8..0x408],0%8
+ S_0___fc_env[0..1] ∈ [--..--]
+ S_1___fc_env[0..1] ∈ [--..--]
+ ==END OF DUMP==
+[eva] tests/builtins/linked_list.c:40:
+ Frama_C_dump_each:
+ # Cvalue domain:
+ MEMORY[bits 0 to 31] ∈ [0..10]
+ [bits 32 to 0x1F9F]# ∈
+ {{ NULL + [0..10] ; &MEMORY + [0..0x3F8],0%8 }} repeated %32
+ [bits 0x1FA0 to 0x1FBF] ∈ {{ NULL ; &MEMORY + [0..0x3F8],0%8 }}
+ [0x3F8..0x3FF] ∈ {0}
+ __fc_errno ∈ [--..--]
+ __fc_stderr ∈ {{ &__fc_initial_stderr }}
+ __fc_stdin ∈ {{ &__fc_initial_stdin }}
+ __fc_stdout ∈ {{ &__fc_initial_stdout }}
+ __fc_fopen[0..15] ∈ {0}
+ __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
+ __fc_heap_status ∈ [--..--]
+ __fc_random_counter ∈ [--..--]
+ __fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
+ __fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
+ [1] ∈ {{ NULL ; &S_1___fc_env[0] }}
+ [2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
+ __fc_mblen_state ∈ [--..--]
+ __fc_mbtowc_state ∈ [--..--]
+ __fc_wctomb_state ∈ [--..--]
+ __fc_initial_stdout.__fc_FILE_id ∈ {1}
+ .__fc_FILE_data ∈ {0}
+ __fc_initial_stderr.__fc_FILE_id ∈ {2}
+ .__fc_FILE_data ∈ {0}
+ __fc_initial_stdin ∈ {0}
+ curr ∈ {{ &MEMORY + [0..0x3F8],0%8 }} or UNINITIALIZED
+ head ∈ {{ NULL ; &MEMORY + [0..0x3F8],0%8 }}
+ i ∈ [1..10]
+ malloc_next_free ∈ [0..0x7FFFFFF8],0%8
+ S_0___fc_env[0..1] ∈ [--..--]
+ S_1___fc_env[0..1] ∈ [--..--]
+ ==END OF DUMP==
+[eva] computing for function malloc <- main.
+ Called from tests/builtins/linked_list.c:41.
+[eva] Recording results for malloc
+[eva] Done for function malloc
+[eva] tests/builtins/linked_list.c:42:
+ Frama_C_dump_each:
+ # Cvalue domain:
+ MEMORY[bits 0 to 31] ∈ [0..10]
+ [bits 32 to 0x1F9F]# ∈
+ {{ NULL + [0..10] ; &MEMORY + [0..0x3F8],0%8 }} repeated %32
+ [bits 0x1FA0 to 0x1FBF] ∈ {{ NULL ; &MEMORY + [0..0x3F8],0%8 }}
+ [0x3F8..0x3FF] ∈ {0}
+ __fc_errno ∈ [--..--]
+ __fc_stderr ∈ {{ &__fc_initial_stderr }}
+ __fc_stdin ∈ {{ &__fc_initial_stdin }}
+ __fc_stdout ∈ {{ &__fc_initial_stdout }}
+ __fc_fopen[0..15] ∈ {0}
+ __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
+ __fc_tmpnam[0..0x7FF] ∈ {0}
+ __fc_p_tmpnam ∈ {{ &__fc_tmpnam[0] }}
+ __fc_heap_status ∈ [--..--]
+ __fc_random_counter ∈ [--..--]
+ __fc_rand_max ∈ {0x7FFF}
+ __fc_random48_init ∈ {0}
+ __fc_random48_counter[0..2] ∈ [--..--]
+ __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
+ __fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
+ [1] ∈ {{ NULL ; &S_1___fc_env[0] }}
+ [2..0xFFF] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
+ __fc_mblen_state ∈ [--..--]
+ __fc_mbtowc_state ∈ [--..--]
+ __fc_wctomb_state ∈ [--..--]
+ __fc_initial_stdout.__fc_FILE_id ∈ {1}
+ .__fc_FILE_data ∈ {0}
+ __fc_initial_stderr.__fc_FILE_id ∈ {2}
+ .__fc_FILE_data ∈ {0}
+ __fc_initial_stdin ∈ {0}
+ curr ∈ {{ NULL ; &MEMORY + [0..0xFFFFFFF8],0%8 }}
+ head ∈ {{ NULL ; &MEMORY + [0..0x3F8],0%8 }}
+ i ∈ [1..10]
+ malloc_next_free ∈ [-0x80000000..0x7FFFFFF8],0%8
+ S_0___fc_env[0..1] ∈ [--..--]
+ S_1___fc_env[0..1] ∈ [--..--]
+ ==END OF DUMP==
[kernel] tests/builtins/linked_list.c:43:
more than 100(128) locations to update in array. Approximating.
[kernel] tests/builtins/linked_list.c:44:
diff --git a/tests/pdg/oracle/simple_intra_slice.res.oracle b/tests/pdg/oracle/simple_intra_slice.res.oracle
index 0e0d826dd446563004cd6ed8a139416b602a05e6..f66cab9671fdd33348f745d49d85427b1d5a9375 100644
--- a/tests/pdg/oracle/simple_intra_slice.res.oracle
+++ b/tests/pdg/oracle/simple_intra_slice.res.oracle
@@ -11,10 +11,10 @@
[eva:alarm] tests/pdg/simple_intra_slice.c:99: Warning:
signed overflow. assert -2147483648 ≤ uninit - 1;
[eva] tests/pdg/simple_intra_slice.c:98: starting to merge loop iterations
-[eva:alarm] tests/pdg/simple_intra_slice.c:99: Warning:
- signed overflow. assert Unknown + 1 ≤ 2147483647;
[eva:alarm] tests/pdg/simple_intra_slice.c:99: Warning:
signed overflow. assert -2147483648 ≤ Unknown - 1;
+[eva:alarm] tests/pdg/simple_intra_slice.c:99: Warning:
+ signed overflow. assert Unknown + 1 ≤ 2147483647;
[eva:alarm] tests/pdg/simple_intra_slice.c:101: Warning:
signed overflow. assert -2147483648 ≤ uninit2 - 1;
[eva] tests/pdg/simple_intra_slice.c:100: starting to merge loop iterations
diff --git a/tests/slicing/oracle/bts1768.res.oracle b/tests/slicing/oracle/bts1768.res.oracle
index 2944f35c986bf58f4bef35facca2995fd6042406..2322f30607ec2d44af35dac97ebe2424209ef183 100644
--- a/tests/slicing/oracle/bts1768.res.oracle
+++ b/tests/slicing/oracle/bts1768.res.oracle
@@ -88,6 +88,26 @@
Called from tests/slicing/bts1768.i:46.
[eva] Recording results for fsm_transition
[eva] Done for function fsm_transition
+[eva] tests/slicing/bts1768.i:45: Reusing old results for call to lecture
+[eva] computing for function fsm_transition <- main.
+ Called from tests/slicing/bts1768.i:46.
+[eva] Recording results for fsm_transition
+[eva] Done for function fsm_transition
+[eva] tests/slicing/bts1768.i:45: Reusing old results for call to lecture
+[eva] computing for function fsm_transition <- main.
+ Called from tests/slicing/bts1768.i:46.
+[eva] Recording results for fsm_transition
+[eva] Done for function fsm_transition
+[eva] tests/slicing/bts1768.i:45: Reusing old results for call to lecture
+[eva] computing for function fsm_transition <- main.
+ Called from tests/slicing/bts1768.i:46.
+[eva] Recording results for fsm_transition
+[eva] Done for function fsm_transition
+[eva] tests/slicing/bts1768.i:45: Reusing old results for call to lecture
+[eva] computing for function fsm_transition <- main.
+ Called from tests/slicing/bts1768.i:46.
+[eva] Recording results for fsm_transition
+[eva] Done for function fsm_transition
[eva:alarm] tests/slicing/bts1768.i:51: Warning:
signed overflow. assert step + 1 ≤ 2147483647;
[eva] tests/slicing/bts1768.i:45: Reusing old results for call to lecture
diff --git a/tests/slicing/oracle/select_simple.res.oracle b/tests/slicing/oracle/select_simple.res.oracle
index 2a4d181dd9645e21781a1e0eb6d89408dd52e570..4c0a739fb0d94af548f8fb10d6425ef15f061a63 100644
--- a/tests/slicing/oracle/select_simple.res.oracle
+++ b/tests/slicing/oracle/select_simple.res.oracle
@@ -11,10 +11,10 @@
[eva:alarm] tests/slicing/simple_intra_slice.i:99: Warning:
signed overflow. assert -2147483648 ≤ uninit - 1;
[eva] tests/slicing/simple_intra_slice.i:98: starting to merge loop iterations
-[eva:alarm] tests/slicing/simple_intra_slice.i:99: Warning:
- signed overflow. assert Unknown + 1 ≤ 2147483647;
[eva:alarm] tests/slicing/simple_intra_slice.i:99: Warning:
signed overflow. assert -2147483648 ≤ Unknown - 1;
+[eva:alarm] tests/slicing/simple_intra_slice.i:99: Warning:
+ signed overflow. assert Unknown + 1 ≤ 2147483647;
[eva:alarm] tests/slicing/simple_intra_slice.i:101: Warning:
signed overflow. assert -2147483648 ≤ uninit2 - 1;
[eva] tests/slicing/simple_intra_slice.i:100: starting to merge loop iterations
diff --git a/tests/slicing/oracle/simple_intra_slice.res.oracle b/tests/slicing/oracle/simple_intra_slice.res.oracle
index 47b1ef6ecb05077d5bdde0fbee6646118f7db781..2a8fafc4d9b415efcf28b9ef1b7cf03ae5e15734 100644
--- a/tests/slicing/oracle/simple_intra_slice.res.oracle
+++ b/tests/slicing/oracle/simple_intra_slice.res.oracle
@@ -11,10 +11,10 @@
[eva:alarm] tests/slicing/simple_intra_slice.i:99: Warning:
signed overflow. assert -2147483648 ≤ uninit - 1;
[eva] tests/slicing/simple_intra_slice.i:98: starting to merge loop iterations
-[eva:alarm] tests/slicing/simple_intra_slice.i:99: Warning:
- signed overflow. assert Unknown + 1 ≤ 2147483647;
[eva:alarm] tests/slicing/simple_intra_slice.i:99: Warning:
signed overflow. assert -2147483648 ≤ Unknown - 1;
+[eva:alarm] tests/slicing/simple_intra_slice.i:99: Warning:
+ signed overflow. assert Unknown + 1 ≤ 2147483647;
[eva:alarm] tests/slicing/simple_intra_slice.i:101: Warning:
signed overflow. assert -2147483648 ≤ uninit2 - 1;
[eva] tests/slicing/simple_intra_slice.i:100: starting to merge loop iterations