package mopsa

  1. Overview
  2. Docs

Module Core.ControlCtx

Control context - representation of the call stack and loop analysis positino of a program analysis

Loop sites

**************

type loop_info =
  1. | Unrolling of int
  2. | Fixpoint_iteration
type loopsite = {
  1. loop_range : Location.range;
  2. loop_info : loop_info;
}

Control context

***************

type control_info =
  1. | Call of Callstack.callsite
  2. | Loop of loopsite
type control_ctx = control_info list
val extract_callstack : control_ctx -> Callstack.callstack
val within_enriched_loop_ctx : control_ctx -> loopsite -> (control_ctx -> 'a) -> 'a
val push_callstack : string -> ?uniq:string -> Location.range -> control_ctx -> control_ctx

push_callstack orig ~uniq range cs adds the call to function orig at location range at the top of the call stack cs. The default unique function name of the function is its original name.

exception Bad_control_ctx

Exception raised when a Call is expected at the top of the control context and a Loop is found (or conversely)

val pop_callstack : control_ctx -> Callstack.callsite * control_ctx

pop_callstack cc returns the last call site in cc and the remaining control context Raises Empty_callstack if the call stack is empty. Raises Bad_control_ctx if the control context starts with Loop info.

val pp_control_ctx : Format.formatter -> control_ctx -> unit

Print control context

val compare_control_ctx : control_ctx -> control_ctx -> int

Compare control context

val empty_control_ctx : control_ctx

Empty control context

val is_empty_control_ctx : control_ctx -> bool

Check that a control context is empty