package mopsa

You can search for identifiers within the package.

in-package search v0.2.0

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

Maintainers

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 =

| Unrolling of int
| Fixpoint_iteration

type loopsite = {

loop_range : Location.range;
loop_info : loop_info;

}

Control context

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

type control_info =

| Call of Callstack.callsite
| 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

On This Page

Loop sites
1. Control context