Class type virtual Cumulative_analysis.cumulative_class

class type virtual ['a] cumulative_class = object .. end
Inherits
method bottom : 'a
method result : 'a

Result of the analysis

Adding partial results to the current ones

method join : 'a -> unit
method compute_funspec : Cil_types.kernel_function -> 'a

Function that computes and returns the partial results on a funspec. May consult self#current_stmt to specialize itself, and return partially contextual results

method clean_kf_result : Cil_types.kernel_function -> 'a -> 'a

Assuming v are the results of the analysis for f (ie. the union of the results on all the statements of f, or compute_funspec f if f has no body), clean_kf_result k v cleans those results before storing them. Use for example to remove out-of-scope locals