I've put together a simple checker that throws no warnings, but models some library functions, which has already helped us to suppress some false positives in other checkers in our runs.
For pure functions, i chose the old evalCall() approach instead of the body-farm approach because i wanted to produce less state splits. For example, this checker produce a single exploded graph branch for ispunct()'s non-zero branch, when its argument is in range:
['!', '/'] U [':', '@'] U ['[', '\`'] U ['{', '~']
I'm not sure if there's a way to write this out with if's and produce less than 4 branches. (Do we have any plans on merging branches more aggressively during analysis?) Because these functions are pure, we'd hardly ever want to catch them with`evalCall()` again in another checker.
Additionally, this checker's brace-initializers for function specifications are quite short - of course they're limited to very simple cases - the list of these cases can be expanded though.
The checker doesn't seem to be noticeably degrading performance. Here's an example of a false positve squashed:
Here line is taken to be "", the line++ statement is executed at least once (by looking at the exploded graph; there's lack of "entering loop body" diagnostic piece because loop condition has complicated CFG, which is why it fails to highlight - a separate issue), and the analyzer fails to realize that isspace('\0') is false.