Decision #853 — malloc.c:4432
Status: partial
Truth table
| row | c0 br 5983 | c1 br 5984 | c2 br 5985 | c3 br 5986 | c4 br 5987 | c5 br 5988 | c6 br 5989 | c7 br 5990 | outcome |
|---|---|---|---|---|---|---|---|---|---|
| 2869 | * | T | T | * | * | * | F | F | F |
| 2870 | * | T | T | * | * | * | F | F | F |
| 2871 | * | T | T | * | * | * | T | * | T |
| 2872 | * | T | T | * | * | * | T | * | T |
| 2873 | * | T | T | * | * | * | T | * | T |
| 2874 | * | T | T | * | * | * | T | * | T |
| 2875 | * | T | T | * | * | * | T | * | T |
| 2876 | * | T | T | * | * | * | T | * | T |
| 2877 | * | T | T | * | * | * | T | * | T |
| 2878 | * | T | T | * | * | * | T | * | T |
| 2879 | * | T | T | * | * | * | T | * | T |
| 5874 | * | T | T | * | * | * | F | F | F |
| 5875 | * | T | T | * | * | * | F | F | F |
| 5876 | * | T | T | * | * | * | T | * | T |
| 5877 | * | T | T | * | * | * | T | * | T |
| 5878 | * | T | T | * | * | * | T | * | T |
| 5879 | * | T | T | * | * | * | T | * | T |
| 5880 | * | T | T | * | * | * | T | * | T |
| 5881 | * | T | T | * | * | * | T | * | T |
| 5882 | * | T | T | * | * | * | T | * | T |
| 5883 | * | T | T | * | * | * | T | * | T |
| 5884 | * | T | T | * | * | * | T | * | T |
| 9015 | * | T | T | * | * | * | F | F | F |
| 9016 | * | T | T | * | * | * | F | F | F |
| 9017 | * | T | T | * | * | * | T | * | T |
| 9018 | * | T | T | * | * | * | T | * | T |
| 9019 | * | T | T | * | * | * | T | * | T |
| 9020 | * | T | T | * | * | * | T | * | T |
| 9021 | * | T | T | * | * | * | T | * | T |
| 9022 | * | T | T | * | * | * | T | * | T |
| 9023 | * | T | T | * | * | * | T | * | T |
| 9024 | * | T | T | * | * | * | T | * | T |
| 9025 | * | T | T | * | * | * | T | * | T |
| 9026 | * | T | T | * | * | * | T | * | T |
| 10468 | * | T | T | * | * | * | F | F | F |
| 10469 | * | T | T | * | * | * | T | * | T |
| 10470 | * | T | T | * | * | * | T | * | T |
| 11598 | * | T | T | * | * | * | F | F | F |
| 11599 | * | T | T | * | * | * | T | * | T |
| 11600 | * | T | T | * | * | * | T | * | T |
| 12707 | * | T | T | * | * | * | F | F | F |
| 12708 | * | T | T | * | * | * | T | * | T |
| 12709 | * | T | T | * | * | * | T | * | T |
| 20418 | * | T | T | * | * | * | F | F | F |
| 20419 | * | T | T | * | * | * | T | * | T |
| 20420 | * | T | T | * | * | * | T | * | T |
| 20421 | * | T | T | * | * | * | T | * | T |
| 20422 | * | T | T | * | * | * | T | * | T |
| 20423 | * | T | T | * | * | * | T | * | T |
| 20424 | * | T | T | * | * | * | T | * | T |
| 28112 | * | T | T | * | * | * | F | F | F |
| 28113 | * | T | T | * | * | * | T | * | T |
| 28114 | * | T | T | * | * | * | T | * | T |
| 28115 | * | T | T | * | * | * | T | * | T |
| 28116 | * | T | T | * | * | * | T | * | T |
| 28117 | * | T | T | * | * | * | T | * | T |
| 28118 | * | T | T | * | * | * | T | * | T |
| 34018 | * | T | T | * | * | * | F | F | F |
| 34019 | * | T | T | * | * | * | T | * | T |
| 34020 | * | T | T | * | * | * | T | * | T |
| 34021 | * | T | T | * | * | * | T | * | T |
| 39956 | * | T | T | * | * | * | F | F | F |
| 39957 | * | T | T | * | * | * | T | * | T |
| 39958 | * | T | T | * | * | * | T | * | T |
| 39959 | * | T | T | * | * | * | T | * | T |
| 42825 | * | T | T | * | * | * | F | F | F |
| 42826 | * | T | T | * | * | * | F | F | F |
| 42827 | * | T | T | * | * | * | T | * | T |
| 42828 | * | T | T | * | * | * | T | * | T |
| 42829 | * | T | T | * | * | * | T | * | T |
| 42830 | * | T | T | * | * | * | T | * | T |
| 45987 | * | T | T | * | * | * | F | F | F |
| 45988 | * | T | T | * | * | * | F | F | F |
| 45989 | * | T | T | * | * | * | T | * | T |
| 45990 | * | T | T | * | * | * | T | * | T |
| 45991 | * | T | T | * | * | * | T | * | T |
| 45992 | * | T | T | * | * | * | T | * | T |
| 45993 | * | T | T | * | * | * | T | * | T |
| 45994 | * | T | T | * | * | * | T | * | T |
| 49345 | * | T | T | * | * | * | F | F | F |
| 49346 | * | T | T | * | * | * | F | F | F |
| 49347 | * | T | T | * | * | * | T | * | T |
| 49348 | * | T | T | * | * | * | T | * | T |
| 49349 | * | T | T | * | * | * | T | * | T |
| 49350 | * | T | T | * | * | * | T | * | T |
| 52365 | * | T | T | * | * | * | F | F | F |
| 52366 | * | T | T | * | * | * | F | F | F |
| 52367 | * | T | T | * | * | * | T | * | T |
| 52368 | * | T | T | * | * | * | T | * | T |
| 52369 | * | T | T | * | * | * | T | * | T |
| 52370 | * | T | T | * | * | * | T | * | T |
| 62234 | * | T | T | * | * | * | F | F | F |
| 62235 | * | T | T | * | * | * | T | * | T |
| 62236 | * | T | T | * | * | * | T | * | T |
| 62237 | * | T | T | * | * | * | T | * | T |
| 62238 | * | T | T | * | * | * | T | * | T |
| 62239 | * | T | T | * | * | * | T | * | T |
| 62240 | * | T | T | * | * | * | T | * | T |
| 72006 | * | T | T | * | * | * | F | F | F |
| 72007 | * | T | T | * | * | * | T | * | T |
| 72008 | * | T | T | * | * | * | T | * | T |
| 72009 | * | T | T | * | * | * | T | * | T |
| 72010 | * | T | T | * | * | * | T | * | T |
| 72011 | * | T | T | * | * | * | T | * | T |
| 72012 | * | T | T | * | * | * | T | * | T |
| 75393 | * | T | T | * | * | * | F | F | F |
| 75394 | * | T | T | * | * | * | T | * | T |
| 75395 | * | T | T | * | * | * | T | * | T |
| 75396 | * | T | T | * | * | * | T | * | T |
| 75397 | * | T | T | * | * | * | T | * | T |
| 75398 | * | T | T | * | * | * | T | * | T |
| 75399 | * | T | T | * | * | * | T | * | T |
| 75400 | * | T | T | * | * | * | T | * | T |
| 75401 | * | T | T | * | * | * | T | * | T |
| 75402 | * | T | T | * | * | * | T | * | T |
| 75403 | * | T | T | * | * | * | T | * | T |
| 75404 | * | T | T | * | * | * | T | * | T |
| 75405 | * | T | T | * | * | * | T | * | T |
| 78868 | * | T | T | * | * | * | F | F | F |
| 78869 | * | T | T | * | * | * | T | * | T |
| 78870 | * | T | T | * | * | * | T | * | T |
| 78871 | * | T | T | * | * | * | T | * | T |
| 78872 | * | T | T | * | * | * | T | * | T |
| 78873 | * | T | T | * | * | * | T | * | T |
| 78874 | * | T | T | * | * | * | T | * | T |
| 78875 | * | T | T | * | * | * | T | * | T |
| 78876 | * | T | T | * | * | * | T | * | T |
| 78877 | * | T | T | * | * | * | T | * | T |
| 78878 | * | T | T | * | * | * | T | * | T |
| 78879 | * | T | T | * | * | * | T | * | T |
| 78880 | * | T | T | * | * | * | T | * | T |
| 80454 | * | T | T | * | * | * | T | * | T |
| 80455 | * | T | T | * | * | * | T | * | T |
| 81682 | * | T | T | * | * | * | F | F | F |
| 81683 | * | T | T | * | * | * | T | * | T |
| 81684 | * | T | T | * | * | * | T | * | T |
| 82841 | * | T | T | * | * | * | F | F | F |
| 82842 | * | T | T | * | * | * | T | * | T |
| 82843 | * | T | T | * | * | * | T | * | T |
| 83931 | * | T | T | * | * | * | F | F | F |
| 83932 | * | T | T | * | * | * | T | * | T |
| 83933 | * | T | T | * | * | * | T | * | T |
| 85220 | * | T | T | * | * | * | F | F | F |
| 85221 | * | T | T | * | * | * | T | * | T |
| 85222 | * | T | T | * | * | * | T | * | T |
| 87298 | * | T | T | * | * | * | F | F | F |
| 87299 | * | T | T | * | * | * | T | * | T |
| 87300 | * | T | T | * | * | * | T | * | T |
| 87301 | * | T | T | * | * | * | T | * | T |
| 87302 | * | T | T | * | * | * | T | * | T |
| 87303 | * | T | T | * | * | * | T | * | T |
| 87304 | * | T | T | * | * | * | T | * | T |
| 87305 | * | T | T | * | * | * | T | * | T |
| 88542 | * | T | T | * | * | * | F | F | F |
| 88543 | * | T | T | * | * | * | T | * | T |
| 90513 | * | T | T | * | * | * | F | F | F |
| 90514 | * | T | T | * | * | * | T | * | T |
| 90515 | * | T | T | * | * | * | T | * | T |
| 90516 | * | T | T | * | * | * | T | * | T |
| 90517 | * | T | T | * | * | * | T | * | T |
| 90518 | * | T | T | * | * | * | T | * | T |
| 90519 | * | T | T | * | * | * | T | * | T |
| 92001 | * | T | T | * | * | * | F | F | F |
| 92002 | * | T | T | * | * | * | T | * | T |
| 92003 | * | T | T | * | * | * | T | * | T |
| 92004 | * | T | T | * | * | * | T | * | T |
| 110902 | * | T | T | * | * | * | F | F | F |
| 110903 | * | T | T | * | * | * | T | * | T |
| 110904 | * | T | T | * | * | * | T | * | T |
| 110905 | * | T | T | * | * | * | T | * | T |
| 110906 | * | T | T | * | * | * | T | * | T |
| 110907 | * | T | T | * | * | * | T | * | T |
| 129765 | * | T | T | * | * | * | F | F | F |
| 129766 | * | T | T | * | * | * | T | * | T |
| 129767 | * | T | T | * | * | * | T | * | T |
| 129768 | * | T | T | * | * | * | T | * | T |
| 129769 | * | T | T | * | * | * | T | * | T |
| 129770 | * | T | T | * | * | * | T | * | T |
| 130935 | * | T | T | * | * | * | F | F | F |
| 132180 | * | T | T | * | * | * | F | F | F |
| 133474 | * | T | T | * | * | * | F | F | F |
Independent-effect pairs
All 8 conditions live in realloc — 8 br_if
c0(branch5983): DEAD view gap →c1(branch5984): GAP view gap →c2(branch5985): GAP view gap →c3(branch5986): DEAD view gap →c4(branch5987): DEAD view gap →c5(branch5988): DEAD view gap →c6(branch5989): PROVED — pair rows2869,2871(masking)c7(branch5990): GAP view gap →