sequencing

cfamily.MemoryAccess

data MemoryAccess (L : Constructs)

An access: a named variable, an lvalue through a pointer, or a call’s effect on input or output, on a variable (a global, or the object a member function is called on), or on memory elsewhere.

cfamily.CallOrder

data CallOrder

How the order of calls could change the result: not at all; through the calls’ effects on each other (the run compares the two orders); or through a call’s effect on an access outside the calls (made after the operands’ statements, in neither order: noted, not compared).

cfamily.CallOrder.join

def CallOrder.join (a : CallOrder) (b : CallOrder) : CallOrder

The stronger of a and b (an access outside the calls outweighs the calls).

cfamily.Clash

data Clash (L : Constructs)

What two unsequenced groups of accesses lead to: certainly the same object (undefined behavior), or pairs of lvalues to compare at run time and how the order of calls could change the result.

cfamily.Clash.none

def Clash.none {L : Constructs} : Clash L

No clash.

cfamily.MemoryAccess.isEffect

def MemoryAccess.isEffect {L : Constructs} (a : MemoryAccess L) : Bool

Whether an access is a call’s effect.

cfamily.TypedExpr.storageVariable

def TypedExpr.storageVariable {L : Constructs} (lv : TypedExpr L) : Option DeclId

The variable whose own storage the lvalue lv certainly is in: a variable, its member, an element of an array variable (out of its bounds is undefined behavior, checked when made); none for what a pointer reaches.

cfamily.TypedExpr.pointedVariable

def TypedExpr.pointedVariable {L : Constructs} (p : TypedExpr L) : Option DeclId

The variable whose own storage the pointer p certainly points into: an array’s decay, the address of an lvalue, an offset of either.

cfamily.TypedExpr.inStorageOf

def TypedExpr.inStorageOf {L : Constructs} (x : DeclId) (lv : TypedExpr L) : Bool

Whether the lvalue lv is certainly in the storage of the variable x.

cfamily.MemoryAccess.effectClashes

def MemoryAccess.effectClashes {L : Constructs} (w : MemoryAccess L) (a : MemoryAccess L) : Bool

Whether a call’s effect w clashes with the access a: a variable’s effect with the variable, or with an lvalue certainly in its storage (an element, a member; what a pointer reaches is not compared with a variable’s effect).

cfamily.Clash.ofPair

def Clash.ofPair {L : Constructs} (w : MemoryAccess L) (a : MemoryAccess L) : Clash L

What a write w and an access a, unsequenced, lead to.

cfamily.Clash.join

def Clash.join {L : Constructs} (a : Clash L) (b : Clash L) : Clash L

Both clashes.

cfamily.Clash.ofWrite

def Clash.ofWrite {L : Constructs} (w : MemoryAccess L) (xs : List (MemoryAccess L)) (c : Clash L) : Clash L

What a write w leads to with accesses xs, joined onto c.

cfamily.Clash.ofWrites

def Clash.ofWrites {L : Constructs} (ws : List (MemoryAccess L)) (xs : List (MemoryAccess L)) : Clash L

What writes ws lead to with accesses xs.

cfamily.Clash.of

def Clash.of {L : Constructs} (writesA : List (MemoryAccess L)) (readsA : List (MemoryAccess L)) (writesB : List (MemoryAccess L)) (readsB : List (MemoryAccess L)) : Clash L

What two unsequenced groups (writes and reads of each) lead to: one’s writes against the other’s writes and reads.

cfamily.Clash.some

def Clash.some {A : Type} (xs : List A) : Bool

Whether the list xs has something.

cfamily.Clash.statements

def Clash.statements {L : Constructs} (n : NodeId) (c : Clash L) (first : List (TypedStmt L)) (second : List (TypedStmt L)) (after : List (TypedStmt L)) : List (TypedStmt L)

The statements of two unsequenced groups (first’s, then second’s) and those after both, with the checks of their clash: undefined behavior when certain; else both orders of the groups’ statements if calls’ effects could clash (bothOrders: the run compares them), or a note that the orders were not compared if a call’s effect could clash with an access outside the calls; and each pair of lvalues compared at run time after them.