package mopsa
Install
Dune Dependency
Authors
Maintainers
Sources
md5=9f673f79708b44a7effb3b6bb3618d2c
sha512=cb91cb428e43a22f1abbcb8219710d0c10a5b3756d0da392d4084b3b3a6157350776c596983e63def344f617d39964e91f244f60c07958695ee5c8c809a9f0f4
doc/abstraction/Abstraction/Simplified/index.html
Module Abstraction.SimplifiedSource
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 = {exec : Core.All.stmt -> 't;(*execute a statement on the pre-state
*)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
Registration
Register a new simplified domain
Find a simplified domain by its name. Raise Not_found if no domain is found
mem_simplified_domain name checks whether a simplified domain with name name is registered
Return the names of registered simplified domains