Class type virtual Cumulative_analysis.cumulative_class

class type virtual ['a] cumulative_class = object .. end

Inherits

Cumulative_analysis.cumulative_visitor

method bottom : 'a

method result : 'a

Result of the analysis

method join : 'a -> unit

Adding partial results to the current ones

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