Upgrading the CBMC version to 5.59.0 caused regression failures related to missing functions. These are now failing with the description "assertion", apparently because they do not include source locations.
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.
Upgrading the CBMC version to 5.59.0 caused regression failures related to missing functions. These are now failing with the description "assertion", apparently because they do not include source locations.