Allow let bindings in function contracts

[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)

[remi-delmas-3000]

With the new contract system based on dynamic frames it is now possible to call C functions in requires/ensures/assigns/frees clauses, the called functions are instrumented for side effects checking.

This new PR #7401 adds support for user-defined predicates based on core predicates __CPROVER_is_fresh and __CPROVER_pointer_in_range.

We could say that the inconvenience has been addressed.