Example: provenance_basic_auto_yx.c

up: index
prev: provenance_basic_auto_xy.c
next: cheri_03_ii.c

1
2
3
4
5
6
7
8
9
10
11
12

    #include <stdio.h>
    #include <string.h> 
    int main() {
      int y=2, x=1;
      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]

Experimental data (what does this mean?) 



cerberus-concrete-PVI Addresses: p=(@6, 0x50) q=(@5, 0x48)


cerberus-concrete-PNVI Addresses: p=(@6, 0x50) q=(@5, 0x48)


gcc-8.1-O0 Addresses: p=0x7fffffffe73c q=0x7fffffffe73c
x=1 y=11 *p=11 *q=11


gcc-8.1-O2 Addresses: p=0x7fffffffe730 q=0x7fffffffe728


gcc-8.1-O3 Addresses: p=0x7fffffffe730 q=0x7fffffffe728


gcc-8.1-O2-no-strict-aliasing Addresses: p=0x7fffffffe700 q=0x7fffffffe6f8


gcc-8.1-O3-no-strict-aliasing Addresses: p=0x7fffffffe700 q=0x7fffffffe6f8


clang-6.0-O0 Addresses: p=0x7fffffffe728 q=0x7fffffffe728
x=1 y=11 *p=11 *q=11


clang-6.0-O2 Addresses: p=0x7fffffffe724 q=0x7fffffffe724
x=1 y=11 *p=11 *q=11


clang-6.0-O3 Addresses: p=0x7fffffffe724 q=0x7fffffffe724
x=1 y=11 *p=11 *q=11


clang-6.0-O2-no-strict-aliasing Addresses: p=0x7fffffffe704 q=0x7fffffffe704
x=1 y=11 *p=11 *q=11


clang-6.0-O3-no-strict-aliasing Addresses: p=0x7fffffffe704 q=0x7fffffffe704
x=1 y=11 *p=11 *q=11


clang-6.0-UBSAN Addresses: p=0x7fffffffe724 q=0x7fffffffe724
x=1 y=11 *p=11 *q=11
provenance_basic_auto_yx.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_yx.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=0x7fffffffe694 q=0x7fffffffe680


clang-6.0-MSAN Addresses: p=0x7fffffffe704 q=0x7fffffffe704
x=1 y=11 *p=11 *q=11


icc-19-O0 Addresses: p=0x7fffffffe708 q=0x7fffffffe700


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=0x7fffffffe6e0 q=0x7fffffffe6d8


compcert-3.4-O Addresses: p=0x7fffffffe6e0 q=0x7fffffffe6d8


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_yx.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_yx.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_yx.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_yx.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_yx.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_yx.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