package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Body.Domain

include sig ... end
val id : unit Mopsa_analyzer__Framework__Core__Id.id
val name : string
val debug : ('a, Format.formatter, unit, unit) format4 -> 'a
val checks : MopsaLib.check list

Initialization of environments

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

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

Command-line options

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

val opt_stub_ignored_cases : string list ref

List of ignored stub cases

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

Check whether a case is ignored

Evaluation of expressions

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

Negate a formula

Translate a formula into prenex normal form

val var_in_expr : MopsaLib.var -> Framework.Core.Ast.Expr.expr -> bool
val remove_unnecessary_quantifiers : ('a * Mopsa_analyzer.MopsaLib.VarSet.elt * Stubs.Ast.set) list -> MopsaLib.expr -> ('a * MopsaLib.var * Stubs.Ast.set) list

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

Evaluate a formula

Initialize the parameters of the stubbed function

Remove parameters from the returned flow

Evaluate the formula of the `assumes` section

Execute an allocation of a new resource

Execute a function call

Execute the `local` section

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

Remove locals

val exec_leaf : Stubs.Ast.leaf -> Framework.Core.Ast.Var.var option -> ('a, 'b) MopsaLib.man -> 'a Core.Flow.flow -> 'a MopsaLib.post

Execute a leaf section

val exec_case : ?stub:Stubs.Ast.stub_func option -> Stubs.Ast.case -> Framework.Core.Ast.Var.var option -> ('a, 'b) MopsaLib.man -> 'a Core.Flow.flow -> 'a MopsaLib.post

Execute the body of a case section

val exec_body : ?stub:Stubs.Ast.stub_func option -> Stubs.Ast.section list -> Framework.Core.Ast.Var.var option -> 'b -> ('a, 'c) MopsaLib.man -> 'a MopsaLib.flow -> ('a, unit) Core.Cases.cases

Execute the body of a stub

Evaluate a call to a stub

Evaluate an otherwise expression

val otherwise_in_condition : MopsaLib.expr -> bool

Check if a condition contains an otherwise expression

Remove newly introduced checks

Move newly introduced checks to a new range

Entry point of expression evaluations

Computation of post-conditions

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

val exec_directive : Stubs.Ast.stub_directive -> 'a -> ('b, 'c) MopsaLib.man -> 'b Core.Flow.flow -> ('b, unit) Core.Cases.cases

Execute a global stub directive

val normalize_requirement_condition : MopsaLib.expr -> MopsaLib.expr

Normalize a requirement condition by adding missing otherwise decorations

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

Check a stub requirement

val exec : MopsaLib.stmt -> ('a, 'b) MopsaLib.man -> 'a Core.Flow.flow -> ('a, unit) Core.Cases.cases option

Handler of queries

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

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

Pretty printer

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

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