Skip to content

CBMC: Remove union/struct workaround (CBMC issue #8813) #826

@mkannwischer

Description

@mkannwischer

#818 introduced MLK_UNION_OR_STRUCT (should be MLD_UNION_OR_STRUCT) as a workaround for diffblue/cbmc#8813. It uses a struct by default (which works fine with CBMC), but switches to a union when MLD_CONFIG_REDUCE_RAM is set.
Once the issue is fixed in CBMC, we should remove the workaround, i.e.,

  • Remove MLK_UNION_OR_STRUCT
  • Use union everywhere
  • Adjust the stack savings in the documentation of the config file.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions