Example: provenance_basic_global_xy.c#include <stdio.h>
#include <string.h>
int x=1, y=2;
int main() {
int *p = &x + 1;
int *q = &y;
printf("Addresses: p=%p q=%p\n",(void*)p,(void*)q);
if (memcmp(&p, &q, sizeof(p)) == 0) {
*p = 11; // does this have undefined behaviour?
printf("x=%d y=%d *p=%d *q=%d\n",x,y,*p,*q);
}
return 0;
}
[link to test in Cerberus and Compiler Explorer]
Experimental data (what does this mean?)
| gcc-8.1-O0 | | Addresses: p=0x600a2c q=0x600a2c
x=1 y=11 *p=11 *q=11
|
| gcc-8.1-O2 | | Addresses: p=0x6009c8 q=0x6009c0
|
| gcc-8.1-O3 | | Addresses: p=0x6009c8 q=0x6009c0
|
| gcc-8.1-O2-no-strict-aliasing | | Addresses: p=0x6009c8 q=0x6009c0
|
| gcc-8.1-O3-no-strict-aliasing | | Addresses: p=0x6009c8 q=0x6009c0
|
| clang-6.0-O0 | | Addresses: p=0x60103c q=0x60103c
x=1 y=11 *p=11 *q=11
|
| clang-6.0-O2 | | Addresses: p=0x60103c q=0x60103c
x=1 y=11 *p=11 *q=11
|
| clang-6.0-O3 | | Addresses: p=0x60103c q=0x60103c
x=1 y=11 *p=11 *q=11
|
| clang-6.0-O2-no-strict-aliasing | | Addresses: p=0x60103c q=0x60103c
x=1 y=11 *p=11 *q=11
|
| clang-6.0-O3-no-strict-aliasing | | Addresses: p=0x60103c q=0x60103c
x=1 y=11 *p=11 *q=11
|
| clang-6.0-UBSAN | | Addresses: p=0x631b54 q=0x631b54
x=1 y=11 *p=11 *q=11
provenance_basic_global_xy.c:9:5: runtime error: store to address 0x000000631b54 with insufficient space for an object of type 'int'
0x000000631b54: note: pointer points here
01 00 00 00 02 00 00 00 00 00 00 00 00 00 00 00 24 7f 42 00 00 00 00 00 09 00 00 00 ff ff ff ff
^
provenance_basic_global_xy.c:10:42: runtime error: load of address 0x000000631b54 with insufficient space for an object of type 'int'
0x000000631b54: note: pointer points here
01 00 00 00 0b 00 00 00 00 00 00 00 00 00 00 00 24 7f 42 00 00 00 00 00 09 00 00 00 ff ff ff ff
^
|
| clang-6.0-ASAN | | Addresses: p=0x716b64 q=0x716ba0
|
| clang-6.0-MSAN | | Addresses: p=0x6b7af4 q=0x6b7af4
x=1 y=11 *p=11 *q=11
|
| icc-19-O0 | | Addresses: p=0x600b5c q=0x600b5c
x=1 y=11 *p=11 *q=11
|
| icc-19-O2 | | Addresses: p=0x6046c4 q=0x6046c4
x=1 y=2 *p=11 *q=11
|
| icc-19-O3 | | Addresses: p=0x6046c4 q=0x6046c4
x=1 y=2 *p=11 *q=11
|
| icc-19-O2-no-strict-aliasing | | Addresses: p=0x6046c4 q=0x6046c4
x=1 y=2 *p=11 *q=11
|
| icc-19-O3-no-strict-aliasing | | Addresses: p=0x6046c4 q=0x6046c4
x=1 y=2 *p=11 *q=11
|
| cerberus-concrete | | BEGIN EXEC[0]
Killed {msg: MerrAccess Store [provenance_basic_global_xy.c:9:5-12] OutOfBoundPtr}
END EXEC[0]
Time spent: 0.037673 seconds
|
| cerberus-symbolic | | BEGIN EXEC[0]
Undefined [other_location(Core parser)]{id: [DUMMY(rev_listFromStr_aux)]}
END EXEC[0]
Time spent: 0.075464 seconds
|
| gcc-4.9-shadowprov | | Addresses: p=0x415150 q=0x415148
|
| CHERI:MIPS-O0 | | Addresses: p=0x30024 q=0x30024
x=1 y=11 *p=11 *q=11
|
| CHERI:MIPS-O2 | | Addresses: p=0x30024 q=0x30024
x=1 y=11 *p=11 *q=11
|
| CHERI:MIPS-O2-no-strict-aliasing | | Addresses: p=0x30024 q=0x30024
x=1 y=11 *p=11 *q=11
|
| CHERI:CHERI-O0-uintcap-addr-exact-equals | | Addresses: p=0x120020014 q=0x120020014
|
| CHERI:CHERI-O2-uintcap-addr-exact-equals | | Addresses: p=0x120020014 q=0x120020014
|
| CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr-exact-equals | | Addresses: p=0x120020014 q=0x120020014
|
| CHERI:CHERI-O0-uintcap-offset-exact-equals | | Addresses: p=0x120020014 q=0x120020014
|
| CHERI:CHERI-O2-uintcap-offset-exact-equals | | Addresses: p=0x120020014 q=0x120020014
|
| CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset-exact-equals | | Addresses: p=0x120020014 q=0x120020014
|
| CHERI:CHERI-O0-uintcap-addr | | Addresses: p=0x120020014 q=0x120020014
|
| CHERI:CHERI-O2-uintcap-addr | | Addresses: p=0x120020014 q=0x120020014
|
| CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr | | Addresses: p=0x120020014 q=0x120020014
|
| CHERI:CHERI-O0-uintcap-offset | | Addresses: p=0x120020014 q=0x120020014
|
| CHERI:CHERI-O2-uintcap-offset | | Addresses: p=0x120020014 q=0x120020014
|
| CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset | | Addresses: p=0x120020014 q=0x120020014
|
| RV-Match | | Addresses: p=(nil) q=(nil)
x=1 y=2 *p=0 *q=2
Comparison of unspecified value:
> in memcmp at /opt/rv-match/c-semantics/x86_64-linux-gcc-glibc/src/string.c:180:13
in main at provenance_basic_global_xy.c:8:3
Unspecified value or behavior (USP-CERL7):
see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9
see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1
Dereferencing a pointer past the end of an array:
> in main at provenance_basic_global_xy.c:9:5
Undefined behavior (UB-CER4):
see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6
see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2
see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C
see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C
see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C
see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18
see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1
Trying to write outside the bounds of an object:
> in main at provenance_basic_global_xy.c:9:5
Undefined behavior (UB-EIO2):
see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6
see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2
see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C
see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C
see CERT-C section MEM35-C http://rvdoc.org/CERT-C/MEM35-C
see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C
see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1
Dereferencing a pointer past the end of an array:
> in main at provenance_basic_global_xy.c:10:5
Undefined behavior (UB-CER4):
see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6
see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2
see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C
see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C
see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C
see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18
see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1
Reading outside the bounds of an object:
> in main at provenance_basic_global_xy.c:10:5
Undefined behavior (UB-EIO7):
see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1
see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2
see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C
see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C
see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C
see CERT-C section STR32-C http://rvdoc.org/CERT-C/STR32-C
see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1
|
| ch2o | | Fatal error: exception Failure("parse_printf")
Raised at file "pervasives.ml", line 30, characters 22-33
Called from file "list.ml", line 55, characters 20-23
Called from file "list.ml", line 55, characters 32-39
Called from file "list.ml", line 55, characters 32-39
Called from file "list.ml", line 55, characters 32-39
Called from file "list.ml", line 55, characters 32-39
Called from file "list.ml", line 55, characters 32-39
Called from file "list.ml", line 55, characters 32-39
Called from file "list.ml", line 55, characters 32-39
|
| compcert-3.2 | | Addresses: p=0x601044 q=0x601044
x=1 y=11 *p=11 *q=11
|
| compcert-3.2-O | | Addresses: p=0x601044 q=0x601044
x=1 y=11 *p=11 *q=11
|
| compcert-3.2-interp | | Time 0: calling main()
--[step_internal_function]-->
Time 1: in function main, statement
p = &x + 1;
q = &y;
printf(__stringlit_1, (void *) p, (void *) q);
if (memcmp(&p, &q, sizeof(int *)) == 0) {
*p = 11;
printf(__stringlit_2, x, y, *., *.);
}
return 0;
return 0;
--[step_seq]-->
Time 2: in function main, statement
p = &x + 1;
q = &y;
printf(__stringlit_1, (void *) p, (void *) q);
if (memcmp(&p, &q, sizeof(int *)) == 0) {
*p = 11;
printf(__stringlit_2, x, y, *., *.);
}
return 0;
--[step_seq]-->
Time 3: in function main, statement p = &x + 1;
--[step_do_1]-->
Time 4: in function main, expression p = &x + 1
--[red_var_local]-->
Time 5: in function main, expression <loc p> = &x + 1
--[red_var_global]-->
Time 6: in function main, expression <loc p> = &<loc x> + 1
--[red_addrof]-->
Time 7: in function main, expression <loc p> = <ptr x> + 1
--[red_binop]-->
Time 8: in function main, expression <loc p> = <ptr x+4>
--[red_assign]-->
Time 9: in function main, expression <ptr x+4>
--[step_do_2]-->
Time 10: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 11: in function main, statement
q = &y;
printf(__stringlit_1, (void *) p, (void *) q);
if (memcmp(&p, &q, sizeof(int *)) == 0) {
*p = 11;
printf(__stringlit_2, x, y, *., *.);
}
return 0;
--[step_seq]-->
Time 12: in function main, statement q = &y;
--[step_do_1]-->
Time 13: in function main, expression q = &y
--[red_var_local]-->
Time 14: in function main, expression <loc q> = &y
--[red_var_global]-->
Time 15: in function main, expression <loc q> = &<loc y>
--[red_addrof]-->
Time 16: in function main, expression <loc q> = <ptr y>
--[red_assign]-->
Time 17: in function main, expression <ptr y>
--[step_do_2]-->
Time 18: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 19: in function main, statement
printf(__stringlit_1, (void *) p, (void *) q);
if (memcmp(&p, &q, sizeof(int *)) == 0) {
*p = 11;
printf(__stringlit_2, x, y, *., *.);
}
return 0;
--[step_seq]-->
Time 20: in function main, statement
printf(__stringlit_1, (void *) p, (void *) q);
--[step_do_1]-->
Time 21: in function main, expression
printf(__stringlit_1, (void *) p, (void *) q)
--[red_var_global]-->
Time 22: in function main, expression
printf(<loc __stringlit_1>, (void *) p, (void *) q)
--[red_rvalof]-->
Time 23: in function main, expression
printf(<ptr __stringlit_1>, (void *) p, (void *) q)
--[red_var_local]-->
Time 24: in function main, expression
printf(<ptr __stringlit_1>, (void *) <loc p>, (void *) q)
--[red_rvalof]-->
Time 25: in function main, expression
printf(<ptr __stringlit_1>, (void *) <ptr x+4>, (void *) q)
--[red_cast]-->
Time 26: in function main, expression
printf(<ptr __stringlit_1>, <ptr x+4>, (void *) q)
--[red_var_local]-->
Time 27: in function main, expression
printf(<ptr __stringlit_1>, <ptr x+4>, (void *) <loc q>)
--[red_rvalof]-->
Time 28: in function main, expression
printf(<ptr __stringlit_1>, <ptr x+4>, (void *) <ptr y>)
--[red_cast]-->
Time 29: in function main, expression
printf(<ptr __stringlit_1>, <ptr x+4>, <ptr y>)
Addresses: p=<56+4> q=<57+0>
Time 29: observable event:
extcall printf(& __stringlit_1, & x+4,
& y) -> 29
--[red_builtin]-->
Time 30: in function main, expression 29
--[step_do_2]-->
Time 31: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 32: in function main, statement
if (memcmp(&p, &q, sizeof(int *)) == 0) {
*p = 11;
printf(__stringlit_2, x, y, *., *.);
}
return 0;
--[step_seq]-->
Time 33: in function main, statement
if (memcmp(&p, &q, sizeof(int *)) == 0) {
*p = 11;
printf(__stringlit_2, x, y, *., *.);
}
--[step_ifthenelse_1]-->
Time 34: in function main, expression memcmp(&p, &q, sizeof(int *)) == 0
--[red_var_global]-->
Time 35: in function main, expression
<loc memcmp>(&p, &q, sizeof(int *)) == 0
--[red_rvalof]-->
Time 36: in function main, expression
<ptr memcmp>(&p, &q, sizeof(int *)) == 0
--[red_var_local]-->
Time 37: in function main, expression
<ptr memcmp>(&<loc p>, &q, sizeof(int *)) == 0
--[red_addrof]-->
Time 38: in function main, expression
<ptr memcmp>(<ptr p>, &q, sizeof(int *)) == 0
--[red_var_local]-->
Time 39: in function main, expression
<ptr memcmp>(<ptr p>, &<loc q>, sizeof(int *)) == 0
--[red_addrof]-->
Time 40: in function main, expression
<ptr memcmp>(<ptr p>, <ptr q>, sizeof(int *)) == 0
--[red_sizeof]-->
Time 41: in function main, expression <ptr memcmp>(<ptr p>, <ptr q>, 4U) == 0
--[red_call]-->
Time 42: calling memcmp(<ptr>, <ptr>, 4)
Stuck state: calling memcmp(<ptr>, <ptr>, 4)
ERROR: Undefined behavior
In file included from provenance_basic_global_xy.c:1:
In file included from /usr/include/stdio.h:64:
In file included from /usr/include/_stdio.h:68:
/usr/include/sys/cdefs.h:81:2: warning: "Unsupported compiler detected" [-W#warnings]
#warning "Unsupported compiler detected"
^
1 warning generated.
|