Module Widen

module Widen: sig .. end
Per-function computation of widening hints.

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
Parses all widening hints defined via the widen_hint syntax extension. The result is memoized for subsequent calls.