Allow `__CPROVER_old(expr)`

[feliperodri]

CBMC version: 5.67.0
Operating system: N/A

New users would have an easier time using function contracts if users could write __CPROVER_old(expr) in requires and ensures clauses. In TLA+, it is routine to write things like (expr)' == (expr) + 1 to mean the expression increasing value by 1.

s2n_stuffer_data_available(&old_stuffer) == 0

The "natural" ensures clause in a function contract to write is

s2n_stuffer_data_available(__CPROVER_old(stuffer)) == 0

but because this is a macro

#define s2n_stuffer_data_available( s )   ((s)->write_cursor - (s)->read_cursor)

this expands to

(__CPROVER_old(stuffer))->write_cursor - (__CPROVER_old(stuffer))->read_cursor 

Because the pointer stuffer does not change, this is equivalent to

stuffer->write_cursor - stuffer->read_cursor

in the post state which is not what is intended.

What the user really wanted to write is

__CPROVER_old(s2n_stuffer_data_available(stuffer)) == 0