|
|
|---|
|
|
|
|---|
Removal of flexible array members.
When a structure with a flexible array member is copied, as in most other uses of structures with flexible array members, the flexible array member is ignored [C:6.7.2.1/18]. This means that, when the structure is copied (e.g. in an assignment), the flexible array member is dropped.
Here we introduce an ACL2 function to do that. This function operates on all values, leaving them unchanged unless the value is a structure with a flexible array member. By operating over all values, this function can be used uniformly when values are copies.