Module Widen_type

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

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.