Frama-C (with the collaboration of F. Kirchner, V. Prevosto and B. Yakobowski) Users of the Value plugin often need to use functions for which there is no available code, or whose code could be abstracted away. In such cases, ACSL specifications often come in handy. Our colleagues at Fraunhofer prepared the...
Read MoreThe Frama-C GUI received a few quality-of-life improvements that have not been announced during the Magnesium release. This post presents some of them, along with general GUI tips. We focus on general-purpose UI improvements, while another post will discuss new Value-specific features, related to the new Values tab. These UI...
Read MoreThe Frama-C blog is back, with an extended set of writers and a different focus: small pieces of (informal) documentation and useful tips for Frama-C users. During its self-awareness period, the Frama-C blog realized that silence is a valid option, sometimes better than the alternatives. Still, we thought better to...
Read MoreA reader's challenge A couple of days ago, faithful reader David Gil sent in a challenge: The reference code for Keccak/SHA-3 has a correctness bug in the Optimized64 implementation. Can the value analysis plugin find it? My patch fixing that bug was accepted; I believe that the trunk is correct...
Read MoreA buffer overflow has been discovered in recent versions of the HTTP server Nginx. Hacker News user jmnicolas pondered out loud: “I wonder if this discovery is a result of OpenBSD switching its focus from Apache to Nginx?” It took me one minute to understand what ey meant. I was...
Read More