In the particular case of the ASSIGNSCALAR rule, the program fragment passed to update is the assignment x ::= e itself, which means that the set of blocks to be updated evaluates to just S P x. Correctness of the update depends on a correctness criterion for the S P function itself. Our formalization uses a predicate admissible S P E M program (shown in Figure  8 ) to express that a static analysis S P computes a safe overapproximation of points-to sets with respect to the given program, environment, and starting memory. An alias function is admissible for a program in a certain configuration if it captures every assignment's target's correctly and is admissible for all possible configurations that arise in the evaluation of subprograms. E x = b E, M, Γ ⊢ offs → o offset, s E, M, Γ ⊢ Var x offs ← (b, offset), s LVALVAR E, M, Γ ⊢ a → Ptr (b, offs), s E, M, Γ ⊢ Deref a ← (b, offs), s LVALMEM E, M, Γ ⊢ Const c → Num c, ⊥ RVALCONST E, M, Γ ⊢ a ← (b, None), sl M b = ScalarVal v Γ b = sr sl ⊔ sr = s E, M, Γ ⊢ Lval a → v, s RVALSCALARLVAL E, M, Γ ⊢ a ← (b, Some idx), sl M b = ArrayVal arr arr idx = v Γ b = sr sl ⊔ sr = s E, M, Γ ⊢ Lval a → v, s RVALARRAYLVAL E, M, Γ ⊢ a ← l, s p = Ptr l E, M, Γ ⊢ AddrOf a → p, s RVALREF E, M, Γ ⊢ a → Num va, sa E, M, Γ ⊢ b → Num vb, sb eval-binop va vb = v sa ⊔ sb = s E, M, Γ ⊢ a • b → Num v, s RVALBINOP E, M, Γ ⊢ p → Ptr (b, Some idx), sb E, M, Γ ⊢ offs → Num i, si l = (b, Some (idx + i)) s = sb ⊔ si E, M, Γ ⊢ p ⊕ offs → Ptr l, s RVALPTRADD E, M, Γ ⊢ NoOffset → o None, ⊥ OFFSNONE E, M, Γ ⊢ i → Num idx, s E, M, Γ ⊢ Index i → o Some idx, s OFFSIDX E, S P , pc ⊢ Skip, M, Γ ⇒ M, Γ SKIP E, M, Γ ⊢ x ← (b, None), sl E, M, Γ ⊢ e → v, sv s = sl ⊔ sv ⊔ pc s ′ = sl ⊔ pc M ′ = M(b := ScalarVal v) Γ ′ = Γ(b := s) Γ ′′ = update S P (x ::= e) s ′ Γ ′ E, S P , pc ⊢ x ::= e, M, Γ ⇒ M ′ , Γ ′′ ASSIGNSCALAR E, M, Γ ⊢ x ← (b, Some i), sl E, M, Γ ⊢ e → v, sv s = sl ⊔ sv ⊔ pc s ′ = sl ⊔ pc M b = ArrayVal arr M ′ = M(b := ArrayVal (arr(i := v))) Γ b = l Γ ′ = Γ(b := s ⊔ l) Γ ′′ = update S P (x ::= e) s ′ Γ ′ E, S P , pc ⊢ x ::= ′ e, M, Γ ⇒ M ′ , Γ ′′ ASSIGNARRAYELEM E, S P , pc ⊢ c 1 , M, Γ ⇒ M ′ , Γ ′ E, S P , pc ⊢ c 2 , M ′ , Γ ′ ⇒ M ′′ , Γ ′′ E, S P , pc ⊢ c 1 ;; c 2 , M, Γ ⇒ M ′′ , Γ ′′ COMP E, M, Γ ⊢ cond → v, s istrue v pc ′ = s ⊔ pc E, S P , pc ′ ⊢ then-body, M, Γ ⇒ M ′ , Γ ′ Γ ′′ = update S P else-body pc ′ Γ ′ E, S P , pc ⊢ If cond then-body else-body, M, Γ ⇒ M ′ , Γ ′′ IFT E, M, Γ ⊢ a → v, s ¬ istrue v pc ′ = s ⊔ pc E, S P , pc ′ ⊢ else-body, M, Γ ⇒ M ′ , Γ ′ Γ ′′ = update S P then-body pc ′ Γ ′ E, S P , pc ⊢ If a then-body else-body, M, Γ ⇒ M ′ , Γ ′′ IFF E, M, Γ ⊢ cond → v, s istrue v pc ′ = s ⊔ pc E, S P , pc ′ ⊢ body, M, Γ ⇒ M ′ , Γ ′ E, S P , pc ′ ⊢ While cond body, M ′ , Γ ′ ⇒ M ′′ , Γ ′′ E, S P , pc ⊢ While cond body, M, Γ ⇒ M ′′ , Γ ′′ WHILET E, M, Γ ⊢ cond → v, s ¬ istrue v pc ′ = s ⊔ pc Γ ′ = update S P body pc ′ Γ E, S P , pc ⊢ While cond body, M, Γ ⇒ M, Γ ′ WHILEF ′ -) = S P x | collect-updates S P (Seq i 1 i 2 ) = collect-updates S P i 1 ∪ collect-updates S P i 2 | collect-updates S P (If -i 1 i 2 ) = collect-updates S P i 1 ∪ collect-updates S P i 2 | collect-updates S P (While -i) = collect- The ASSIGNARRAYELEM rule is similar to ASSIGNSCALAR in its handling of the label memory.