package mopsa

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

Install

Dune Dependency

Authors

Maintainers

Sources

mopsa-analyzer-v1.1.tar.gz
md5=fdee20e988343751de440b4f6b67c0f4
sha512=f5cbf1328785d3f5ce40155dada2d95e5de5cce4f084ea30cfb04d1ab10cc9403a26cfb3fa55d0f9da72244482130fdb89c286a9aed0d640bba46b7c00e09500

doc/ast/Ast/Stmt/index.html

Module Ast.StmtSource

Statements

This module is responsible for extending the Mopsa AST with new statements. This is done by creating new variant constructor of the extensible type stmt_kind, for instance

  type stmt_kind += S_assign of expr * expr

creates a new assignment statement, which needs to be registered

  let () = register_stmt {
      compare = (fun next s1 s2 ->
          match skind s1, skind s2 with
          | S_assign(x1,e1), S_assign(x2,e2) ->
            Compare.pair compare_expr compare_expr (x1,e1) (x2,e2)
          | _ -> next s1 s2
        );
      print = (fun next s ->
          match skind s with
          | S_assign(x,e) -> Format.fprintf fmt "%a = %a;" pp_expr x pp_expr e
          | _    -> next fmt s
        );
    }
Sourcetype stmt_kind = ..

Extensible kinds of statements

Sourcetype stmt = {
  1. skind : stmt_kind;
    (*

    kind of the statement

    *)
  2. srange : Mopsa_utils.Location.range;
    (*

    location range of the statement

    *)
}

Statements

Create a statement

Sourceval skind : stmt -> stmt_kind

Get the kind of a statement

Get the location range of a statement

Sourceval compare_stmt : stmt -> stmt -> int

Total order between statements

Sourceval pp_stmt : Stdlib.Format.formatter -> stmt -> unit

Pretty-printer of statements

Registration

Sourceval register_stmt : stmt Mopsa_utils.TypeExt.info -> unit

register_stmt info registers a new statement by registering its compare function info.compare and pretty-printer info.print

Sourceval register_stmt_compare : stmt Mopsa_utils.TypeExt.compare -> unit

Register a comparison function for statements

Sourceval register_stmt_pp : stmt Mopsa_utils.TypeExt.print -> unit

Register a pretty-printer function for statements

Blocks

Sourcetype block = stmt list

Blocks are sequences of statements

Sourceval pp_block : Stdlib.Format.formatter -> block -> unit

Pretty-printer for blocks

Common statements

Sourcetype stmt_kind +=
  1. | S_program of Program.program * string list option
    (*

    Command-line arguments as given to Mopsa after --

    *)

Programs

Sourcetype stmt_kind +=
  1. | S_assign of Expr.expr * Expr.expr
    (*

    rhs

    *)

Assignments

mk_assign lhs rhs range creates the assignment lhs = rhs;

Sourcetype stmt_kind +=
  1. | S_assume of Expr.expr
    (*

    condition

    *)

Tests

Create a test statement

Sourcetype stmt_kind +=
  1. | S_add of Expr.expr
    (*

    Add a dimension to the environment

    *)
  2. | S_remove of Expr.expr
    (*

    Remove a dimension from the environment and invalidate all references to it

    *)
  3. | S_invalidate of Expr.expr
    (*

    Invalidate all references to a dimension without removing it

    *)
  4. | S_rename of Expr.expr * Expr.expr
    (*

    new

    *)
  5. | S_forget of Expr.expr
    (*

    Forget a dimension by putting ⊤ (all possible values) in it. Note that the dimension is not removed

    *)
  6. | S_project of Expr.expr list
    (*

    Project the environment on the given list of dimensions. All other dimensions are removed

    *)
  7. | S_expand of Expr.expr * Expr.expr list
    (*

    Expand a dimension into a list of other dimensions. The expanded dimension is untouched

    *)
  8. | S_fold of Expr.expr * Expr.expr list
    (*

    Fold a list of dimensions into a single one. The folded dimensions are removed

    *)
  9. | S_block of stmt list * Var.var list
    (*

    local variables declared within the block

    *)
  10. | S_breakpoint of string
    (*

    Trigger a breakpoint

    *)

Dimensions

Utility functions to create various statements for dimension management

Sourceval mk_invalidate_var : Var.var -> Mopsa_utils.Location.range -> stmt
Sourceval mk_project : Expr.expr list -> Mopsa_utils.Location.range -> stmt
Sourceval mk_project_vars : Var.var list -> Mopsa_utils.Location.range -> stmt
Sourceval mk_expand_var : Var.var -> Var.var list -> Mopsa_utils.Location.range -> stmt
Sourceval mk_fold_var : Var.var -> Var.var list -> Mopsa_utils.Location.range -> stmt
Sourceval mk_breakpoint : string -> Mopsa_utils.Location.range -> stmt

Containers of statements

Sets of statements

Maps of statements

OCaml

Innovation. Community. Security.