1-X.do_it
Class that implements the analysis. Must not deal with memoization, as this is automatically done by the functor
inherit 'a cumulative_visitor
method compute_funspec : Frama_c_kernel.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 : Frama_c_kernel.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