package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type nodes = Pdg_aux.NS.t

type result = nodes Frama_c_kernel.Kernel_function.Map.t

val initial_nodes : 
  skip:Frama_c_kernel.Locations.Zone.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  Pdg_types.PdgTypes.Node.t list

val nodes_impacted_by_stmts : 
  ?skip:Frama_c_kernel.Locations.Zone.t ->
  ?restrict:Frama_c_kernel.Locations.Zone.t ->
  ?reason:bool ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt list ->
  result * nodes Frama_c_kernel.Kernel_function.Map.t * Reason_graph.reason

nodes in returned map are initial nodes

val nodes_impacted_by_nodes : 
  ?skip:Frama_c_kernel.Locations.Zone.t ->
  ?restrict:Frama_c_kernel.Locations.Zone.t ->
  ?reason:bool ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Pdg_types.PdgTypes.Node.t list ->
  result * nodes Frama_c_kernel.Kernel_function.Map.t * Reason_graph.reason

nodes in returned map are initial nodes

val stmts_impacted : 
  ?skip:Frama_c_kernel.Locations.Zone.t ->
  reason:bool ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt list ->
  Frama_c_kernel.Cil_types.stmt list

val nodes_impacted : 
  ?skip:Frama_c_kernel.Locations.Zone.t ->
  reason:bool ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Pdg_types.PdgTypes.Node.t list ->
  nodes

val result_to_nodes : result -> nodes

val nodes_to_stmts : nodes -> Frama_c_kernel.Cil_types.stmt list

val impact_in_kf : result -> Frama_c_kernel.Cil_types.kernel_function -> nodes

val skip : unit -> Frama_c_kernel.Locations.Zone.t

computed from the option -impact-skip