Example: provenance_basic_global_xy.c

up: index
prev: -
next: provenance_basic_global_yx.c

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

    #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);
      }
    }
[link to run test in Cerberus]

Experimental data (what does this mean?) 



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=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


compcert-3.4 Addresses: p=0x601044 q=0x601044
x=1 y=11 *p=11 *q=11


compcert-3.4-O Addresses: p=0x601044 q=0x601044
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_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