module Widen_hints_ext:sig
..end
Syntax extension for widening hints, used by Value.
val dkey : Self.category
type
hint_vars =
| |
HintAllVars |
| |
HintVar of |
| |
HintMem of |
val pp_hvars : Stdlib.Format.formatter -> hint_vars -> unit
type
hint_lval = {
|
vars : |
|
names : |
|
loc : |
}
Type of widening hints: a special kind of lval for which the hints will apply and a list of names (e.g. global).
typet =
hint_lval * Cil_types.term list
val get_stmt_widen_hint_terms : Cil_types.stmt -> t list
get_stmt_widen_hint_terms s
returns the list of widen hints associated to
s
.
val is_global : t -> bool
is_global wh
returns true iff widening hint wh
has a "global" prefix.
val is_dynamic : t -> bool
is_dynamic wh
returns true iff widening hint wh
has a "dynamic" prefix.