Example: provenance_basic_auto_xy.c#include <stdio.h>
#include <string.h>
int main() {
int x=1, y=2;
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=0x7fff26839290 q=0x7fff26839288
|
| gcc-8.1-O2 | | Addresses: p=0x7ffe5f8cb48c q=0x7ffe5f8cb48c
x=1 y=11 *p=11 *q=11
|
| gcc-8.1-O3 | | Addresses: p=0x7ffc4d5327bc q=0x7ffc4d5327bc
x=1 y=11 *p=11 *q=11
|
| gcc-8.1-O2-no-strict-aliasing | | Addresses: p=0x7fffb51013cc q=0x7fffb51013cc
x=1 y=11 *p=11 *q=11
|
| gcc-8.1-O3-no-strict-aliasing | | Addresses: p=0x7ffe69c2f55c q=0x7ffe69c2f55c
x=1 y=11 *p=11 *q=11
|
| clang-6.0-O0 | | Addresses: p=0x7ffecb93509c q=0x7ffecb935094
|
| clang-6.0-O2 | | Addresses: p=0x7ffedb4fc6d8 q=0x7ffedb4fc6d0
|
| clang-6.0-O3 | | Addresses: p=0x7ffe6ff85ab8 q=0x7ffe6ff85ab0
|
| clang-6.0-O2-no-strict-aliasing | | Addresses: p=0x7fff310b9228 q=0x7fff310b9220
|
| clang-6.0-O3-no-strict-aliasing | | Addresses: p=0x7fff14368a08 q=0x7fff14368a00
|
| clang-6.0-UBSAN | | Addresses: p=0x7ffe7c5dd224 q=0x7ffe7c5dd224
x=1 y=11 *p=11 *q=11
provenance_basic_auto_xy.c:9:5: runtime error: store to address 0x7ffe7c5dd224 with insufficient space for an object of type 'int'
0x7ffe7c5dd224: note: pointer points here
01 00 00 00 02 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 30 78 5c 4f 20 7f 00 00
^
provenance_basic_auto_xy.c:10:42: runtime error: load of address 0x7ffe7c5dd224 with insufficient space for an object of type 'int'
0x7ffe7c5dd224: note: pointer points here
01 00 00 00 0b 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 30 78 5c 4f 20 7f 00 00
^
|
| clang-6.0-ASAN | | Addresses: p=0x7ffc54d84724 q=0x7ffc54d84730
|
| clang-6.0-MSAN | | Addresses: p=0x7fff7a775fa4 q=0x7fff7a775fa4
x=1 y=11 *p=11 *q=11
|
| icc-19-O0 | | Addresses: p=0x7ffcb73d3ab4 q=0x7ffcb73d3ab4
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_auto_xy.c:9:5-12] OutOfBoundPtr}
END EXEC[0]
Time spent: 0.048945 seconds
|
| cerberus-symbolic | | BEGIN EXEC[0]
Undefined [other_location(Core parser)]{id: [DUMMY(rev_listFromStr_aux)]}
END EXEC[0]
Time spent: 0.078668 seconds
|
| gcc-4.9-shadowprov | | Addresses: p=0x7ffcde1137ec q=0x7ffcde113818
|
| CHERI:MIPS-O0 | | Addresses: p=0x7fffffe9f4 q=0x7fffffe9ec
|
| CHERI:MIPS-O2 | | Addresses: p=0x7fffffe9e8 q=0x7fffffe9e0
|
| CHERI:MIPS-O2-no-strict-aliasing | | Addresses: p=0x7fffffe9c8 q=0x7fffffe9c0
|
| CHERI:CHERI-O0-uintcap-addr-exact-equals | | Addresses: p=0x7fffffe48c q=0x7fffffe484
|
| CHERI:CHERI-O2-uintcap-addr-exact-equals | | Addresses: p=0x7fffffe430 q=0x7fffffe428
|
| CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr-exact-equals | | Addresses: p=0x7fffffe410 q=0x7fffffe408
|
| CHERI:CHERI-O0-uintcap-offset-exact-equals | | Addresses: p=0x7fffffe48c q=0x7fffffe484
|
| CHERI:CHERI-O2-uintcap-offset-exact-equals | | Addresses: p=0x7fffffe430 q=0x7fffffe428
|
| CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset-exact-equals | | Addresses: p=0x7fffffe410 q=0x7fffffe408
|
| CHERI:CHERI-O0-uintcap-addr | | Addresses: p=0x7fffffe4ac q=0x7fffffe4a4
|
| CHERI:CHERI-O2-uintcap-addr | | Addresses: p=0x7fffffe450 q=0x7fffffe448
|
| CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr | | Addresses: p=0x7fffffe420 q=0x7fffffe418
|
| CHERI:CHERI-O0-uintcap-offset | | Addresses: p=0x7fffffe4ac q=0x7fffffe4a4
|
| CHERI:CHERI-O2-uintcap-offset | | Addresses: p=0x7fffffe450 q=0x7fffffe448
|
| CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset | | Addresses: p=0x7fffffe420 q=0x7fffffe418
|
| 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_auto_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_auto_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_auto_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_auto_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_auto_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
Indeterminate value used in an expression:
> in main at provenance_basic_auto_xy.c:10:5
Undefined behavior (UB-CEE2):
see C11 section 6.2.4 http://rvdoc.org/C11/6.2.4
see C11 section 6.7.9 http://rvdoc.org/C11/6.7.9
see C11 section 6.8 http://rvdoc.org/C11/6.8
see C11 section J.2:1 item 11 http://rvdoc.org/C11/J.2
see CERT-C section EXP33-C http://rvdoc.org/CERT-C/EXP33-C
see MISRA-C section 8.9:1 http://rvdoc.org/MISRA-C/8.9
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
|
| compcert-3.2 | | Addresses: p=0x7ffd1e79a12c q=0x7ffd1e79a12c
x=1 y=11 *p=11 *q=11
|
| compcert-3.2-O | | Addresses: p=0x7ffe74b6fc4c q=0x7ffe74b6fc4c
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
x = 1;
y = 2;
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
x = 1;
y = 2;
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 x = 1;
--[step_do_1]-->
Time 4: in function main, expression x = 1
--[red_var_local]-->
Time 5: in function main, expression <loc x> = 1
--[red_assign]-->
Time 6: in function main, expression 1
--[step_do_2]-->
Time 7: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 8: in function main, statement
y = 2;
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 9: in function main, statement y = 2;
--[step_do_1]-->
Time 10: in function main, expression y = 2
--[red_var_local]-->
Time 11: in function main, expression <loc y> = 2
--[red_assign]-->
Time 12: in function main, expression 2
--[step_do_2]-->
Time 13: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 14: 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 15: in function main, statement p = &x + 1;
--[step_do_1]-->
Time 16: in function main, expression p = &x + 1
--[red_var_local]-->
Time 17: in function main, expression <loc p> = &x + 1
--[red_var_local]-->
Time 18: in function main, expression <loc p> = &<loc x> + 1
--[red_addrof]-->
Time 19: in function main, expression <loc p> = <ptr x> + 1
--[red_binop]-->
Time 20: in function main, expression <loc p> = <ptr x+4>
--[red_assign]-->
Time 21: in function main, expression <ptr x+4>
--[step_do_2]-->
Time 22: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 23: 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 24: in function main, statement q = &y;
--[step_do_1]-->
Time 25: in function main, expression q = &y
--[red_var_local]-->
Time 26: in function main, expression <loc q> = &y
--[red_var_local]-->
Time 27: in function main, expression <loc q> = &<loc y>
--[red_addrof]-->
Time 28: in function main, expression <loc q> = <ptr y>
--[red_assign]-->
Time 29: in function main, expression <ptr y>
--[step_do_2]-->
Time 30: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 31: 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 32: in function main, statement
printf(__stringlit_1, (void *) p, (void *) q);
--[step_do_1]-->
Time 33: in function main, expression
printf(__stringlit_1, (void *) p, (void *) q)
--[red_var_global]-->
Time 34: in function main, expression
printf(<loc __stringlit_1>, (void *) p, (void *) q)
--[red_rvalof]-->
Time 35: in function main, expression
printf(<ptr __stringlit_1>, (void *) p, (void *) q)
--[red_var_local]-->
Time 36: in function main, expression
printf(<ptr __stringlit_1>, (void *) <loc p>, (void *) q)
--[red_rvalof]-->
Time 37: in function main, expression
printf(<ptr __stringlit_1>, (void *) <ptr x+4>, (void *) q)
--[red_cast]-->
Time 38: in function main, expression
printf(<ptr __stringlit_1>, <ptr x+4>, (void *) q)
--[red_var_local]-->
Time 39: in function main, expression
printf(<ptr __stringlit_1>, <ptr x+4>, (void *) <loc q>)
--[red_rvalof]-->
Time 40: in function main, expression
printf(<ptr __stringlit_1>, <ptr x+4>, (void *) <ptr y>)
--[red_cast]-->
Time 41: in function main, expression
printf(<ptr __stringlit_1>, <ptr x+4>, <ptr y>)
Addresses: p=<57+4> q=<58+0>
Stuck state: in function main, expression
printf(<ptr __stringlit_1>, <ptr x+4>, <ptr y>)
Addresses: p=<57+4> q=<58+0>
Stuck subexpression:
printf(<ptr __stringlit_1>, <ptr x+4>, <ptr y>)
ERROR: Undefined behavior
In file included from provenance_basic_auto_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.
|