package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
type reason_type =
  1. | Intraprocedural of Pdg_types.PdgTypes.Dpd.t
    (*

    The effect of n' in f impact n, which is also in f.

    *)
  2. | InterproceduralDownward
    (*

    the effect of n' in f has an effect on a callee f' of f, in which n is located.

    *)
  3. | InterproceduralUpward
    (*

    the effect of n' in f has an effect on a caller f' of f (once the call to f has ended), n being in f'.

    *)

Why is a node impacted. The reasons will be given as n is impacted by the effect of [n'], and the impact is of type reason.

type reason_graph = Reason.Set.t

Map from a node to the kernel_function it belongs to

type reason = {
  1. reason_graph : reason_graph;
  2. nodes_origin : nodes_origin;
  3. initial_nodes : Pdg_aux.NS.t;
}
val empty : reason
val to_dot_formatter : ?in_kf:Frama_c_kernel.Cil_types.kernel_function -> reason -> Stdlib.Format.formatter -> unit
val print_dot_graph : reason -> unit