5 ms·
Check out KCC, too, since the foundation is open-source, offers extra benefits for languages modeled in it, and has a commercial tool for C with either low or n
by nickpsecurity 9y ago
Check out KCC, too, since the foundation is open-source, offers extra benefits for languages modeled in it, and has a commercial tool for C with either low or no false positives depending on how it measures up to claims. No affiliation. I just find the K framework plus an executable, formal semantics for C cool as heck. :)
https://github.com/kframework/c-semantics https://github.com/kframework/c-semantics
https://runtimeverification.com/match/ https://runtimeverification.com/match/
They also have an article comparing it to Tis-interpreter here:
https://runtimeverification.com/blog/?p=307 https://runtimeverification.com/blog/?p=307
Their K has been used for languages from Scheme to Prolog to C. More recently, they also did a semantics for a VM for smart contracts. They're doing a lot of interesting stuff. Builds on Maude and rewriting logic if anyone is curious.
- dhekir 9y agotis-interpreter also has an open-source foundation, which is Frama-C (http://www.frama-c.com http://www.frama-c.com). Both share some common code. Their purpose is not exactly the same as RV-Match's; they are more concerned with soundness and absence of run-time errors (as well as other properties and analyses), while RV-Match is a bug detection tool, focusing on not having false positives. It's important to realize the difference when comparing such kinds of tools. Depending on the situation, one is more appropriate than the other, but in some cases the results may be complementary (as in RV-Match's comparison, where the reported bugs were different for each of them), so if there's already some effort to try one of them (plus the *San's from LLVM), it may be worth trying the others as well. Every bit of help is welcome when dealing with a language such as C. Disclaimer: I work with Frama-C.