8 A pointer logic and certifying compiler We use II/p to denote performing S/p for each S in II. When an effective pointer q is assigned a value which is not equal to q,I/q should be performed.For example,in Fig.2 where II ={fu,v->pre},[v,u->next}}, II/v={fu,u->next->pre},fu->next}}.(fu->next}means that u->next is an effective pointer and is not equal to any of other pointers. data data pre pre next ext Fig.2.Pointers in a doubly-linked cyclic list 5)M\p or D\p replaces the pointers in N or D which use p's aliases as their prefixes with their other aliases.A/p or D/p deletes the aliases of p from A or p Np q:N|Vp':closure(p).-prefix(p',q)}u q'q:N.p'closure(p).(prefix(p',q)'=alias(q,p))} NIp≌{q:WI(q∈closure(p)} N/{p1…pn}≌(NIp1).…/Pn) The formal definitions of D\p and D/p are similar. 6)We use the set operator U to represent the union of two pointer sets.Usually. this operator is used to add a pointer to a pointer set.And we also use set operators U and -and their combinations to represent the addition,deletion and substitution of equivalent sets. 7)Function no_leak(p)tests the result of S/p for S containing p(just testing,not really deleting).This testing is to avoid memory leaks caused by an assignment to p. no_leak(p)if equals(p)/p!=0 then true else false 2.3 Axioms and inference rules In this section,we define axioms and inference rules in our pointer logic.In the following rules,p and q are access paths;p.eq is p's equivalent set,and p.eq equals(p).8 A pointer logic and certifying compiler We use Π/p to denote performing S/p for each S in Π. When an effective pointer q is assigned a value which is not equal to q, Π/q should be performed. For example, in Fig. 2 where Π = {{u, v->pre}, {v, u->next}}, Π/v = {{u, u->next->pre}, {u->next}}. ({u->next} means that u->next is an effective pointer and is not equal to any of other pointers.) ￾

    ￾

    ￾
Fig. 2. Pointers in a doubly-linked cyclic list 5) N \p or D\p replaces the pointers in N or D which use p’s aliases as their prefixes with their other aliases. N /p or D/p deletes the aliases of p from N or D. N \p , {q : N | ∀p 0 : closure(p).¬prefix(p 0 , q)}∪ {q 0 | ∃q : N .∃p 0 : closure(p).(prefix(p 0 , q) ∧ q 0 ≡ alias(q, p))} N /p , {q : N | ¬(q ∈ closure(p))} N /{p1 . . . pn} , ((N /p1 ). . . /pn) The formal definitions of D\p and D/p are similar. 6) We use the set operator ∪ to represent the union of two pointer sets. Usually, this operator is used to add a pointer to a pointer set. And we also use set operators ∪ and − and their combinations to represent the addition, deletion and substitution of equivalent sets. 7) Function no leak(p) tests the result of S/p for S containing p (just testing, not really deleting). This testing is to avoid memory leaks caused by an assignment to p. no leak(p) , if equals(p)/p!=∅ then true else false 2.3 Axioms and inference rules In this section, we define axioms and inference rules in our pointer logic. In the following rules, p and q are access paths; p.eq is p’s equivalent set, and p.eq = equals(p).