Tag Archives: ACSL

Frama-C and ACSL are on GitHub
André Maroneze on 22 November 2016

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: It contains snapshots of...

Read More

A mini ACSL tutorial for Value, part 3: indirect assigns
André Maroneze on 12 October 2016

To 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 More

A mini ACSL tutorial for Value, part 2: functional dependencies
André Maroneze on 30 September 2016

In 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

A mini-tutorial of ACSL specifications for Value
André Maroneze on 23 September 2016

(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 More

Pascal Cuoq on 4 February 2014

Jesse 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