package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Module `Impact.Reason_graph`Source

Sourcetype reason_type =

| Intraprocedural of Pdg_types.PdgTypes.Dpd.t
(*
The effect of n' in f impact n, which is also in f.
*)
| InterproceduralDownward
(*
the effect of n' in f has an effect on a callee f' of f, in which n is located.
*)
| 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.

module ReasonType : Frama_c_kernel.Datatype.S with type t = reason_type

module Reason : 
  Frama_c_kernel.Datatype.S_with_collections
    with type t =
           Pdg_types.PdgTypes.Node.t * Pdg_types.PdgTypes.Node.t * reason_type

Sourcetype reason_graph = Reason.Set.t

Source

type nodes_origin =
  Frama_c_kernel.Cil_types.kernel_function Pdg_types.PdgTypes.Node.Map.t

Map from a node to the kernel_function it belongs to

Sourcetype reason = {

reason_graph : reason_graph;
nodes_origin : nodes_origin;
initial_nodes : Pdg_aux.NS.t;

}

module DatatypeReason : Frama_c_kernel.Datatype.S with type t = reason

Sourceval empty : reason

Source

val to_dot_formatter : 
  ?in_kf:Frama_c_kernel.Cil_types.kernel_function ->
  reason ->
  Format.formatter ->
  unit

Sourceval print_dot_graph : reason -> unit

package frama-c

Module Impact.Reason_graphSource

Module `Impact.Reason_graph`Source