|
|
|---|
|
|
|
|---|
Fixtype of values.
This is a tagged union type, introduced by fty::deftagsum.
For now we only support the standard unsigned and signed integer values
(except
As mentioned in pointer, we define a pointer value as consisting of a pointer (as defined there) and a type. Note that [C17] does not prescribe 0 to represent a null pointer, even though 0 is used in null pointer constants [C17:6.3.2.3/3]. The type is not the pointer type, but the referenced type; this way, we avoid having to constrain the type to be a pointer type.
Array values are modeled as consisting of the element type and a non-empty list of values. [C17:6.2.5/20] requires arrays to be non-empty.
Arrays are indexed via integers [C17] only provides minimum requirements for the sizes of integer types, not maximum requirements. Other than practical considerations, nothing, mathematically, prevents some integer types to consists of thousands or millions of bits. So our model of arrays requires them to be non-empty, but puts no maximum limits on their length.
This definition of arrays alone does not prevent arrays from having values of different types. That all the values have the element type can and will be enforced in separate predicates.
Structures are modeled as consisting of a tag (identifier), a non-empty list of member values, and a flag saying whether the structure has a flexible array member [C17:6.7.2.1/18]. The tag is the one that identifies the structure type; we only model structures with non-anonymous types. [C17:6.2.5/20] requires at least one member, which we capture with an invariant. If the flexible array member flag is set, there must be at least two members (i.e. one besides the flexible array member), and the last member must be an array; we do not capture these requirements here, but we may in the future. The member values must have distinct names; we do not capture this requirement here, but we may in the future.
The requirement that the member values match the members of the structure type requires contextual information about the structure type. So this requirement cannot be captured in this definition of values.