[CN-exec] Provenance issue: function prologues have to be inserted before CN_LOAD

[moratorium08]

The problematic code:

int y;
int main() /*@ accesses y; @*/ {y = 2;return 0;}

This becomes

int main() /*@ accesses y; @*/ {CN_STORE(
  /* EXECUTABLE CN PRECONDITION */
  signed int __cn_ret = 0;
  initialise_ownership_ghost_state();
  initialise_ghost_stack_depth();
  alloc_ghost_array(0);
  initialise_exec_c_locs_mode(0);
  initialise_ownership_stack_mode(0);
  c_add_to_ghost_state((&y), sizeof(signed int), get_cn_stack_depth());
  y, 2);{ __cn_ret = 0; goto __cn_epilogue; }
/* EXECUTABLE CN POSTCONDITION */
__cn_epilogue:

  c_remove_from_ghost_state((&y), sizeof(signed int));

  free_ghost_array();

return __cn_ret;

}

which is incorrect.

misc

• CN version: 384f4f3

[rbanerjee20]

I guess this is an issue with multiple injections at the same point. Adding spaces/newlines between the curly braces and function body results in the correct instrumentation.