Hacker News Reader

And vice versa; Frama-C doesn't attempt to prove the absence of data races, last I checked.

In fact there exists a plugin that can do that but it is currently not free:

(And by the way since it is not done by typing it is hard to use on legacy code)