Documentation
¶
Index ¶
- func BinOp(mem L.Memory, v1, v2 L.AbstractValue, ssaVal *ssa.BinOp) (result L.AbstractValue)
- func Close(val L.AbstractValue) L.OpOutcomes
- func CondWait(val L.AbstractValue) L.OpOutcomes
- func CondWake(val L.AbstractValue) L.OpOutcomes
- func FlatReceive(ZERO L.AbstractValue, commaOk bool) valueTransfer
- func FlatSend(payload L.AbstractValue) valueTransfer
- func IntervalReceive(ZERO L.AbstractValue, commaOk bool) valueTransfer
- func IntervalSend(payload L.AbstractValue) valueTransfer
- func Load(v L.AbstractValue, mem L.Memory) (res L.AbstractValue)
- func Lock(val L.AbstractValue) L.OpOutcomes
- func RLock(val L.AbstractValue) L.OpOutcomes
- func RUnlock(val L.AbstractValue) L.OpOutcomes
- func SwapWildcard(pt *pointer.Result, mem L.Memory, l loc.AddressableLocation) L.Memory
- func Sync(commaOk bool) valueTransfer
- func ToDeref(v L.AbstractValue) L.OpOutcomes
- func TypeAdapter(from, to T.Type, v L.AbstractValue) L.AbstractValue
- func UnOp(v L.AbstractValue, ssaVal *ssa.UnOp) (result L.AbstractValue)
- func Unlock(val L.AbstractValue) L.OpOutcomes
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func BinOp ¶
func BinOp(mem L.Memory, v1, v2 L.AbstractValue, ssaVal *ssa.BinOp) (result L.AbstractValue)
func CondWait ¶
func CondWait(val L.AbstractValue) L.OpOutcomes
Models stepping into .Wait() calls. Any .Wait() call involves checking whether the associated mutex may be locked. If the mutex may be unlocked, then executing .Wait() might result in a fatal exception.
func CondWake ¶
func CondWake(val L.AbstractValue) L.OpOutcomes
Called when a thread tries to wakes up either from a call to .Signal() or .Broadcast(). Checks whether the associated mutex may be unlocked, in which case waking will succeed.
func FlatReceive ¶
func FlatReceive(ZERO L.AbstractValue, commaOk bool) valueTransfer
func FlatSend ¶
func FlatSend(payload L.AbstractValue) valueTransfer
Abstract transformation on a single channel abstract buffer element.
func IntervalReceive ¶
func IntervalReceive(ZERO L.AbstractValue, commaOk bool) valueTransfer
func IntervalSend ¶
func IntervalSend(payload L.AbstractValue) valueTransfer
func Load ¶
func Load(v L.AbstractValue, mem L.Memory) (res L.AbstractValue)
func Lock ¶
func Lock(val L.AbstractValue) L.OpOutcomes
func RLock ¶
func RLock(val L.AbstractValue) L.OpOutcomes
func RUnlock ¶
func RUnlock(val L.AbstractValue) L.OpOutcomes
func SwapWildcard ¶
Swap a wildcard value with the result of the upfront analysis. Produces a memory where the value has been updated.
func Sync ¶
func Sync(commaOk bool) valueTransfer
Model synchronization between synchronous channels.
func ToDeref ¶
func ToDeref(v L.AbstractValue) L.OpOutcomes
Get all the locations that could be dereferenced
func TypeAdapter ¶
func TypeAdapter(from, to T.Type, v L.AbstractValue) L.AbstractValue
Adapt types for implicit/permissive type coercions allowed by Golang
func UnOp ¶
func UnOp(v L.AbstractValue, ssaVal *ssa.UnOp) (result L.AbstractValue)
func Unlock ¶
func Unlock(val L.AbstractValue) L.OpOutcomes
Types ¶
This section is empty.
Source Files