Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package bap-core-theory
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Effect sorts.
The sort of an effect holds static information that is common to all effects of that sort.
We distinguish two kinds of effects - ctrl effects that affect which instructions will be executed next and data effects that affect only the values in the computer storage.
The unit effect represents an effect that is a mixture of ctrl and data effects.
type +'a t = 'a sortval top : unit ttop is a set of all possible effects.
This sort indicates that the statement can have any effect.
val bot : 'a tbot is an empty set of effects.
This sort indicates that the statement doesn't have any observable effects, thus it could be coerced to any other sort.
val order : 'a t -> 'b t -> KB.Order.partialorder xs ys orders effects by the order of inclusion.
xs is before ys if ys includes all effects of xs, otherwise.