layout

cfamily.Ty.complete

def Ty.complete {L : Constructs} (ext : TypeExtension L) (tgt : Target) (g : Globals L) (t : Ty L) : Ty L

Completes a type: each struct or union name is looked up at most as many times as there are definitions.

cfamily.Ty.tagName

def Ty.tagName {L : Constructs} (t : Ty L) : String

The name of a struct or union type (complete or not), else the empty string.

cfamily.Ty.roundUp

def Ty.roundUp (x : Nat) (a : Nat) : Nat

x rounded up to a multiple of a (a is at least 1).

cfamily.BitField

record BitField

A bit-field’s width and the width of its type’s unit.

cfamily.Ty.bitFieldOf

def Ty.bitFieldOf {L : Constructs} (tgt : Target) (t : Ty L) : Option BitField

Whether a type is a bit-field’s: an integer type narrower than its rank’s (C11 6.7.2.1p10).

cfamily.Placement

data Placement

How a struct member is placed: whole (size and alignment in bytes), or as a bit-field (width and unit in bits, and whether it is named: an unnamed one does not align the struct).

cfamily.Ty.bytesOf

def Ty.bytesOf (width : Nat) : Nat

The bytes of a width in bits, at least 1 (bool is one byte).

cfamily.Ty.startOf

def Ty.startOf (offset : Nat) (m : Placement) : Nat

Where a member placed after an offset in bits starts (the System V ABI): a whole member at its alignment; a bit-field where the last one ended unless it would cross its unit, then at the next unit; width 0 at the next unit.

cfamily.Placement.bits

def Placement.bits (m : Placement) : Nat

The bits a member takes: a whole member’s bytes, a bit-field’s width.

cfamily.Ty.placeAll

def Ty.placeAll (offset : Nat) (members : List Placement) : Nat

The end in bits of members placed in order from an offset in bits.

cfamily.Ty.startsFrom

def Ty.startsFrom (offset : Nat) (members : List Placement) : List Nat

Where in bits each of the members placed in order from an offset starts.

cfamily.Placement.align

def Placement.align (m : Placement) : Nat

A member’s alignment in bytes (an unnamed bit-field’s is 1).

cfamily.Ty.maxAlign

def Ty.maxAlign (members : List (Nat * Nat)) : Nat

The greatest alignment among members, at least 1.

cfamily.Ty.structLayout

def Ty.structLayout (members : List Placement) : Nat * Nat

A struct’s layout: members in order, the size rounded up to the greatest alignment.

cfamily.Ty.unionLayout

def Ty.unionLayout (members : List (Nat * Nat)) : Nat * Nat

A union’s layout: the largest member, rounded up to the greatest alignment.

cfamily.Ty.layout

def Ty.layout {L : Constructs} (ext : TypeExtension L) (tgt : Target) (g : Globals L) (t : Ty L) : Nat * Nat

The size and alignment of a type: the dialect’s own layout if it has one for the type, else the C rules.

cfamily.Ty.size

def Ty.size {L : Constructs} (ext : TypeExtension L) (tgt : Target) (g : Globals L) (t : Ty L) : Nat

The size of a type in bytes.

cfamily.Ty.align

def Ty.align {L : Constructs} (ext : TypeExtension L) (tgt : Target) (g : Globals L) (t : Ty L) : Nat

The alignment of a type in bytes.