package frama-c

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Filtering on analysis callstacks

type rcallstack

List.rev on a callstack, enforced by strong typing outside of this module

val empty : rcallstack
val from_callstack : Eva.Callstack.t -> rcallstack
type filter = rcallstack list option

Filters on callstacks. None means that all callstacks are active

val callstack_matches : filter -> rcallstack -> bool
val callsite_matches : filter -> Frama_c_kernel.Cil_types.stmt -> bool
val focused_callstacks : unit -> filter
val focus_on_callstacks : filter -> unit
val is_reachable_stmt : filter -> Frama_c_kernel.Cil_types.stmt -> bool
val is_non_terminating_instr : filter -> Frama_c_kernel.Cil_types.stmt -> bool
val register_to_zone_functions : (module Gui_eval.S) -> unit