module Widen_type: sig
.. end
Widening hints for the Value Analysis datastructures.
include Datatype.S
val empty : t
An empty set of hints
val default : unit -> t
A default set of hints
val join : t -> t -> t
val pretty : Format.formatter -> t -> unit
Pretty-prints a set of hints (for debug purposes only).
Since Silicon-20161101
val num_hints : Cil_types.stmt option -> Base.t option -> Ival.Widen_Hints.t -> t
Define numeric hints for one or all variables (None
),
for a certain stmt or for all statements (None
).
val var_hints : Cil_types.stmt -> Base.Set.t -> t
Define a set of bases to widen in priority for a given statement.
val hints_from_keys : Cil_types.stmt ->
t -> Base.Set.t * (Base.t -> Locations.Location_Bytes.generic_widen_hint)
Widen hints for a given statement, suitable for function
Cvalue.Model.widen
.