• Robbert Krebbers's avatar
    Fix bugs in pointer operations · baaee9e0
    Robbert Krebbers authored
    * Equality comparison of NULL and non NULL pointers should be defined
    * Pointer comparisons, casts, and truth should only be defined for pointers
      that are alive
    * Treat dead pointers as indeterminate values in refinements. The proofs that
      all operations preserve refinement indicate that dead pointers can be indeed
      by replaced by anything without affecting the program's behavior.
    baaee9e0
option.v 11.6 KB