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.
Frama-C (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) that is very similar in spirit to Astree.
MOPSA (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), 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.