Frama-C In 2016, a few blog posts (part 1, part 2, part 3) presented a short tutorial on writing ACSL clauses for Eva (back then, the Value Analysis plug-in). A few things changed since then, but posting them again in this blog would lead to the same issue in the future....
Read MoreIn Frama-C 23 (Vanadium), two new kinds of ACSL annotations are available, to complement assert: the admit and check annotations. In a nutshell, assert P is equivalent to check P; admit P. The former allows easier checking of the validity of predicates, while the latter documents the introduction of external...
Read MoreWe 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