Example: cheri_03_ii.c

up: index
prev: provenance_basic_auto_yx.c
next: pointer_offset_from_ptr_subtraction_global_xy.c

1
2
3
4
5
6
7
8
9
10

    #include <stdio.h>
    int main() {
      int x[2];
      int *p = &x[0];
      //is this free of undefined behaviour?
      int *q = p + 11;
      q = q - 10;
      *q = 1;
      printf("x[1]=%i  *q=%i\n",x[1],*q);
    }
[link to run test in Cerberus]

Experimental data (what does this mean?) 



cerberus-concrete-PVI-plain Undefined behaviour: the result of some pointer arithmetic operator was out of bound at other_location(Concrete)


cerberus-concrete-PVI-ae Undefined behaviour: the result of some pointer arithmetic operator was out of bound at other_location(Concrete)


cerberus-concrete-PVI-ae-udi Undefined behaviour: the result of some pointer arithmetic operator was out of bound at other_location(Concrete)


gcc-8.3-O0 x[1]=1  *q=1


gcc-8.3-O2 x[1]=1  *q=1


gcc-8.3-O3 x[1]=1  *q=1


gcc-8.3-O2-no-strict-aliasing x[1]=1  *q=1


gcc-8.3-O3-no-strict-aliasing x[1]=1  *q=1


clang-7.0.1-O0 x[1]=1  *q=1


clang-7.0.1-O2 x[1]=1  *q=1


clang-7.0.1-O3 x[1]=1  *q=1


clang-7.0.1-O2-no-strict-aliasing x[1]=1  *q=1


clang-7.0.1-O3-no-strict-aliasing x[1]=1  *q=1


icc-19-O0 x[1]=1  *q=1


icc-19-O2 x[1]=1  *q=1


icc-19-O3 x[1]=1  *q=1


icc-19-O2-no-strict-aliasing x[1]=1  *q=1


icc-19-O3-no-strict-aliasing x[1]=1  *q=1