| A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
1 | test | allowed behaviour | observed behaviour | sound w.r.t P*VI? (relying on UB or ND?) | |||||||||||||
2 | cerb (simple alloc) | gcc-8.1 | clang-6 | icc-19 | compcert-3.4 | RV-match | RV-match (wrt ISO C11) | ||||||||||
3 | test family | PVI | PNVI | PVI = PNVI ? | PVI | PNVI | PVI | PNVI | PVI | PNVI | PVI | PNVI | PVI | PNVI | |||
4 | 1 | provenance_basic_global_xy.c | UB | UB | yes | UB | UB | y (n) | y (n) | y (n) | y (n) | y (y for O2+) | y (y for O2+) | y (n) | y (n) | UB | yes |
5 | provenance_basic_global_yx.c | UB | UB | yes | not triggered | not triggered | y (y for O2+) | y (y for O2+) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | UB | yes | |
6 | provenance_basic_auto_xy.c | UB | UB | yes | UB | UB | y (n) | y (n) | y (n) | y (n) | y (y for O2+) | y (y for O2+) | y (n) | y (n) | UB | yes | |
7 | provenance_basic_auto_yx.c | UB | UB | yes | not triggered | not triggered | y (n) | y (n) | y (n) | y (n) | y (y for O2+) | y (y for O2+) | y (n) | y (n) | UB | yes | |
8 | 2 | cheri_03_ii.c | defined | defined | yes | defined | defined | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | UB | yes |
9 | 3 | pointer_offset_from_ptr_subtraction_global_xy.c | UB (ptrdiff) | UB (ptrdiff) | yes | UB (ptrdiff) | UB (ptrdiff) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | UB | yes |
10 | pointer_offset_from_ptr_subtraction_global_yx.c | UB (ptrdiff) | UB (ptrdiff) | yes | UB (ptrdiff) | UB (ptrdiff) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | UB | yes | |
11 | pointer_offset_from_ptr_subtraction_auto_xy.c | UB (ptrdiff) | UB (ptrdiff) | yes | UB (ptrdiff) | UB (ptrdiff) | y (n) | y (n) | y (n) | y (n) | y (y for O2+) | y (y for O2+) | y (n) | y (n) | UB | yes | |
12 | pointer_offset_from_ptr_subtraction_auto_yx.c | UB (ptrdiff) | UB (ptrdiff) | yes | UB (ptrdiff) | UB (ptrdiff) | y (n) | y (n) | y (n) | y (n) | y (y for O2+) | y (y for O2+) | y (n) | y (n) | UB | yes | |
13 | 4 | provenance_equality_global_xy.c | defined ND | defined ND | yes | defined ND (triggered) | defined ND (triggered) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | unspecified | yes |
14 | provenance_equality_global_yx.c | defined ND | defined ND | yes | not triggered | not triggered | y (y for O2+) | y (y for O2+) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | unspecified | yes | |
15 | provenance_equality_auto_xy.c | defined ND | defined ND | yes | defined ND (triggered) | defined ND (triggered) | y (y for O2+) | y (y for O2+) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | unspecified | yes | |
16 | provenance_equality_auto_yx.c | defined ND | defined ND | yes | not triggered | not triggered | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | unspecified | yes | |
17 | provenance_equality_global_fn_xy.c | defined ND | defined ND | yes | defined ND (triggered) | defined ND (triggered) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | unspecified | yes | |
18 | provenance_equality_global_fn_yx.c | defined ND | defined ND | yes | not triggered | not triggered | y (y for O2+) | y (y for O2+) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | unspecified | yes | |
19 | 5 | provenance_roundtrip_via_intptr_t.c | defined | defined | yes | defined | defined | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | warn impl-def | yes |
20 | 6 | provenance_basic_using_uintptr_t_global_xy.c | UB | defined | no | UB | defined | y (n) | y (n) | y (n) | y (n) | y (y for O2+) | n (y) | y (n) | y (n) | UB | yes |
21 | provenance_basic_using_uintptr_t_global_yx.c | UB | defined | no | not triggered | not triggered | y (y for O2+) | n (y) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | UB | yes | |
22 | provenance_basic_using_uintptr_t_auto_xy.c | UB | defined | no | UB | defined | y (n) | y (n) | y (n) | y (n) | y (y for O2+) | n (y) | y (n) | y (n) | UB | yes | |
23 | provenance_basic_using_uintptr_t_auto_yx.c | UB | defined | no | not triggered | not triggered | y (n) | y (n) | y (n) | y (n) | y (y for O2+) | n (y) | y (n) | y (n) | UB | yes | |
24 | 7 | pointer_offset_from_int_subtraction_global_xy.c | UB | defined | no | UB | defined (triggered) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | UB | yes, but claims "pointer diff" in integer world is UB + gives some UB in stdlib header (memcmp) |
25 | pointer_offset_from_int_subtraction_global_yx.c | UB | defined | no | UB | defined (triggered) | y (n) | y (n) | y(n) | y(n) | y(n) | y(n) | y (n) | y (n) | UB | yes, but claims "pointer diff" in integer world is UB + gives some UB in stdlib header (memcmp) | |
26 | pointer_offset_from_int_subtraction_auto_xy.c | UB | defined | no | UB | defined (triggered) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | UB | yes, but claims "pointer diff" in integer world is UB + gives some UB in stdlib header (memcmp) | |
27 | pointer_offset_from_int_subtraction_auto_yx.c | UB | defined | no | UB | defined (triggered) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | UB | yes, but claims "pointer diff" in integer world is UB + gives some UB in stdlib header (memcmp) | |
28 | 8 | pointer_offset_xor_global.c | UB | defined | no | UB | defined | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | UB | yes, but claims "r" is a null pointer |
29 | pointer_offset_xor_auto.c | UB | defined | no | UB | defined | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | UB | yes, but claims "r" is a null pointer | |
30 | 9 | provenance_tag_bits_via_uintptr_t_1.c | defined | defined | yes | defined | defined | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | warn impl-def | yes |
31 | 10 | pointer_arith_algebraic_properties_2_global.c | defined | defined | yes | defined | defined | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | warn impl-def | yes |
32 | 11 | pointer_arith_algebraic_properties_3_global.c | UB | defined | no | UB | defined | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | UB | yes |
33 | 12 | pointer_copy_memcpy.c | defined | defined | yes | defined | defined | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | defined | yes |
34 | 13 | pointer_copy_user_dataflow_direct_bytewise.c | defined | defined | yes | defined | defined | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | defined | yes |
35 | 14 | pointer_copy_user_ctrlflow_bytewise.c | UB | defined | no | UB | defined | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | UB | yes |
36 | 15 | pointer_copy_user_ctrlflow_bitwise.c | UB | defined | no | UB | defined | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | impl-def, followed by segfault of kcc | NO: segfault before giving an UB |
37 | 16 | provenance_equality_uintptr_t_global_xy.c | defined | defined | yes | defined | defined | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | unspecified | should be implementation-defined not unspecified value or behaviour |
38 | provenance_equality_uintptr_t_global_yx.c | defined | defined | yes | defined | defined | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | unspecified | should be implementation-defined not unspecified value or behaviour | |
39 | provenance_equality_uintptr_t_auto_xy.c | defined | defined | yes | defined | defined | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | unspecified | should be implementation-defined not unspecified value or behaviour | |
40 | provenance_equality_uintptr_t_auto_yx.c | defined | defined | yes | defined | defined | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | unspecified | should be implementation-defined not unspecified value or behaviour | |
41 | 17 | provenance_union_punning_2_global_xy.c | UB | defined | no | UB | defined | y (n) | y (n) | y (n) | y (n) | y (y for O2+) | n (y) | y (n) | y (n) | UB | yes |
42 | provenance_union_punning_2_global_yx.c | UB | defined | no | not triggered | not triggered | y (y for O2+) | n (y) | y (n) | y (n) | y (n) | y (n) | y (n) | y (n) | UB | yes | |
43 | provenance_union_punning_2_auto_xy.c | UB | defined | no | UB | defined | y (n) | y (n) | y (n) | y (n) | y (y for O2+) | n (y) | y (n) | y (n) | UB | yes | |
44 | provenance_union_punning_2_auto_yx.c | UB | defined | no | not triggered | not triggered | y (n) | y (n) | y (n) | y (n) | y (y for O2+) | n (y) | y (n) | y (n) | UB | yes | |
45 | 18 | provenance_via_io_percentp_global.c | filesystem and scanf() are not currently supported by Cerberus | NO OPT | NO OPT | NO OPT | NO OPT | NO OPT | NO OPT | NO OPT | NO OPT | UB ("execution failed" but not segfault) | yes | ||||
46 | 19 | provenance_via_io_bytewise_global.c | NO OPT | NO OPT | NO OPT | NO OPT | NO OPT | NO OPT | NO OPT | NO OPT | UB | yes | |||||
47 | 20 | provenance_via_io_uintptr_t_global.c | UB | ||||||||||||||
48 | 21 | pointer_from_integer_1pg.c | UB | UB | yes | UB | UB | y (y for O0+) | y (y for O0+) | y (y for O2+) | y (y for O2+) | y (y for O2+) | y (y for O2+) | y (y for O) | y (y for O) | can't get the right address, so no data | |
49 | 22 | pointer_from_integer_1ig.c | UB | defined | no | UB | defined | y (y for O2+) | n (y) | y (y for O2+) | n (y) | y (y for O2+) | n (y) | y (y for O) | n (y) | can't get the right address, so no data | |
50 | 23 | pointer_from_integer_1p.c | UB | UB | yes | UB | UB | can't test with charon | impl-def, followed by segfault of kcc | NO: segfault before giving an UB | |||||||
51 | 24 | pointer_from_integer_1i.c | UB | UB | yes | UB | defined (only one allocator) | can't test with charon | impl-def, followed by segfault of kcc | NO: segfault before giving an UB | |||||||
52 | 25 | pointer_from_integer_2.c | UB | UB | yes | UB | defined (only one allocator) | can't test with charon | impl-def, followed by segfault of kcc | NO: segfault before giving an UB | |||||||
53 | 26 | pointer_from_integer_2g.c | UB | defined | no | UB | defined | y (n) | y (n) | y (y for O2+) | n (y) | y (n) | y (n) | y (y for O) | n (y) | can't get the right address, so no data | |
54 | 27 | provenance_lost_escape_1.c | defined | defined | yes | defined | defined | y (n) | y (n) | y (n) | y (n) | y (n) | n (y) | y (n) | y (n) | UB + unknown error | maybe a bug, but warn about that possiblity |