Relation between Hoare Type Theory and pointers

Question

My understanding is that in Hoare Type Theory every imperative statement has a type of the form {Pre}res:T{Post} where T is the type of the result of the computation and Pre and Post are propositions representing respectively the pre and postconditions of the statement and res is the result of type T which can appear in the postcondition.

Given the following program in pseudo-C:

int i=0;
int*p=&i;
*p=1
return i;

How can Hoare type theory represent the the fact that i must be 1?After all,it's not clear i is modified in the above snippet,and it can be hidden even from the programmer if we begin to add lambdas and partial application