Example: provenance_via_io_uintptr_t_global.c

up: index
prev: provenance_via_io_bytewise_global.c
next: pointer_from_integer_1pg.c

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

    #include <stdio.h>
    #include <stdlib.h>
    #include <string.h>
    #include <inttypes.h>
    int x=1;
    int main() {
      int *p = &x;
      uintptr_t i = (uintptr_t) p;
      FILE *f = fopen(
        "provenance_via_io_uintptr_t_global.tmp","w+b");
      printf("Addresses: i=%"PRIuPTR" \n",i);
      // print pointer address to a file
      fprintf(f,"%"PRIuPTR"\n",i);
      rewind(f);
      uintptr_t k;
      // read a pointer address from the file
      int n = fscanf(f,"%"SCNuPTR"\n",&k);
      if (n != 1) exit(EXIT_FAILURE);
      printf("Addresses: k=%"PRIuPTR"\n",k);
      int *r = (int *)k;
      // are r and q now equivalent?  
      *r=12; // is this free of undefined behaviour?                                                           
      _Bool b1 = (r==p); // do they compare equal?                      
      _Bool b2 = (0==memcmp(&r,&p,sizeof(r)));//same reps?
      printf("x=%i *r=%i b1=%s b2=%s\n",x,*r,
             b1?"true":"false",b2?"true":"false");
    }
[link to run test in Cerberus]

Experimental data (what does this mean?) 



cerberus-concrete-PVI exit codes: compile 0 / execute 1
provenance_via_io_uintptr_t_global.c:18:20: error: use of undeclared identifier '__cerbvar_EXIT_FAILURE'
  if (n != 1) exit(EXIT_FAILURE);
                   ^
§6.5.1#2: 
2   An identifier is a primary expression, provided it has been declared as designating an
    object (in which case it is an lvalue) or a function (in which case it is a function
    designator).91)


cerberus-concrete-PNVI exit codes: compile 0 / execute 1
provenance_via_io_uintptr_t_global.c:18:20: error: use of undeclared identifier '__cerbvar_EXIT_FAILURE'
  if (n != 1) exit(EXIT_FAILURE);
                   ^
§6.5.1#2: 
2   An identifier is a primary expression, provided it has been declared as designating an
    object (in which case it is an lvalue) or a function (in which case it is a function
    designator).91)


gcc-8.1-O0 Addresses: i=6294768 
Addresses: k=6294768
x=12 *r=12 b1=true b2=true


gcc-8.1-O2 Addresses: i=6294568 
Addresses: k=6294568
x=12 *r=12 b1=true b2=true


gcc-8.1-O3 Addresses: i=6294568 
Addresses: k=6294568
x=12 *r=12 b1=true b2=true


gcc-8.1-O2-no-strict-aliasing Addresses: i=6294568 
Addresses: k=6294568
x=12 *r=12 b1=true b2=true


gcc-8.1-O3-no-strict-aliasing Addresses: i=6294568 
Addresses: k=6294568
x=12 *r=12 b1=true b2=true


clang-6.0-O0 Addresses: i=6295656 
Addresses: k=6295656
x=12 *r=12 b1=true b2=true


clang-6.0-O2 Addresses: i=6295648 
Addresses: k=6295648
x=12 *r=12 b1=true b2=true


clang-6.0-O3 Addresses: i=6295648 
Addresses: k=6295648
x=12 *r=12 b1=true b2=true


clang-6.0-O2-no-strict-aliasing Addresses: i=6295648 
Addresses: k=6295648
x=12 *r=12 b1=true b2=true


clang-6.0-O3-no-strict-aliasing Addresses: i=6295648 
Addresses: k=6295648
x=12 *r=12 b1=true b2=true


clang-6.0-UBSAN Addresses: i=6499200 
Addresses: k=6499200
x=12 *r=12 b1=true b2=true


clang-6.0-ASAN Addresses: i=7433088 
Addresses: k=7433088
x=12 *r=12 b1=true b2=true


clang-6.0-MSAN Addresses: i=7043840 
Addresses: k=7043840
x=12 *r=12 b1=true b2=true


icc-19-O0 Addresses: i=6295160 
Addresses: k=6295160
x=12 *r=12 b1=true b2=true


icc-19-O2 Addresses: i=6309600 
Addresses: k=6309600
x=12 *r=12 b1=true b2=true


icc-19-O3 Addresses: i=6309600 
Addresses: k=6309600
x=12 *r=12 b1=true b2=true


icc-19-O2-no-strict-aliasing Addresses: i=6309600 
Addresses: k=6309600
x=12 *r=12 b1=true b2=true


icc-19-O3-no-strict-aliasing Addresses: i=6309600 
Addresses: k=6309600
x=12 *r=12 b1=true b2=true


compcert-3.4 Addresses: i=6295656 
Addresses: k=6295656
x=12 *r=12 b1=true b2=true


compcert-3.4-O Addresses: i=6295656 
Addresses: k=6295656
x=12 *r=12 b1=true b2=true


kcc-1.0 exit codes: compile 0 / execute 139
Addresses: i=0 
Addresses: k=0
Printing an unspecified value:
      > in printf at provenance_via_io_uintptr_t_global.c:11:3
        in main at provenance_via_io_uintptr_t_global.c:11:3

    Unspecified value or behavior (USP-STDIO2):
        see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1

Printing an unspecified value:
      > in fprintf at provenance_via_io_uintptr_t_global.c:13:3
        in main at provenance_via_io_uintptr_t_global.c:13:3

    Unspecified value or behavior (USP-STDIO2):
        see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1

Conversion from an integer to non-null pointer:
      > in main at provenance_via_io_uintptr_t_global.c:20:3

    Implementation defined behavior (IMPL-CCV13):
        see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3
        see CERT section INT36-C http://rvdoc.org/CERT/INT36-C

Dereferencing a null pointer:
      > in main at provenance_via_io_uintptr_t_global.c:22:3

    Undefined behavior (UB-CER3):
        see C11 section 6.5.3.2:4 http://rvdoc.org/C11/6.5.3.2
        see C11 section J.2:1 item 43 http://rvdoc.org/C11/J.2
        see CERT-C section EXP34-C http://rvdoc.org/CERT-C/EXP34-C
        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1

Execution failed (configuration dumped)