pointer-aliasing.c

// pointer aliasing causes sometimes the properties of pointer manipulation.
// not able to satisfy the conditions.

/* @
requires \valid(a) && \valid_read(b);
assigns *a;
ensures *a == \old(*a) + *b; // this one will  be facing the issues because of lack of verification of 
ensures *b == \old(*b);
*/

void pointer_add(int* a, int* b) {
  *a = *a + *b;
}

/** why is the validation of the assign clause in the previous function ?
as its a pointer that is only modified (in both condition if a !=b and a == b) and thus the value of the pointer is not changed, but the value of the pointed memory is changed.

*/

// in order to define the condition that all of the above pointers are seperately implemented? 
// we will be using the \separated(p1, ..., pn) predicate as follows:

/*@
  requires \valid(a) && \valid_read(b);
  \separated(a, b); // this will ensure that the pointers a and b are not pointing to the same memory location and resolves issue of the upcoming descriptions.
  assigns  *a;
  ensures  *a == \old(*a)+ *b;
  ensures  *b == \old(*b);


*/
void pointer_add_separated(int* a, int* b) {
  *a += *b;
}