Frama-C We are glad to announce the creation of official GitHub repositories for Frama-C and ACSL, to stimulate contributions from the community, and to better contribute back to it. Frama-C is on GitHub Frama-C now (in fact, since a few months) has an official GitHub repository: https://github.com/Frama-C/Frama-C-snapshot It contains snapshots of...
Read MoreTo conclude our 3-part series on ACSL specifications for Value, we present a feature introduced in Frama-C Aluminium that allows more precise specifications: the indirect label in ACSL assigns clauses. The expressivity gains when writing \froms are especially useful for plugins such as Value. Indirect assigns Starting in Frama-C Aluminium...
Read MoreIn our previous post, we left you in a cliffhanger: which \from is missing from our ACSL specification for safe_get_random_char? In this post, we explain the functional dependencies in our specification, how to test them, and then present the missing dependency. Where do the \from come from? Our complete specification...
Read More(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 MoreJesse Ruderman on assertions and fuzzing Jesse Ruderman has published a blog post on assertions and how they complement fuzzing. Key quote: “Fuzzers make things go wrong. Assertions make sure we find out.” Readers of this blog are accustomed to me talking about differential testing where a reference result (say...
Read More