• Robbert Krebbers's avatar
    Let the malloc expression non-deterministically yield NULL. · fdcc90dd
    Robbert Krebbers authored
    * This behavior is "implementation defined" and can be turned on and off
      using the Boolean field "alloc_can_fail" of the class "Env".
    * The expression "EAlloc" is now an r-value of pointer type instead of an
      l-value.
    * The executable semantics for expressions is now non-deterministic. Hence,
      some proofs had to be revised.
    fdcc90dd
collections.v 22.4 KB