package mopsa

  1. Overview
  2. Docs
MOPSA: A Modular and Open Platform for Static Analysis using Abstract Interpretation

Install 

dune-project
 Dependency

mopsa.lip6.fr Readme Changelog Edit opam file Versions (3)

Authors

  1. A
    Antoine Miné
  2. A
    Abdelraouf Ouadjaout
  3. M
    Matthieu Journault
  4. A
    Aymeric Fromherz
  5. R
    Raphaël Monat
  6. F
    Francesco Parolini
  7. M
    Marco Milanese
  8. J
    Jérôme Boillot

Maintainers

  1. A
    Antoine Miné <antoine.mine@lip6.fr>
  2. A
    Abdelraouf Ouadjaout <ouadjaout@gmail.com>
  3. R
    Raphaël Monat <raphael.monat@inria.fr>

Sources

mopsa-analyzer-v1.2.tar.gz
md5=37966e98ffeebcedc09bd6e9b2b81f69
sha512=40d4d826c25f680766c07eccbabdf5e8a4fa023016e8a164e4e4f6b3781c8484dc4df437055721dfd19b9db8fb7fe3b61236c4833186d346fc7204a68d01eaaa

doc/mopsa.mopsa_utils/Mopsa_utils/Core/ControlCtx/index.html

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