Wp.Layout
Region Utilities
module type Data = sig ... end
type offset =
| Field of Frama_c_kernel.Cil_types.fieldinfo |
| Index of Frama_c_kernel.Cil_types.typ * int |
type lvalue =
| Eval of Frama_c_kernel.Cil_types.exp |
| Tval of Frama_c_kernel.Cil_types.term |
| Assigned of Frama_c_kernel.Cil_types.stmt |
Generalized l-values
module Offset : sig ... end
type deref = usage * Frama_c_kernel.Cil_types.typ
module Alias : sig ... end
module Usage : sig ... end
module Value : sig ... end
module Matrix : sig ... end
type 'a overlay = 'a range list
module Range : sig ... end
module Overlay : sig ... end
module Compound : sig ... end
module Cluster : sig ... end
type 'a from =
| Fvar of Frama_c_kernel.Cil_types.varinfo |
| Ffield of 'a * int |
| Findex of 'a |
| Fderef of 'a |
| Farray of 'a |
type root =
| Rnone |
| Rfield of Frama_c_kernel.Cil_types.varinfo * int |
| Rindex of Frama_c_kernel.Cil_types.varinfo |
| Rtop |
module Root : sig ... end
type chunks = Qed.Intset.t
module Chunk : sig ... end
module RW : sig ... end
Read-Write access
module Flat : sig ... end
Flatten arrays
module Pack : sig ... end
Pack fields