Example: pointer_copy_user_dataflow_direct_bytewise_struct.c

#include <stdio.h>
#include <string.h>
typedef struct { int i; float f; } st;
st s1 = {.i=1, .f=1.0 };
st s2;
void user_memcpy(unsigned char* dest, 
                 unsigned char *src, size_t n) {
  while (n > 0)  {		
    *dest = *src;
    src += 1;
    dest += 1;
    n -= 1;
  }
}
int main() {
  st *p = &s1;
  st *q = &s2;
  user_memcpy((unsigned char*)q, 
              (unsigned char*)p, sizeof(st));
  // is this free of undefined behaviour?
  printf("p->i = %d  q->i = %d\n",p->i,q->i);
}
[link to test in Cerberus and Compiler Explorer]

Experimental data (what does this mean?) 



gcc-8.1-O0 p->i = 1  q->i = 1


gcc-8.1-O2 p->i = 1  q->i = 1


gcc-8.1-O3 p->i = 1  q->i = 1


gcc-8.1-O2-no-strict-aliasing p->i = 1  q->i = 1


gcc-8.1-O3-no-strict-aliasing p->i = 1  q->i = 1


clang-6.0-O0 p->i = 1  q->i = 1


clang-6.0-O2 p->i = 1  q->i = 1


clang-6.0-O3 p->i = 1  q->i = 1


clang-6.0-O2-no-strict-aliasing p->i = 1  q->i = 1


clang-6.0-O3-no-strict-aliasing p->i = 1  q->i = 1


clang-6.0-UBSAN p->i = 1  q->i = 1


clang-6.0-ASAN p->i = 1  q->i = 1


clang-6.0-MSAN p->i = 1  q->i = 1


icc-19-O0 p->i = 1  q->i = 1


icc-19-O2 p->i = 1  q->i = 1


icc-19-O3 p->i = 1  q->i = 1


icc-19-O2-no-strict-aliasing p->i = 1  q->i = 1


icc-19-O3-no-strict-aliasing p->i = 1  q->i = 1


cerberus-concrete BEGIN EXEC[0]
Defined {value: "Specified(0)", stdout: "p->i = 1  q->i = 1\n", blocked: "false"}
END EXEC[0]
Time spent: 0.046866 seconds


cerberus-symbolic exit codes: compile 0 / execute 1
BOGUS!!!!
BOGUS!!!!
cerberus: internal error, uncaught exception:
          Failure("TODO: Symbolic defacto, isWellAligned_ptrval")
          


gcc-4.9-shadowprov p->i = 1  q->i = 1


CHERI:MIPS-O0 p->i = 1  q->i = 1


CHERI:MIPS-O2 p->i = 1  q->i = 1


CHERI:MIPS-O2-no-strict-aliasing p->i = 1  q->i = 1


CHERI:CHERI-O0-uintcap-addr-exact-equals p->i = 1  q->i = 1


CHERI:CHERI-O2-uintcap-addr-exact-equals p->i = 1  q->i = 1


CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr-exact-equals p->i = 1  q->i = 1


CHERI:CHERI-O0-uintcap-offset-exact-equals p->i = 1  q->i = 1


CHERI:CHERI-O2-uintcap-offset-exact-equals p->i = 1  q->i = 1


CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset-exact-equals p->i = 1  q->i = 1


CHERI:CHERI-O0-uintcap-addr p->i = 1  q->i = 1


CHERI:CHERI-O2-uintcap-addr p->i = 1  q->i = 1


CHERI:CHERI-O2-no-strict-aliasing-uintcap-addr p->i = 1  q->i = 1


CHERI:CHERI-O0-uintcap-offset p->i = 1  q->i = 1


CHERI:CHERI-O2-uintcap-offset p->i = 1  q->i = 1


CHERI:CHERI-O2-no-strict-aliasing-uintcap-offset p->i = 1  q->i = 1


RV-Match p->i = 1  q->i = 1


ch2o Fatal error: exception Main.Unknown_specifier(_)
Raised at file "bytes.ml", line 220, characters 25-34
Called from file "ratio.ml", line 553, characters 12-30


compcert-3.2 p->i = 1  q->i = 1


compcert-3.2-O p->i = 1  q->i = 1


compcert-3.2-interp Time 0: calling main()
--[step_internal_function]-->
Time 1: in function main, statement
  p = &s1;
  q = &s2;
  user_memcpy((unsigned char *) q, (unsigned char *) p, sizeof(struct _692));
  printf(__stringlit_1, ((*.)).i, ((*.)).i);
  return 0;
--[step_seq]-->
Time 2: in function main, statement
  p = &s1;
  q = &s2;
  user_memcpy((unsigned char *) q, (unsigned char *) p, sizeof(struct _692));
  printf(__stringlit_1, ((*.)).i, ((*.)).i);
--[step_seq]-->
Time 3: in function main, statement p = &s1;
--[step_do_1]-->
Time 4: in function main, expression p = &s1
--[red_var_local]-->
Time 5: in function main, expression <loc p> = &s1
--[red_var_global]-->
Time 6: in function main, expression <loc p> = &<loc s1>
--[red_addrof]-->
Time 7: in function main, expression <loc p> = <ptr s1>
--[red_assign]-->
Time 8: in function main, expression <ptr s1>
--[step_do_2]-->
Time 9: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 10: in function main, statement
  q = &s2;
  user_memcpy((unsigned char *) q, (unsigned char *) p, sizeof(struct _692));
  printf(__stringlit_1, ((*.)).i, ((*.)).i);
--[step_seq]-->
Time 11: in function main, statement q = &s2;
--[step_do_1]-->
Time 12: in function main, expression q = &s2
--[red_var_local]-->
Time 13: in function main, expression <loc q> = &s2
--[red_var_global]-->
Time 14: in function main, expression <loc q> = &<loc s2>
--[red_addrof]-->
Time 15: in function main, expression <loc q> = <ptr s2>
--[red_assign]-->
Time 16: in function main, expression <ptr s2>
--[step_do_2]-->
Time 17: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 18: in function main, statement
  user_memcpy((unsigned char *) q, (unsigned char *) p, sizeof(struct _692));
  printf(__stringlit_1, ((*.)).i, ((*.)).i);
--[step_seq]-->
Time 19: in function main, statement
  user_memcpy((unsigned char *) q, (unsigned char *) p, sizeof(struct _692));
--[step_do_1]-->
Time 20: in function main, expression
  user_memcpy((unsigned char *) q, (unsigned char *) p, sizeof(struct _692))
--[red_var_global]-->
Time 21: in function main, expression
  <loc user_memcpy>((unsigned char *) q, 
                    (unsigned char *) p, 
                    sizeof(struct _692))
--[red_rvalof]-->
Time 22: in function main, expression
  <ptr user_memcpy>((unsigned char *) q, 
                    (unsigned char *) p, 
                    sizeof(struct _692))
--[red_var_local]-->
Time 23: in function main, expression
  <ptr user_memcpy>((unsigned char *) <loc q>, 
                    (unsigned char *) p, 
                    sizeof(struct _692))
--[red_rvalof]-->
Time 24: in function main, expression
  <ptr user_memcpy>((unsigned char *) <ptr s2>, 
                    (unsigned char *) p, 
                    sizeof(struct _692))
--[red_cast]-->
Time 25: in function main, expression
  <ptr user_memcpy>(<ptr s2>, (unsigned char *) p, sizeof(struct _692))
--[red_var_local]-->
Time 26: in function main, expression
  <ptr user_memcpy>(<ptr s2>, (unsigned char *) <loc p>, sizeof(struct _692))
--[red_rvalof]-->
Time 27: in function main, expression
  <ptr user_memcpy>(<ptr s2>, (unsigned char *) <ptr s1>,
                    sizeof(struct _692))
--[red_cast]-->
Time 28: in function main, expression
  <ptr user_memcpy>(<ptr s2>, <ptr s1>, sizeof(struct _692))
--[red_sizeof]-->
Time 29: in function main, expression
  <ptr user_memcpy>(<ptr s2>, <ptr s1>, 8U)
--[red_call]-->
Time 30: calling user_memcpy(<ptr s2>, <ptr s1>, 8)
--[step_internal_function]-->
Time 31: in function user_memcpy, statement
  while (n > 0) {
    *dest = *src;
    src += 1;
    dest += 1;
    n -= 1;
  }
--[step_while]-->
Time 32: in function user_memcpy, expression n > 0
--[red_var_local]-->
Time 33: in function user_memcpy, expression <loc n> > 0
--[red_rvalof]-->
Time 34: in function user_memcpy, expression 8U > 0
--[red_binop]-->
Time 35: in function user_memcpy, expression 1
--[step_while_true]-->
Time 36: in function user_memcpy, statement
  *dest = *src; src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 37: in function user_memcpy, statement *dest = *src;
--[step_do_1]-->
Time 38: in function user_memcpy, expression *dest = *src
--[red_var_local]-->
Time 39: in function user_memcpy, expression *<loc dest> = *src
--[red_rvalof]-->
Time 40: in function user_memcpy, expression *<ptr s2> = *src
--[red_deref]-->
Time 41: in function user_memcpy, expression <loc s2> = *src
--[red_var_local]-->
Time 42: in function user_memcpy, expression <loc s2> = *<loc src>
--[red_rvalof]-->
Time 43: in function user_memcpy, expression <loc s2> = *<ptr s1>
--[red_deref]-->
Time 44: in function user_memcpy, expression <loc s2> = <loc s1>
--[red_rvalof]-->
Time 45: in function user_memcpy, expression <loc s2> = 1
--[red_assign]-->
Time 46: in function user_memcpy, expression 1
--[step_do_2]-->
Time 47: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 48: in function user_memcpy, statement src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 49: in function user_memcpy, statement src += 1;
--[step_do_1]-->
Time 50: in function user_memcpy, expression src += 1
--[red_var_local]-->
Time 51: in function user_memcpy, expression <loc src> += 1
--[red_assignop]-->
Time 52: in function user_memcpy, expression <loc src> = <ptr s1> + 1
--[red_binop]-->
Time 53: in function user_memcpy, expression <loc src> = <ptr s1+1>
--[red_assign]-->
Time 54: in function user_memcpy, expression <ptr s1+1>
--[step_do_2]-->
Time 55: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 56: in function user_memcpy, statement dest += 1; n -= 1;
--[step_seq]-->
Time 57: in function user_memcpy, statement dest += 1;
--[step_do_1]-->
Time 58: in function user_memcpy, expression dest += 1
--[red_var_local]-->
Time 59: in function user_memcpy, expression <loc dest> += 1
--[red_assignop]-->
Time 60: in function user_memcpy, expression <loc dest> = <ptr s2> + 1
--[red_binop]-->
Time 61: in function user_memcpy, expression <loc dest> = <ptr s2+1>
--[red_assign]-->
Time 62: in function user_memcpy, expression <ptr s2+1>
--[step_do_2]-->
Time 63: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 64: in function user_memcpy, statement n -= 1;
--[step_do_1]-->
Time 65: in function user_memcpy, expression n -= 1
--[red_var_local]-->
Time 66: in function user_memcpy, expression <loc n> -= 1
--[red_assignop]-->
Time 67: in function user_memcpy, expression <loc n> = 8U - 1
--[red_binop]-->
Time 68: in function user_memcpy, expression <loc n> = 7U
--[red_assign]-->
Time 69: in function user_memcpy, expression 7U
--[step_do_2]-->
Time 70: in function user_memcpy, statement /*skip*/;
--[step_skip_or_continue_while]-->
Time 71: in function user_memcpy, statement
  while (n > 0) {
    *dest = *src;
    src += 1;
    dest += 1;
    n -= 1;
  }
--[step_while]-->
Time 72: in function user_memcpy, expression n > 0
--[red_var_local]-->
Time 73: in function user_memcpy, expression <loc n> > 0
--[red_rvalof]-->
Time 74: in function user_memcpy, expression 7U > 0
--[red_binop]-->
Time 75: in function user_memcpy, expression 1
--[step_while_true]-->
Time 76: in function user_memcpy, statement
  *dest = *src; src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 77: in function user_memcpy, statement *dest = *src;
--[step_do_1]-->
Time 78: in function user_memcpy, expression *dest = *src
--[red_var_local]-->
Time 79: in function user_memcpy, expression *<loc dest> = *src
--[red_rvalof]-->
Time 80: in function user_memcpy, expression *<ptr s2+1> = *src
--[red_deref]-->
Time 81: in function user_memcpy, expression <loc s2+1> = *src
--[red_var_local]-->
Time 82: in function user_memcpy, expression <loc s2+1> = *<loc src>
--[red_rvalof]-->
Time 83: in function user_memcpy, expression <loc s2+1> = *<ptr s1+1>
--[red_deref]-->
Time 84: in function user_memcpy, expression <loc s2+1> = <loc s1+1>
--[red_rvalof]-->
Time 85: in function user_memcpy, expression <loc s2+1> = 0
--[red_assign]-->
Time 86: in function user_memcpy, expression 0
--[step_do_2]-->
Time 87: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 88: in function user_memcpy, statement src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 89: in function user_memcpy, statement src += 1;
--[step_do_1]-->
Time 90: in function user_memcpy, expression src += 1
--[red_var_local]-->
Time 91: in function user_memcpy, expression <loc src> += 1
--[red_assignop]-->
Time 92: in function user_memcpy, expression <loc src> = <ptr s1+1> + 1
--[red_binop]-->
Time 93: in function user_memcpy, expression <loc src> = <ptr s1+2>
--[red_assign]-->
Time 94: in function user_memcpy, expression <ptr s1+2>
--[step_do_2]-->
Time 95: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 96: in function user_memcpy, statement dest += 1; n -= 1;
--[step_seq]-->
Time 97: in function user_memcpy, statement dest += 1;
--[step_do_1]-->
Time 98: in function user_memcpy, expression dest += 1
--[red_var_local]-->
Time 99: in function user_memcpy, expression <loc dest> += 1
--[red_assignop]-->
Time 100: in function user_memcpy, expression <loc dest> = <ptr s2+1> + 1
--[red_binop]-->
Time 101: in function user_memcpy, expression <loc dest> = <ptr s2+2>
--[red_assign]-->
Time 102: in function user_memcpy, expression <ptr s2+2>
--[step_do_2]-->
Time 103: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 104: in function user_memcpy, statement n -= 1;
--[step_do_1]-->
Time 105: in function user_memcpy, expression n -= 1
--[red_var_local]-->
Time 106: in function user_memcpy, expression <loc n> -= 1
--[red_assignop]-->
Time 107: in function user_memcpy, expression <loc n> = 7U - 1
--[red_binop]-->
Time 108: in function user_memcpy, expression <loc n> = 6U
--[red_assign]-->
Time 109: in function user_memcpy, expression 6U
--[step_do_2]-->
Time 110: in function user_memcpy, statement /*skip*/;
--[step_skip_or_continue_while]-->
Time 111: in function user_memcpy, statement
  while (n > 0) {
    *dest = *src;
    src += 1;
    dest += 1;
    n -= 1;
  }
--[step_while]-->
Time 112: in function user_memcpy, expression n > 0
--[red_var_local]-->
Time 113: in function user_memcpy, expression <loc n> > 0
--[red_rvalof]-->
Time 114: in function user_memcpy, expression 6U > 0
--[red_binop]-->
Time 115: in function user_memcpy, expression 1
--[step_while_true]-->
Time 116: in function user_memcpy, statement
  *dest = *src; src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 117: in function user_memcpy, statement *dest = *src;
--[step_do_1]-->
Time 118: in function user_memcpy, expression *dest = *src
--[red_var_local]-->
Time 119: in function user_memcpy, expression *<loc dest> = *src
--[red_rvalof]-->
Time 120: in function user_memcpy, expression *<ptr s2+2> = *src
--[red_deref]-->
Time 121: in function user_memcpy, expression <loc s2+2> = *src
--[red_var_local]-->
Time 122: in function user_memcpy, expression <loc s2+2> = *<loc src>
--[red_rvalof]-->
Time 123: in function user_memcpy, expression <loc s2+2> = *<ptr s1+2>
--[red_deref]-->
Time 124: in function user_memcpy, expression <loc s2+2> = <loc s1+2>
--[red_rvalof]-->
Time 125: in function user_memcpy, expression <loc s2+2> = 0
--[red_assign]-->
Time 126: in function user_memcpy, expression 0
--[step_do_2]-->
Time 127: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 128: in function user_memcpy, statement src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 129: in function user_memcpy, statement src += 1;
--[step_do_1]-->
Time 130: in function user_memcpy, expression src += 1
--[red_var_local]-->
Time 131: in function user_memcpy, expression <loc src> += 1
--[red_assignop]-->
Time 132: in function user_memcpy, expression <loc src> = <ptr s1+2> + 1
--[red_binop]-->
Time 133: in function user_memcpy, expression <loc src> = <ptr s1+3>
--[red_assign]-->
Time 134: in function user_memcpy, expression <ptr s1+3>
--[step_do_2]-->
Time 135: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 136: in function user_memcpy, statement dest += 1; n -= 1;
--[step_seq]-->
Time 137: in function user_memcpy, statement dest += 1;
--[step_do_1]-->
Time 138: in function user_memcpy, expression dest += 1
--[red_var_local]-->
Time 139: in function user_memcpy, expression <loc dest> += 1
--[red_assignop]-->
Time 140: in function user_memcpy, expression <loc dest> = <ptr s2+2> + 1
--[red_binop]-->
Time 141: in function user_memcpy, expression <loc dest> = <ptr s2+3>
--[red_assign]-->
Time 142: in function user_memcpy, expression <ptr s2+3>
--[step_do_2]-->
Time 143: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 144: in function user_memcpy, statement n -= 1;
--[step_do_1]-->
Time 145: in function user_memcpy, expression n -= 1
--[red_var_local]-->
Time 146: in function user_memcpy, expression <loc n> -= 1
--[red_assignop]-->
Time 147: in function user_memcpy, expression <loc n> = 6U - 1
--[red_binop]-->
Time 148: in function user_memcpy, expression <loc n> = 5U
--[red_assign]-->
Time 149: in function user_memcpy, expression 5U
--[step_do_2]-->
Time 150: in function user_memcpy, statement /*skip*/;
--[step_skip_or_continue_while]-->
Time 151: in function user_memcpy, statement
  while (n > 0) {
    *dest = *src;
    src += 1;
    dest += 1;
    n -= 1;
  }
--[step_while]-->
Time 152: in function user_memcpy, expression n > 0
--[red_var_local]-->
Time 153: in function user_memcpy, expression <loc n> > 0
--[red_rvalof]-->
Time 154: in function user_memcpy, expression 5U > 0
--[red_binop]-->
Time 155: in function user_memcpy, expression 1
--[step_while_true]-->
Time 156: in function user_memcpy, statement
  *dest = *src; src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 157: in function user_memcpy, statement *dest = *src;
--[step_do_1]-->
Time 158: in function user_memcpy, expression *dest = *src
--[red_var_local]-->
Time 159: in function user_memcpy, expression *<loc dest> = *src
--[red_rvalof]-->
Time 160: in function user_memcpy, expression *<ptr s2+3> = *src
--[red_deref]-->
Time 161: in function user_memcpy, expression <loc s2+3> = *src
--[red_var_local]-->
Time 162: in function user_memcpy, expression <loc s2+3> = *<loc src>
--[red_rvalof]-->
Time 163: in function user_memcpy, expression <loc s2+3> = *<ptr s1+3>
--[red_deref]-->
Time 164: in function user_memcpy, expression <loc s2+3> = <loc s1+3>
--[red_rvalof]-->
Time 165: in function user_memcpy, expression <loc s2+3> = 0
--[red_assign]-->
Time 166: in function user_memcpy, expression 0
--[step_do_2]-->
Time 167: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 168: in function user_memcpy, statement src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 169: in function user_memcpy, statement src += 1;
--[step_do_1]-->
Time 170: in function user_memcpy, expression src += 1
--[red_var_local]-->
Time 171: in function user_memcpy, expression <loc src> += 1
--[red_assignop]-->
Time 172: in function user_memcpy, expression <loc src> = <ptr s1+3> + 1
--[red_binop]-->
Time 173: in function user_memcpy, expression <loc src> = <ptr s1+4>
--[red_assign]-->
Time 174: in function user_memcpy, expression <ptr s1+4>
--[step_do_2]-->
Time 175: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 176: in function user_memcpy, statement dest += 1; n -= 1;
--[step_seq]-->
Time 177: in function user_memcpy, statement dest += 1;
--[step_do_1]-->
Time 178: in function user_memcpy, expression dest += 1
--[red_var_local]-->
Time 179: in function user_memcpy, expression <loc dest> += 1
--[red_assignop]-->
Time 180: in function user_memcpy, expression <loc dest> = <ptr s2+3> + 1
--[red_binop]-->
Time 181: in function user_memcpy, expression <loc dest> = <ptr s2+4>
--[red_assign]-->
Time 182: in function user_memcpy, expression <ptr s2+4>
--[step_do_2]-->
Time 183: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 184: in function user_memcpy, statement n -= 1;
--[step_do_1]-->
Time 185: in function user_memcpy, expression n -= 1
--[red_var_local]-->
Time 186: in function user_memcpy, expression <loc n> -= 1
--[red_assignop]-->
Time 187: in function user_memcpy, expression <loc n> = 5U - 1
--[red_binop]-->
Time 188: in function user_memcpy, expression <loc n> = 4U
--[red_assign]-->
Time 189: in function user_memcpy, expression 4U
--[step_do_2]-->
Time 190: in function user_memcpy, statement /*skip*/;
--[step_skip_or_continue_while]-->
Time 191: in function user_memcpy, statement
  while (n > 0) {
    *dest = *src;
    src += 1;
    dest += 1;
    n -= 1;
  }
--[step_while]-->
Time 192: in function user_memcpy, expression n > 0
--[red_var_local]-->
Time 193: in function user_memcpy, expression <loc n> > 0
--[red_rvalof]-->
Time 194: in function user_memcpy, expression 4U > 0
--[red_binop]-->
Time 195: in function user_memcpy, expression 1
--[step_while_true]-->
Time 196: in function user_memcpy, statement
  *dest = *src; src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 197: in function user_memcpy, statement *dest = *src;
--[step_do_1]-->
Time 198: in function user_memcpy, expression *dest = *src
--[red_var_local]-->
Time 199: in function user_memcpy, expression *<loc dest> = *src
--[red_rvalof]-->
Time 200: in function user_memcpy, expression *<ptr s2+4> = *src
--[red_deref]-->
Time 201: in function user_memcpy, expression <loc s2+4> = *src
--[red_var_local]-->
Time 202: in function user_memcpy, expression <loc s2+4> = *<loc src>
--[red_rvalof]-->
Time 203: in function user_memcpy, expression <loc s2+4> = *<ptr s1+4>
--[red_deref]-->
Time 204: in function user_memcpy, expression <loc s2+4> = <loc s1+4>
--[red_rvalof]-->
Time 205: in function user_memcpy, expression <loc s2+4> = 0
--[red_assign]-->
Time 206: in function user_memcpy, expression 0
--[step_do_2]-->
Time 207: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 208: in function user_memcpy, statement src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 209: in function user_memcpy, statement src += 1;
--[step_do_1]-->
Time 210: in function user_memcpy, expression src += 1
--[red_var_local]-->
Time 211: in function user_memcpy, expression <loc src> += 1
--[red_assignop]-->
Time 212: in function user_memcpy, expression <loc src> = <ptr s1+4> + 1
--[red_binop]-->
Time 213: in function user_memcpy, expression <loc src> = <ptr s1+5>
--[red_assign]-->
Time 214: in function user_memcpy, expression <ptr s1+5>
--[step_do_2]-->
Time 215: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 216: in function user_memcpy, statement dest += 1; n -= 1;
--[step_seq]-->
Time 217: in function user_memcpy, statement dest += 1;
--[step_do_1]-->
Time 218: in function user_memcpy, expression dest += 1
--[red_var_local]-->
Time 219: in function user_memcpy, expression <loc dest> += 1
--[red_assignop]-->
Time 220: in function user_memcpy, expression <loc dest> = <ptr s2+4> + 1
--[red_binop]-->
Time 221: in function user_memcpy, expression <loc dest> = <ptr s2+5>
--[red_assign]-->
Time 222: in function user_memcpy, expression <ptr s2+5>
--[step_do_2]-->
Time 223: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 224: in function user_memcpy, statement n -= 1;
--[step_do_1]-->
Time 225: in function user_memcpy, expression n -= 1
--[red_var_local]-->
Time 226: in function user_memcpy, expression <loc n> -= 1
--[red_assignop]-->
Time 227: in function user_memcpy, expression <loc n> = 4U - 1
--[red_binop]-->
Time 228: in function user_memcpy, expression <loc n> = 3U
--[red_assign]-->
Time 229: in function user_memcpy, expression 3U
--[step_do_2]-->
Time 230: in function user_memcpy, statement /*skip*/;
--[step_skip_or_continue_while]-->
Time 231: in function user_memcpy, statement
  while (n > 0) {
    *dest = *src;
    src += 1;
    dest += 1;
    n -= 1;
  }
--[step_while]-->
Time 232: in function user_memcpy, expression n > 0
--[red_var_local]-->
Time 233: in function user_memcpy, expression <loc n> > 0
--[red_rvalof]-->
Time 234: in function user_memcpy, expression 3U > 0
--[red_binop]-->
Time 235: in function user_memcpy, expression 1
--[step_while_true]-->
Time 236: in function user_memcpy, statement
  *dest = *src; src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 237: in function user_memcpy, statement *dest = *src;
--[step_do_1]-->
Time 238: in function user_memcpy, expression *dest = *src
--[red_var_local]-->
Time 239: in function user_memcpy, expression *<loc dest> = *src
--[red_rvalof]-->
Time 240: in function user_memcpy, expression *<ptr s2+5> = *src
--[red_deref]-->
Time 241: in function user_memcpy, expression <loc s2+5> = *src
--[red_var_local]-->
Time 242: in function user_memcpy, expression <loc s2+5> = *<loc src>
--[red_rvalof]-->
Time 243: in function user_memcpy, expression <loc s2+5> = *<ptr s1+5>
--[red_deref]-->
Time 244: in function user_memcpy, expression <loc s2+5> = <loc s1+5>
--[red_rvalof]-->
Time 245: in function user_memcpy, expression <loc s2+5> = 0
--[red_assign]-->
Time 246: in function user_memcpy, expression 0
--[step_do_2]-->
Time 247: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 248: in function user_memcpy, statement src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 249: in function user_memcpy, statement src += 1;
--[step_do_1]-->
Time 250: in function user_memcpy, expression src += 1
--[red_var_local]-->
Time 251: in function user_memcpy, expression <loc src> += 1
--[red_assignop]-->
Time 252: in function user_memcpy, expression <loc src> = <ptr s1+5> + 1
--[red_binop]-->
Time 253: in function user_memcpy, expression <loc src> = <ptr s1+6>
--[red_assign]-->
Time 254: in function user_memcpy, expression <ptr s1+6>
--[step_do_2]-->
Time 255: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 256: in function user_memcpy, statement dest += 1; n -= 1;
--[step_seq]-->
Time 257: in function user_memcpy, statement dest += 1;
--[step_do_1]-->
Time 258: in function user_memcpy, expression dest += 1
--[red_var_local]-->
Time 259: in function user_memcpy, expression <loc dest> += 1
--[red_assignop]-->
Time 260: in function user_memcpy, expression <loc dest> = <ptr s2+5> + 1
--[red_binop]-->
Time 261: in function user_memcpy, expression <loc dest> = <ptr s2+6>
--[red_assign]-->
Time 262: in function user_memcpy, expression <ptr s2+6>
--[step_do_2]-->
Time 263: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 264: in function user_memcpy, statement n -= 1;
--[step_do_1]-->
Time 265: in function user_memcpy, expression n -= 1
--[red_var_local]-->
Time 266: in function user_memcpy, expression <loc n> -= 1
--[red_assignop]-->
Time 267: in function user_memcpy, expression <loc n> = 3U - 1
--[red_binop]-->
Time 268: in function user_memcpy, expression <loc n> = 2U
--[red_assign]-->
Time 269: in function user_memcpy, expression 2U
--[step_do_2]-->
Time 270: in function user_memcpy, statement /*skip*/;
--[step_skip_or_continue_while]-->
Time 271: in function user_memcpy, statement
  while (n > 0) {
    *dest = *src;
    src += 1;
    dest += 1;
    n -= 1;
  }
--[step_while]-->
Time 272: in function user_memcpy, expression n > 0
--[red_var_local]-->
Time 273: in function user_memcpy, expression <loc n> > 0
--[red_rvalof]-->
Time 274: in function user_memcpy, expression 2U > 0
--[red_binop]-->
Time 275: in function user_memcpy, expression 1
--[step_while_true]-->
Time 276: in function user_memcpy, statement
  *dest = *src; src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 277: in function user_memcpy, statement *dest = *src;
--[step_do_1]-->
Time 278: in function user_memcpy, expression *dest = *src
--[red_var_local]-->
Time 279: in function user_memcpy, expression *<loc dest> = *src
--[red_rvalof]-->
Time 280: in function user_memcpy, expression *<ptr s2+6> = *src
--[red_deref]-->
Time 281: in function user_memcpy, expression <loc s2+6> = *src
--[red_var_local]-->
Time 282: in function user_memcpy, expression <loc s2+6> = *<loc src>
--[red_rvalof]-->
Time 283: in function user_memcpy, expression <loc s2+6> = *<ptr s1+6>
--[red_deref]-->
Time 284: in function user_memcpy, expression <loc s2+6> = <loc s1+6>
--[red_rvalof]-->
Time 285: in function user_memcpy, expression <loc s2+6> = 128
--[red_assign]-->
Time 286: in function user_memcpy, expression 128
--[step_do_2]-->
Time 287: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 288: in function user_memcpy, statement src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 289: in function user_memcpy, statement src += 1;
--[step_do_1]-->
Time 290: in function user_memcpy, expression src += 1
--[red_var_local]-->
Time 291: in function user_memcpy, expression <loc src> += 1
--[red_assignop]-->
Time 292: in function user_memcpy, expression <loc src> = <ptr s1+6> + 1
--[red_binop]-->
Time 293: in function user_memcpy, expression <loc src> = <ptr s1+7>
--[red_assign]-->
Time 294: in function user_memcpy, expression <ptr s1+7>
--[step_do_2]-->
Time 295: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 296: in function user_memcpy, statement dest += 1; n -= 1;
--[step_seq]-->
Time 297: in function user_memcpy, statement dest += 1;
--[step_do_1]-->
Time 298: in function user_memcpy, expression dest += 1
--[red_var_local]-->
Time 299: in function user_memcpy, expression <loc dest> += 1
--[red_assignop]-->
Time 300: in function user_memcpy, expression <loc dest> = <ptr s2+6> + 1
--[red_binop]-->
Time 301: in function user_memcpy, expression <loc dest> = <ptr s2+7>
--[red_assign]-->
Time 302: in function user_memcpy, expression <ptr s2+7>
--[step_do_2]-->
Time 303: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 304: in function user_memcpy, statement n -= 1;
--[step_do_1]-->
Time 305: in function user_memcpy, expression n -= 1
--[red_var_local]-->
Time 306: in function user_memcpy, expression <loc n> -= 1
--[red_assignop]-->
Time 307: in function user_memcpy, expression <loc n> = 2U - 1
--[red_binop]-->
Time 308: in function user_memcpy, expression <loc n> = 1U
--[red_assign]-->
Time 309: in function user_memcpy, expression 1U
--[step_do_2]-->
Time 310: in function user_memcpy, statement /*skip*/;
--[step_skip_or_continue_while]-->
Time 311: in function user_memcpy, statement
  while (n > 0) {
    *dest = *src;
    src += 1;
    dest += 1;
    n -= 1;
  }
--[step_while]-->
Time 312: in function user_memcpy, expression n > 0
--[red_var_local]-->
Time 313: in function user_memcpy, expression <loc n> > 0
--[red_rvalof]-->
Time 314: in function user_memcpy, expression 1U > 0
--[red_binop]-->
Time 315: in function user_memcpy, expression 1
--[step_while_true]-->
Time 316: in function user_memcpy, statement
  *dest = *src; src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 317: in function user_memcpy, statement *dest = *src;
--[step_do_1]-->
Time 318: in function user_memcpy, expression *dest = *src
--[red_var_local]-->
Time 319: in function user_memcpy, expression *<loc dest> = *src
--[red_rvalof]-->
Time 320: in function user_memcpy, expression *<ptr s2+7> = *src
--[red_deref]-->
Time 321: in function user_memcpy, expression <loc s2+7> = *src
--[red_var_local]-->
Time 322: in function user_memcpy, expression <loc s2+7> = *<loc src>
--[red_rvalof]-->
Time 323: in function user_memcpy, expression <loc s2+7> = *<ptr s1+7>
--[red_deref]-->
Time 324: in function user_memcpy, expression <loc s2+7> = <loc s1+7>
--[red_rvalof]-->
Time 325: in function user_memcpy, expression <loc s2+7> = 63
--[red_assign]-->
Time 326: in function user_memcpy, expression 63
--[step_do_2]-->
Time 327: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 328: in function user_memcpy, statement src += 1; dest += 1; n -= 1;
--[step_seq]-->
Time 329: in function user_memcpy, statement src += 1;
--[step_do_1]-->
Time 330: in function user_memcpy, expression src += 1
--[red_var_local]-->
Time 331: in function user_memcpy, expression <loc src> += 1
--[red_assignop]-->
Time 332: in function user_memcpy, expression <loc src> = <ptr s1+7> + 1
--[red_binop]-->
Time 333: in function user_memcpy, expression <loc src> = <ptr s1+8>
--[red_assign]-->
Time 334: in function user_memcpy, expression <ptr s1+8>
--[step_do_2]-->
Time 335: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 336: in function user_memcpy, statement dest += 1; n -= 1;
--[step_seq]-->
Time 337: in function user_memcpy, statement dest += 1;
--[step_do_1]-->
Time 338: in function user_memcpy, expression dest += 1
--[red_var_local]-->
Time 339: in function user_memcpy, expression <loc dest> += 1
--[red_assignop]-->
Time 340: in function user_memcpy, expression <loc dest> = <ptr s2+7> + 1
--[red_binop]-->
Time 341: in function user_memcpy, expression <loc dest> = <ptr s2+8>
--[red_assign]-->
Time 342: in function user_memcpy, expression <ptr s2+8>
--[step_do_2]-->
Time 343: in function user_memcpy, statement /*skip*/;
--[step_skip_seq]-->
Time 344: in function user_memcpy, statement n -= 1;
--[step_do_1]-->
Time 345: in function user_memcpy, expression n -= 1
--[red_var_local]-->
Time 346: in function user_memcpy, expression <loc n> -= 1
--[red_assignop]-->
Time 347: in function user_memcpy, expression <loc n> = 1U - 1
--[red_binop]-->
Time 348: in function user_memcpy, expression <loc n> = 0U
--[red_assign]-->
Time 349: in function user_memcpy, expression 0U
--[step_do_2]-->
Time 350: in function user_memcpy, statement /*skip*/;
--[step_skip_or_continue_while]-->
Time 351: in function user_memcpy, statement
  while (n > 0) {
    *dest = *src;
    src += 1;
    dest += 1;
    n -= 1;
  }
--[step_while]-->
Time 352: in function user_memcpy, expression n > 0
--[red_var_local]-->
Time 353: in function user_memcpy, expression <loc n> > 0
--[red_rvalof]-->
Time 354: in function user_memcpy, expression 0U > 0
--[red_binop]-->
Time 355: in function user_memcpy, expression 0
--[step_while_false]-->
Time 356: in function user_memcpy, statement /*skip*/;
--[step_skip_call]-->
Time 357: returning <undef>
--[step_returnstate]-->
Time 358: in function main, expression <undef>
--[step_do_2]-->
Time 359: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 360: in function main, statement
  printf(__stringlit_1, ((*.)).i, ((*.)).i);
--[step_do_1]-->
Time 361: in function main, expression
  printf(__stringlit_1, ((*.)).i, ((*.)).i)
--[red_var_global]-->
Time 362: in function main, expression
  printf(<loc __stringlit_1>, ((*.)).i, ((*.)).i)
--[red_rvalof]-->
Time 363: in function main, expression
  printf(<ptr __stringlit_1>, ((*.)).i, ((*.)).i)
--[red_var_local]-->
Time 364: in function main, expression
  printf(<ptr __stringlit_1>, ((*.)).i, ((*.)).i)
--[red_rvalof]-->
Time 365: in function main, expression
  printf(<ptr __stringlit_1>, ((*.)).i, ((*.)).i)
--[red_deref]-->
Time 366: in function main, expression
  printf(<ptr __stringlit_1>, <loc s1>.i, ((*.)).i)
--[red_rvalof]-->
Time 367: in function main, expression
  printf(<ptr __stringlit_1>, <ptr s1>.i, ((*.)).i)
--[red_field_struct]-->
Time 368: in function main, expression
  printf(<ptr __stringlit_1>, <loc s1>, ((*.)).i)
--[red_rvalof]-->
Time 369: in function main, expression
  printf(<ptr __stringlit_1>, 1, ((*.)).i)
--[red_var_local]-->
Time 370: in function main, expression
  printf(<ptr __stringlit_1>, 1, ((*.)).i)
--[red_rvalof]-->
Time 371: in function main, expression
  printf(<ptr __stringlit_1>, 1, ((*.)).i)
--[red_deref]-->
Time 372: in function main, expression
  printf(<ptr __stringlit_1>, 1, <loc s2>.i)
--[red_rvalof]-->
Time 373: in function main, expression
  printf(<ptr __stringlit_1>, 1, <ptr s2>.i)
--[red_field_struct]-->
Time 374: in function main, expression
  printf(<ptr __stringlit_1>, 1, <loc s2>)
--[red_rvalof]-->
Time 375: in function main, expression printf(<ptr __stringlit_1>, 1, 1)
p->i = 1  q->i = 1
Time 375: observable event:
                     extcall printf(& __stringlit_1, 1, 1) -> 19
--[red_builtin]-->
Time 376: in function main, expression 19
--[step_do_2]-->
Time 377: in function main, statement /*skip*/;
--[step_skip_seq]-->
Time 378: in function main, statement return 0;
--[step_return_1]-->
Time 379: in function main, expression 0
--[step_return_2]-->
Time 380: returning 0
Time 380: program terminated (exit code = 0)
In file included from pointer_copy_user_dataflow_direct_bytewise_struct.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.