package frama-c

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val transform_category : File.code_transformation_category

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).

OCaml

Innovation. Community. Security.