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);
      }
    }

[link to run test in Cerberus]

cerberus-concrete-PVI Undefined behaviour: out of bounds pointer at memory store at 9:5-12 cerberus-concrete-PNVI Undefined behaviour: out of bounds pointer at memory store at 9:5-12 gcc-8.1-O0 Addresses: p=0x7fffffffe740 q=0x7fffffffe738 gcc-8.1-O2 Addresses: p=0x7fffffffe72c q=0x7fffffffe72c x=1 y=11 *p=11 *q=11 gcc-8.1-O3 Addresses: p=0x7fffffffe72c q=0x7fffffffe72c x=1 y=11 *p=11 *q=11 gcc-8.1-O2-no-strict-aliasing Addresses: p=0x7fffffffe6fc q=0x7fffffffe6fc x=1 y=11 *p=11 *q=11 gcc-8.1-O3-no-strict-aliasing Addresses: p=0x7fffffffe6fc q=0x7fffffffe6fc x=1 y=11 *p=11 *q=11 clang-6.0-O0 Addresses: p=0x7fffffffe72c q=0x7fffffffe724 clang-6.0-O2 Addresses: p=0x7fffffffe728 q=0x7fffffffe720 clang-6.0-O3 Addresses: p=0x7fffffffe728 q=0x7fffffffe720 clang-6.0-O2-no-strict-aliasing Addresses: p=0x7fffffffe708 q=0x7fffffffe700 clang-6.0-O3-no-strict-aliasing Addresses: p=0x7fffffffe708 q=0x7fffffffe700 clang-6.0-UBSAN Addresses: p=0x7fffffffe724 q=0x7fffffffe724 x=1 y=11 *p=11 *q=11 provenance_basic_auto_xy.c:9:5: runtime error: store to address 0x7fffffffe724 with insufficient space for an object of type 'int' 0x7fffffffe724: 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 58 ee f6 ff 7f 00 00 ^ provenance_basic_auto_xy.c:10:42: runtime error: load of address 0x7fffffffe724 with insufficient space for an object of type 'int' 0x7fffffffe724: 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 58 ee f6 ff 7f 00 00 ^ clang-6.0-ASAN Addresses: p=0x7fffffffe684 q=0x7fffffffe690 clang-6.0-MSAN Addresses: p=0x7fffffffe704 q=0x7fffffffe704 x=1 y=11 *p=11 *q=11 icc-19-O0 Addresses: p=0x7fffffffe704 q=0x7fffffffe704 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 compcert-3.4 Addresses: p=0x7fffffffe6dc q=0x7fffffffe6dc x=1 y=11 *p=11 *q=11 compcert-3.4-O Addresses: p=0x7fffffffe6dc q=0x7fffffffe6dc x=1 y=11 *p=11 *q=11 kcc-1.0 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/profiles/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

cerberus-concrete-PVI		Undefined behaviour: out of bounds pointer at memory store at 9:5-12
cerberus-concrete-PNVI		Undefined behaviour: out of bounds pointer at memory store at 9:5-12
gcc-8.1-O0		Addresses: p=0x7fffffffe740 q=0x7fffffffe738
gcc-8.1-O2		Addresses: p=0x7fffffffe72c q=0x7fffffffe72c x=1 y=11 p=11 q=11
gcc-8.1-O3		Addresses: p=0x7fffffffe72c q=0x7fffffffe72c x=1 y=11 p=11 q=11
gcc-8.1-O2-no-strict-aliasing		Addresses: p=0x7fffffffe6fc q=0x7fffffffe6fc x=1 y=11 p=11 q=11
gcc-8.1-O3-no-strict-aliasing		Addresses: p=0x7fffffffe6fc q=0x7fffffffe6fc x=1 y=11 p=11 q=11
clang-6.0-O0		Addresses: p=0x7fffffffe72c q=0x7fffffffe724
clang-6.0-O2		Addresses: p=0x7fffffffe728 q=0x7fffffffe720
clang-6.0-O3		Addresses: p=0x7fffffffe728 q=0x7fffffffe720
clang-6.0-O2-no-strict-aliasing		Addresses: p=0x7fffffffe708 q=0x7fffffffe700
clang-6.0-O3-no-strict-aliasing		Addresses: p=0x7fffffffe708 q=0x7fffffffe700
clang-6.0-UBSAN		Addresses: p=0x7fffffffe724 q=0x7fffffffe724 x=1 y=11 p=11 q=11 provenance_basic_auto_xy.c:9:5: runtime error: store to address 0x7fffffffe724 with insufficient space for an object of type 'int' 0x7fffffffe724: 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 58 ee f6 ff 7f 00 00 ^ provenance_basic_auto_xy.c:10:42: runtime error: load of address 0x7fffffffe724 with insufficient space for an object of type 'int' 0x7fffffffe724: 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 58 ee f6 ff 7f 00 00 ^
clang-6.0-ASAN		Addresses: p=0x7fffffffe684 q=0x7fffffffe690
clang-6.0-MSAN		Addresses: p=0x7fffffffe704 q=0x7fffffffe704 x=1 y=11 p=11 q=11
icc-19-O0		Addresses: p=0x7fffffffe704 q=0x7fffffffe704 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
compcert-3.4		Addresses: p=0x7fffffffe6dc q=0x7fffffffe6dc x=1 y=11 p=11 q=11
compcert-3.4-O		Addresses: p=0x7fffffffe6dc q=0x7fffffffe6dc x=1 y=11 p=11 q=11
kcc-1.0		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/profiles/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

Example: provenance_basic_auto_xy.c

Example: `provenance_basic_auto_xy.c`