proposition: Lemma sapil_ptr_val: forall p m n, isptr p -> if Archi.ptr64 then force_val (sem_add_ptr_long int_or_ptr_type (offset_val (WORD_SIZE * m) p) (Vlong (Int64.repr n))) = offset_val (WORD_SIZE * (m + n)) p else force_val (sem_add_ptr_int int_or_ptr_type Signed (offset_val (WORD_SIZE * m) p) (vint n)) = offset_val (WORD_SIZE * (m + n)) p.
proof: Proof. intros. simpl. first [rewrite sem_add_pi_ptr_special' | rewrite sem_add_pl_ptr_special']; auto. simpl. fold WORD_SIZE. rewrite offset_offset_val. f_equal. lia. Qed.
imports: CertiGraph.CertiGC(env_graph_gc gc_spec) CertiGraph.msl_ext.ramification_lemmas VST.concurrency.conclib