package soteria

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

Module Sym_states.Pure_fun

State model component of pure functions. A piece of state represents a function `f()` that returns a value in a certain set. It is quite similar to the agreement algebra, except that there is no allocation, there necessarily exists a value, and if we don't know it, we instantiate it on read/consumption.

module Codom (Symex : Symex.Base) : sig ... end

FIXME: This is almost verbatim the same thing as the input of excl

module Make (Symex : Symex.Base) (C : Codom(Symex).S) : sig ... end