package mopsa

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
include sig ... end
val id : unit Core__Id.id
val name : string
val debug : ('a, Stdlib.Format.formatter, unit, unit) Stdlib.format4 -> 'a
val checks : Mopsa.check list

Initialization of environments

==============================

val init : 'a -> 'b -> 'c -> 'c

Command-line options

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

val opt_stub_ignored_cases : string list Stdlib.ref

List of ignored stub cases

val is_case_ignored : Ast.stub_func option -> Ast.case -> bool

Check whether a case is ignored

Evaluation of expressions

=========================

Negate a formula

val formula_to_prenex : Ast.formula Mopsa.with_range -> (Ast.quant * Mopsa.var * Ast.set) list * Mopsa.expr

Translate a formula into prenex normal form

val vars_of_condition : Mopsa.expr -> Mopsa.VarSet.t
val var_in_expr : Mopsa.var -> Ast.Expr.expr -> bool
val remove_unnecessary_quantifiers : ('a * Mopsa.VarSet.elt * Ast.set) list -> Mopsa.expr -> ('a * Mopsa.var * Ast.set) list

Translate a prenex encoding (i.e. quantifiers and a condition) into an expression

Evaluate a formula

val init_params : Ast.Expr.expr list -> Ast.Var.var list -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Core.Flow.flow -> 'a Core.Flow.flow

Initialize the parameters of the stubbed function

val remove_params : Ast.Var.var list -> Mopsa_utils.Location.range -> ('a, 'b) Core.Manager.man -> 'a Core.Flow.flow -> 'a Core.Flow.flow

Remove parameters from the returned flow

Evaluate the formula of the `assumes` section

val exec_local_new : Ast.Var.var -> string -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Core.Flow.flow -> 'a Mopsa.post

Execute an allocation of a new resource

val exec_local_call : Ast.Var.var -> Mopsa.expr -> Mopsa.expr list -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Core.Flow.flow -> 'a Core.Post.post

Execute a function call

val exec_local : Ast.local Mopsa.with_range -> ('a, 'b) Mopsa.man -> 'a Core.Flow.flow -> 'a Mopsa.post

Execute the `local` section

val exec_assigns : Ast.assigns Mopsa.with_range -> ('a, 'b) Mopsa.man -> 'a Core.Flow.flow -> 'a Core.Post.post
val clean_post : Ast.local Mopsa.with_range list -> Mopsa_utils.Location.range -> ('a, 'b) Core.Manager.man -> 'a Core.Flow.flow -> 'a Core.Flow.flow

Remove locals

val exec_free : Mopsa.expr Mopsa.with_range -> ('a, 'b) Mopsa.man -> 'a Core.Flow.flow -> 'a Core.Post.post
val exec_message : Ast.message Mopsa.with_range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Post.post
val exec_leaf : Ast.leaf -> Ast.Var.var option -> ('a, 'b) Mopsa.man -> 'a Core.Flow.flow -> 'a Mopsa.post

Execute a leaf section

val exec_case : Ast.case -> Ast.Var.var option -> ('a, 'b) Core.Manager.man -> 'a Core.Flow.flow -> 'a Mopsa.flow

Execute the body of a case section

val exec_body : ?stub:Ast.stub_func option -> Ast.section list -> Ast.Var.var option -> 'b -> ('a, 'c) Mopsa.man -> 'a Mopsa.flow -> 'a Mopsa.Flow.flow

Execute the body of a stub

val eval_stub_call : Ast.stub_func -> Ast.Expr.expr list -> Ast.Var.var option -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Eval.eval

Evaluate a call to a stub

Evaluate an otherwise expression

val discard_empty_quantification_intervals : (Ast.quant * Ast.Var.var * Ast.set) list -> Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Core.Flow.flow -> ('a, Ast.Expr.expr) Core.Cases.cases
val otherwise_in_condition : Mopsa.expr -> bool

Check if a condition contains an otherwise expression

val remove_new_checks : 'a Mopsa.Flow.flow -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Remove newly introduced checks

Move newly introduced checks to a new range

val eval : Mopsa.expr -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> ('a, Ast.Expr.expr) Mopsa.Cases.cases option

Entry point of expression evaluations

Computation of post-conditions

==============================

val exec_directive : Ast.stub_directive -> 'a -> ('b, 'c) Core.Manager.man -> 'b Core.Flow.flow -> 'b Mopsa.Post.post

Execute a global stub directive

val normalize_requirement_condition : Mopsa.expr -> Mopsa.expr

Normalize a requirement condition by adding missing otherwise decorations

val exec_requires : Mopsa.expr -> 'a -> ('b, 'c) Mopsa.man -> 'b Core.Flow.flow -> ('b, unit) Mopsa.Cases.cases

Check a stub requirement

val exec : Mopsa.stmt -> ('a, 'b) Core.Manager.man -> 'a Core.Flow.flow -> 'a Mopsa.Post.post option

Handler of queries

==================

val ask : 'a -> 'b -> 'c -> 'd option

Pretty printer

==============

val print_expr : 'a -> 'b -> 'c -> 'd -> unit
OCaml

Innovation. Community. Security.