Module Ghost_accesses

module Ghost_accesses: sig .. end

Checks that memory accesses are well-typed in the sense of the \ghost qualifier. That is, only ghost code can declare ghost memory, and ghost code can modify only ghost memory. Registered as a transformation category (that doesn't transform anything but will complain if there are bad accesses).


val transform_category : File.code_transformation_category