Skip to content

Pack CAR validity var, lower bound and upper bound in a single struct object #7198

Closed
@feliperodri

Description

@feliperodri

CBMC version: 5.67.0
Operating system: N/A

Function and loop contract instrumentation introduces three variables (car_valid, car_lb, car_ub) for each target specified in the assigns clause, for each local declaration, and for each assignment lhs. This greatly augments the number of objects created by CBMC during SymEx, and the number of object bits to use for pointers during the analysis.

Packing the three variables in a single struct would reduce the number of objects by 3 and save us one object bit.

Metadata

Metadata

Labels

Code ContractsFunction and loop contractsawsBugs or features of importance to AWS CBMC usersenhancement

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions