module Origin:sig
..end
module LocationLattice:sig
..end
type
origin =
| |
Misalign_read of |
(* |
Read of not all the bits of a
pointer, typically through a pointer cast
| *) |
| |
Leaf of |
(* |
Result of a function without a body
| *) |
| |
Merge of |
(* |
Join between two control-flows
| *) |
| |
Arith of |
(* |
Arithmetic operation that cannot be
represented, eg.
'&x * 2' | *) |
| |
Well |
(* |
Imprecise variables of the initial state
| *) |
| |
Unknown |
include Datatype.S
type
kind =
| |
K_Misalign_read |
| |
K_Leaf |
| |
K_Merge |
| |
K_Arith |
val current : kind -> origin
Cil.CurrentLoc
val pretty_as_reason : Format.formatter -> t -> unit
because of <origin>
if the origin is not Unknown
, or
nothing otherwiseval top : t
val is_top : t -> bool
val bottom : t
val join : t -> t -> t
val link : t -> t -> t
val meet : t -> t -> t
val narrow : t -> t -> t
val is_included : t -> t -> bool