Skip to content

Allow let bindings in function contracts #7201

Closed
@feliperodri

Description

@feliperodri

CBMC version: 5.67.0
Operating system: N/A

For readability by naive readers, and even for hardened pros, we need to allow let bindings in function contract expressions for easy-to-read contracts.

size_t expected_length = (expected != NULL) ? strlen(expected) : 0;
if ( ... S2N_SUCCESS ...) {
     uint8_t *actual = stuffer->blob.data + stuffer->read_cursor - expected_length;
     assert(!memcmp(actual, expected, expected_length));
}

among other things. The ensure clause should be something like

__CPROVER_ensures(!memcmp(actual, expected, expected_length))

Without lets, the best we can do is in-place expansion of both expressions (unreadable: notice that the double nesting of expected_length in this expression) or approximate the lets with preprocessor defines

#define EXPECTED_LENGTH ((expected != NULL) ? strlen(expected) : 0)
#define ACTUAL (stuffer->blob.data + stuffer->read_cursor - EXPECTED_LENGTH)

Metadata

Metadata

Assignees

Labels

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

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions