package mopsa

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

Simplified domains

The signature SIMPLIFIED provides a minimal interface to implement abstract domains that don't require communication with other domains. This is particularly useful for abstractions that are at the leaves of the abstraction DAG.

Lattice operations and transfer functions operate on the abstract element of the domain without being able to access to the top-level abstraction. The manager is therefore not accessible, only a simplified version is provided that can be used to perform queries on the pre-state.

Simplified manager

type ('a, 't) simplified_man = {
  1. exec : Core.All.stmt -> 't;
    (*

    execute a statement on the pre-state

    *)
  2. ask : 'r. ('a, 'r) Core.All.query -> 'r;
    (*

    ask a query on the pre-state

    *)
}

Simplified managers provide access to the pre-state and can be used to perform queries or execute statements.

Signature

module type SIMPLIFIED = sig ... end

Registration

val register_simplified_domain : (module SIMPLIFIED) -> unit

Register a new simplified domain

val find_simplified_domain : string -> (module SIMPLIFIED)

Find a simplified domain by its name. Raise Not_found if no domain is found

val mem_simplified_domain : string -> bool

mem_simplified_domain name checks whether a simplified domain with name name is registered

val simplified_domain_names : unit -> string list

Return the names of registered simplified domains

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