News for hackers. Stuff that matters.

A comment on Frama-C: Modular Analysis of C Programs. Parent comment

Re:Frama-C: Modular Analysis of C Programs by mcguire on Tuesday October 06, 2020 @12:13PM (#24699314)
What's the status of handling manual memory management? The last time I looked, that was a huge, gaping hole in both Spark and Frama-C provers.
[ Parent | on HN ]
Re:Frama-C: Modular Analysis of C Programs by KsassPeuk on Wednesday October 07, 2020 @02:57AM (#24705926)
It depends on the verification tool you use.

Eva (the abstract interpreter) has different ways to model dynamic allocation. It is thus a tradeoff to find between precision and computation time.

WP does not have dynamic allocation support. This is an ongoing work, but it will not be available in the next release. Note that there are different ways to model the behavior of dynamic allocation, generally via axiomatic definitions and/or ghosts.

[ Parent | on HN ]