proposition: Lemma sapi_ptr_val: forall p m n, isptr p -> Int.min_signed <= n <= Int.max_signed -> (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. rewrite sem_add_pi_ptr_special; [| easy | | easy]. - simpl. rewrite offset_offset_val. f_equal. fold WORD_SIZE; rep_lia. - rewrite isptr_offset_val. assumption. Qed.
imports: CertiGraph.CertiGC(env_graph_gc gc_spec) CertiGraph.msl_ext.ramification_lemmas VST.concurrency.conclib