Example: `provenance_basic_auto_yx.c`

#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);
  }
  return 0;
}

[link to test in Cerberus and Compiler Explorer]

Experimental data (what does this mean?)


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

gcc-8.1-O2   Addresses: p=0x7ffe4660ddf0 q=0x7ffe4660dde8

gcc-8.1-O3   Addresses: p=0x7ffccdf60bf0 q=0x7ffccdf60be8

gcc-8.1-O2-no-strict-aliasing   Addresses: p=0x7ffe0d4f1930 q=0x7ffe0d4f1928

gcc-8.1-O3-no-strict-aliasing   Addresses: p=0x7fff8be1b180 q=0x7fff8be1b178

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

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

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

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

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

clang-6.0-UBSAN   Addresses: p=0x7ffff7e4ef84 q=0x7ffff7e4ef84
x=1 y=11 *p=11 *q=11
provenance_basic_auto_yx.c:9:5: runtime error: store to address 0x7ffff7e4ef84 with insufficient space for an object of type 'int'
0x7ffff7e4ef84: 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 e8 ae 63 bb 7f 00 00
              ^ 
provenance_basic_auto_yx.c:10:42: runtime error: load of address 0x7ffff7e4ef84 with insufficient space for an object of type 'int'
0x7ffff7e4ef84: 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 e8 ae 63 bb 7f 00 00
              ^ 

clang-6.0-ASAN   Addresses: p=0x7fffc9108394 q=0x7fffc9108380

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

icc-19-O0   Addresses: p=0x7ffcef084178 q=0x7ffcef084170

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]
Defined {value: "Specified(0)", stdout: "Addresses: p=<6>:80 q=<5>:72\n", blocked: "false"}
END EXEC[0]
Time spent: 0.048259 seconds

cerberus-symbolic   BEGIN EXEC[0]
Undefined [other_location(Core parser)]{id: [DUMMY(rev_listFromStr_aux)]}
END EXEC[0]
Time spent: 0.072964 seconds

gcc-4.9-shadowprov   Addresses: p=0x7ffc4fc6d91c q=0x7ffc4fc6d948

CHERI:MIPS-O0   Addresses: p=0x7fffffe9f0 q=0x7fffffe9f0
x=1 y=11 *p=11 *q=11

CHERI:MIPS-O2   Addresses: p=0x7fffffe9e4 q=0x7fffffe9e4
x=1 y=11 *p=11 *q=11

CHERI:MIPS-O2-no-strict-aliasing   Addresses: p=0x7fffffe9c4 q=0x7fffffe9c4
x=1 y=11 *p=11 *q=11

CHERI:CHERI-O0-uintcap-addr-exact-equals   Addresses: p=0x7fffffe488 q=0x7fffffe488

CHERI:CHERI-O2-uintcap-addr-exact-equals   Addresses: p=0x7fffffe42c q=0x7fffffe42c

CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr-exact-equals   Addresses: p=0x7fffffe40c q=0x7fffffe40c

CHERI:CHERI-O0-uintcap-offset-exact-equals   Addresses: p=0x7fffffe488 q=0x7fffffe488

CHERI:CHERI-O2-uintcap-offset-exact-equals   Addresses: p=0x7fffffe42c q=0x7fffffe42c

CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset-exact-equals   Addresses: p=0x7fffffe40c q=0x7fffffe40c

CHERI:CHERI-O0-uintcap-addr   Addresses: p=0x7fffffe4a8 q=0x7fffffe4a8

CHERI:CHERI-O2-uintcap-addr   Addresses: p=0x7fffffe44c q=0x7fffffe44c

CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr   Addresses: p=0x7fffffe41c q=0x7fffffe41c

CHERI:CHERI-O0-uintcap-offset   Addresses: p=0x7fffffe4a8 q=0x7fffffe4a8

CHERI:CHERI-O2-uintcap-offset   Addresses: p=0x7fffffe44c q=0x7fffffe44c

CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset   Addresses: p=0x7fffffe41c q=0x7fffffe41c

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


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=0x7ffc9fbc74c0 q=0x7ffc9fbc74b8

compcert-3.2-O   Addresses: p=0x7ffd22cf04a0 q=0x7ffd22cf0498

compcert-3.2-interp   Time 0: calling main()
--[step_internal_function]-->
Time 1: in function main, statement
  y = 2;
  x = 1;
  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
  y = 2;
  x = 1;
  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 y = 2;
--[step_do_1]-->
Time 4: in function main, expression y = 2
--[red_var_local]-->
Time 5: in function main, expression <loc y> = 2
--[red_assign]-->
Time 6: in function main, expression 2
--[step_do_2]-->
Time 7: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 8: in function main, statement
  x = 1;
  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 x = 1;
--[step_do_1]-->
Time 10: in function main, expression x = 1
--[red_var_local]-->
Time 11: in function main, expression <loc x> = 1
--[red_assign]-->
Time 12: in function main, expression 1
--[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=<58+4> q=<57+0>
Stuck state: in function main, expression
                              printf(<ptr __stringlit_1>, <ptr x+4>, <ptr y>)
Addresses: p=<58+4> q=<57+0>
Stuck subexpression:
                              printf(<ptr __stringlit_1>, <ptr x+4>, <ptr y>)
ERROR: Undefined behavior
In file included from provenance_basic_auto_yx.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.

gcc-8.1-O0		Addresses: p=0x7ffc1b1a318c q=0x7ffc1b1a318c x=1 y=11 p=11 q=11
gcc-8.1-O2		Addresses: p=0x7ffe4660ddf0 q=0x7ffe4660dde8
gcc-8.1-O3		Addresses: p=0x7ffccdf60bf0 q=0x7ffccdf60be8
gcc-8.1-O2-no-strict-aliasing		Addresses: p=0x7ffe0d4f1930 q=0x7ffe0d4f1928
gcc-8.1-O3-no-strict-aliasing		Addresses: p=0x7fff8be1b180 q=0x7fff8be1b178
clang-6.0-O0		Addresses: p=0x7ffd82d01458 q=0x7ffd82d01458 x=1 y=11 p=11 q=11
clang-6.0-O2		Addresses: p=0x7fff7c8e5404 q=0x7fff7c8e5404 x=1 y=11 p=11 q=11
clang-6.0-O3		Addresses: p=0x7ffd2c962c34 q=0x7ffd2c962c34 x=1 y=11 p=11 q=11
clang-6.0-O2-no-strict-aliasing		Addresses: p=0x7ffd3effcbd4 q=0x7ffd3effcbd4 x=1 y=11 p=11 q=11
clang-6.0-O3-no-strict-aliasing		Addresses: p=0x7ffd56456a24 q=0x7ffd56456a24 x=1 y=11 p=11 q=11
clang-6.0-UBSAN		Addresses: p=0x7ffff7e4ef84 q=0x7ffff7e4ef84 x=1 y=11 p=11 q=11 provenance_basic_auto_yx.c:9:5: runtime error: store to address 0x7ffff7e4ef84 with insufficient space for an object of type 'int' 0x7ffff7e4ef84: 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 e8 ae 63 bb 7f 00 00 ^ provenance_basic_auto_yx.c:10:42: runtime error: load of address 0x7ffff7e4ef84 with insufficient space for an object of type 'int' 0x7ffff7e4ef84: 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 e8 ae 63 bb 7f 00 00 ^
clang-6.0-ASAN		Addresses: p=0x7fffc9108394 q=0x7fffc9108380
clang-6.0-MSAN		Addresses: p=0x7ffd765ce6b4 q=0x7ffd765ce6b4 x=1 y=11 p=11 q=11
icc-19-O0		Addresses: p=0x7ffcef084178 q=0x7ffcef084170
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] Defined {value: "Specified(0)", stdout: "Addresses: p=<6>:80 q=<5>:72\n", blocked: "false"} END EXEC[0] Time spent: 0.048259 seconds
cerberus-symbolic		BEGIN EXEC[0] Undefined [other_location(Core parser)]{id: [DUMMY(rev_listFromStr_aux)]} END EXEC[0] Time spent: 0.072964 seconds
gcc-4.9-shadowprov		Addresses: p=0x7ffc4fc6d91c q=0x7ffc4fc6d948
CHERI:MIPS-O0		Addresses: p=0x7fffffe9f0 q=0x7fffffe9f0 x=1 y=11 p=11 q=11
CHERI:MIPS-O2		Addresses: p=0x7fffffe9e4 q=0x7fffffe9e4 x=1 y=11 p=11 q=11
CHERI:MIPS-O2-no-strict-aliasing		Addresses: p=0x7fffffe9c4 q=0x7fffffe9c4 x=1 y=11 p=11 q=11
CHERI:CHERI-O0-uintcap-addr-exact-equals		Addresses: p=0x7fffffe488 q=0x7fffffe488
CHERI:CHERI-O2-uintcap-addr-exact-equals		Addresses: p=0x7fffffe42c q=0x7fffffe42c
CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr-exact-equals		Addresses: p=0x7fffffe40c q=0x7fffffe40c
CHERI:CHERI-O0-uintcap-offset-exact-equals		Addresses: p=0x7fffffe488 q=0x7fffffe488
CHERI:CHERI-O2-uintcap-offset-exact-equals		Addresses: p=0x7fffffe42c q=0x7fffffe42c
CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset-exact-equals		Addresses: p=0x7fffffe40c q=0x7fffffe40c
CHERI:CHERI-O0-uintcap-addr		Addresses: p=0x7fffffe4a8 q=0x7fffffe4a8
CHERI:CHERI-O2-uintcap-addr		Addresses: p=0x7fffffe44c q=0x7fffffe44c
CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr		Addresses: p=0x7fffffe41c q=0x7fffffe41c
CHERI:CHERI-O0-uintcap-offset		Addresses: p=0x7fffffe4a8 q=0x7fffffe4a8
CHERI:CHERI-O2-uintcap-offset		Addresses: p=0x7fffffe44c q=0x7fffffe44c
CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset		Addresses: p=0x7fffffe41c q=0x7fffffe41c
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_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
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=0x7ffc9fbc74c0 q=0x7ffc9fbc74b8
compcert-3.2-O		Addresses: p=0x7ffd22cf04a0 q=0x7ffd22cf0498
compcert-3.2-interp		Time 0: calling main() --[step_internal_function]--> Time 1: in function main, statement y = 2; x = 1; 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 y = 2; x = 1; 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 y = 2; --[step_do_1]--> Time 4: in function main, expression y = 2 --[red_var_local]--> Time 5: in function main, expression <loc y> = 2 --[red_assign]--> Time 6: in function main, expression 2 --[step_do_2]--> Time 7: in function main, statement /skip/; --[step_skip_seq]--> Time 8: in function main, statement x = 1; 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 x = 1; --[step_do_1]--> Time 10: in function main, expression x = 1 --[red_var_local]--> Time 11: in function main, expression <loc x> = 1 --[red_assign]--> Time 12: in function main, expression 1 --[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=<58+4> q=<57+0> Stuck state: in function main, expression printf(<ptr __stringlit_1>, <ptr x+4>, <ptr y>) Addresses: p=<58+4> q=<57+0> Stuck subexpression: printf(<ptr __stringlit_1>, <ptr x+4>, <ptr y>) ERROR: Undefined behavior In file included from provenance_basic_auto_yx.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.

Example: provenance_basic_auto_yx.c

Example: `provenance_basic_auto_yx.c`