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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct