module Widen:sig
..end
Stores a mapping from statements to parsed dynamic hint terms.
Only stores mappings for statements with annotations, to avoid
wasting memory.
The dataflow iteration consults this table each time it reaches
a statement with an annotation. It must quickly evaluate the
bases related to the annotations, to see if there are new bases
that should be added to the global widening hints. Therefore,
we store, for each annotation, the set of bases computed so far,
plus the thresholds (to avoid recomputing them).
val getWidenHints : Cil_types.kernel_function ->
Cil_types.stmt ->
Base.Set.t * (Base.t -> Locations.Location_Bytes.numerical_widen_hint)
getWidenHints kf s
retrieves the set of widening hints related to
function kf
and statement s
.val precompute_widen_hints : unit -> unit