Can I easily exclude some contracts from static analysis?

Question

There are certain contracts that I know that a static analyzer cannot prove. I can exclude some kinds of contract violation errors from the whole function, but this is too wide. I can eliminate some violation errors using the functionality of baseline.xml, although this is almost impossible to verify or document in a command environment.

In short, is it possible to do something like

Contract.Requires(DoesHalt() == true, ExcludeFromStaticAnalysis=true);

There are also certain contracts in third-party libraries, which, apparently, are dead ends for a static analyzer. I would like to disable them for static analysis. One of my favorite examples is a contract built for the .NET charting library. The argument of the first depth search function, which determines which vertex in the graph to start the search has a Contract.Requires , which requires that the vertex be a member of the graph. A reasonable contract might even be worthwhile in a debug build, but far from being statically provable. But every time I use the first depth search, I have to find a way to ignore the static violation. (It is not allowed using Contract.Assume )

Without the ability to break provable things out of unprovable things, I find that static analysis is just too noisy, even with a small, clean code base.

Answer 1

For static analysis, I do not know how to do this. The runtime checker has a custom runtime with which it would be possible, but not for static checking.

What you can do is use basic functionality . This gives you the ability to hide all warnings that static checkers give you at a specific time. These warnings are collected in an XML file until you disable basic functions.

This can significantly reduce static verification noise for an existing code base.