3 ms·
It is a shame that there is no open source equivalent to tools like Astree: https://www.absint.com/astree/index.htm https://www.absint.com/astree/index.htm In
by ryao 3y ago
It is a shame that there is no open source equivalent to tools like Astree:
https://www.absint.com/astree/index.htm https://www.absint.com/astree/index.htm
In theory, it is possible to write completely memory safe code in C/C++ using it. As long as its analysis generates no complaints, there are no memory safety issues in the analyzed code.
- deely3 3y agoCan I ask a strawman/obvious question? Does developers of most complex systems use this tool, and if not, then why?
- edwcross 3y agoI beg to differ: there are a few tools which are comparable. Frama-C (https://www.frama-c.com https://www.frama-c.com) is an open source framework that has, among its analyzers, one based on abstract interpretation (https://www.frama-c.com/fc-plugins/eva.html https://www.frama-c.com/fc-plugins/eva.html) that is very similar in spirit to Astree. MOPSA (https://mopsa.lip6.fr https://mopsa.lip6.fr) is another open-source project (albeit more recent, and in a more "academic" stage) that also provides abstract interpretation to analyze C programs for flaws. NASA also released IKOS (https://github.com/NASA-SW-VnV/ikos https://github.com/NASA-SW-VnV/ikos), on the same vein. Of course they lack the polish of a product which costs tens of thousands of euros per license, but they are open source, and their purpose is the same: to ensure code safety via formal methods, in particular abstract interpretation. It is possible to get these tools to analyze some code and generate no complaints, which ensures absence of several kinds of problems, such as memory safety issues. Then again, it's hard to know exactly how much they differ from Astree, since you need a license to compare them, and I don't even know if you are allowed to publish such comparisons.