model-checking

We should introduce a flag (and an associated proof harness annotation) to enable --malloc-can-fail in CBMC.

At first, this might seem useless, because many std data structures will simply panic on allocation failure. (And without #692, this just means all such proof harnesses would just have failures that are unavoidable.)

But there is no-std Rust code out there that might be very int

The TlaDocumentSymbolsProvider stumbles on operators while parsing constants and doesn't report them as model symbols. As a result, const operator names don't appear in the outline panel and in completion suggestions. Such operators also prevent parsing of the following constants.

A simple case:

CONSTANT Foo(_), Bar

Neither Foo nor Bar makes it to the model symbols list

There are several unused parameter warnings all over the place.

As these parameters mostly exist on purpose (e.g. for function overloading), those warnings can probably be ignored.
Once we are at c++17, we should insert the new attribute [[maybe_unused]] wherever this is the case.