Code contracts in CBMC provide way to safely abstract parts of a program, typically in order to accelerate the verification process. The key idea is to overapproximate the possible set of program states, while still being precise enough to be able to prove the desired property.

To learn more about contracts, take a look at the chapter Design by Contract from the book Object-Oriented Software Construction by Bertrand Meyer or read the notes Contract-based Design by George Fairbanks.

For extra steps required to compositionally reason about file-local functions [please consult this link](todo-link-to-cprover-manual-static-functions).