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_analyzer/Mopsa_analyzer/Languages/Cfg/Ast/index.html

Module Cfg.Ast

Extends the simple Universal language with Control Flow Graphs.

Graph types

module Loc : sig ... end
module TagLoc : sig ... end
module Range : sig ... end
module Port : sig ... end
module LocSet : sig ... end
module LocMap : sig ... end
module LocHash : sig ... end
module TagLocSet : sig ... end
module TagLocMap : sig ... end
module TagLocHash : sig ... end
module RangeSet : sig ... end
module RangeMap : sig ... end
module RangeHash : sig ... end
module CFG_Param : sig ... end

Build CFG module.

module CFG : sig ... end
type graph = (unit, MopsaLib.stmt) CFG.graph

Edges are labelled with a statement. Nodes have no information in the graph structure. Abstract invariant information will be kept in maps separately from the CFG. This way, CFG can be kept immutable.

type node = (unit, MopsaLib.stmt) CFG.node
type edge = (unit, MopsaLib.stmt) CFG.edge
type node_id = TagLoc.t
type edge_id = Range.t
type port = MopsaLib.token
type cfg = {
  1. cfg_graph : graph;
  2. mutable cfg_order : node Mopsa_utils.Containers.GraphSig.nested_list list;
}

Graph utilities

val mk_node_id : ?id:int -> ?tag:string -> Loc.t -> node_id
val fresh_node_id : int LocHash.t
val mk_fresh_node_id : ?tag:string -> Loc.t -> node_id

Fresh node with some source location information. NOTE: Do not mix mk_fresh_node_id and mk_node_id as it can break uniqueness.

val loc_anonymous : Loc.t
val mk_anonymous_node_id : ?tag:string -> unit -> node_id

Fresh node without any source location information.

val copy_node_id : node_id -> node_id
val node_loc : node_id -> Loc.t
val pp_node_id : Format.formatter -> TagLoc.t -> unit
val pp_node_as_id : Format.formatter -> ('a, 'b) CFG.node -> unit
val compare_node_id : TagLoc.t -> TagLoc.t -> int
val mk_edge_id : ?tag:string -> MopsaLib.range -> edge_id
val fresh_edge_id : int RangeHash.t
val mk_fresh_edge_id : ?tag:string -> MopsaLib.range -> edge_id

Fresh range with possible some source range information. NOTE: Do not mix mk_fresh_edge_id and mk_edge_id as it can break uniqueness.

val mk_anonymous_edge_id : ?tag:string -> unit -> edge_id

Fresh range without any source range information.

val edge_range : edge_id -> MopsaLib.range
val pp_edge_id : Format.formatter -> MopsaLib.range -> unit
val pp_edge_as_id : Format.formatter -> ('a, 'b) CFG.edge -> unit
val compare_edge_id : MopsaLib.range -> MopsaLib.range -> int

Flows

type MopsaLib.token +=
  1. | T_cfg_node of node_id
  2. | T_cfg_edge_post of edge_id * port
  3. | T_cfg_entry of port

Associate a flow to each CFG node. We can store abstract information for the whole graph in a single abstract state, using node flows. We also associate a flow to cache the post-image of each CFG edge.

type MopsaLib.token +=
  1. | T_true
  2. | T_false

Flow for true and false branch of tests.

Statements

type MopsaLib.stmt_kind +=
  1. | S_cfg of cfg
  2. | S_test of MopsaLib.expr
    (*

    test nodes, with a true and a false branch

    *)
  3. | S_skip
    (*

    empty node

    *)