search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
424 stars 91 forks source link

Changed definition of valid_pointer' wrt locations with PURE resource… #771

Closed lennartberinger closed 4 weeks ago

lennartberinger commented 2 months ago

…s, to facilitate proof of lemma func_at_valid_pointer and ensuing lemmas about func_ptr and func_ptr'