Blog

Tag Archives: ACSL

Assertions
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

Post-conditions and names of arguments
Pascal Cuoq on 17 January 2014

In an ACSL post-condition, any reference to the name of one of the function's arguments is assumed to refer to the initial value of the argument. /* ensures arg == 1; */ void f(int arg) { arg = 1; } For instance, in function f above, Frama-C's value analysis plug-in...

Read More

Debugging with WP
Virgile Prevosto on 6 November 2012

Initial setting So, I was checking a small demo of the WP plug-in the other day, just before making a presentation of Frama-C to some future fellow user. This was the traditional binary_search verification presented in the Berlin training session in 2010 but using the WP plugin instead of Jessie....

Read More

assume and assert
Pascal Cuoq on 3 August 2012

The previous post links to a message [removed dead link] from Michał Moskal highlighting ACSL constructs that the VCC developers at Microsoft Research had either regretted the absence of or found superfluous while re-designing their own annotation language for VCC. In that e-mail the third item in the “missing” list...

Read More

restrict is not good for modular reasoning
Pascal Cuoq on 2 August 2012

ACSL There were quite a few posts recently that were concerned with ACSL, and a few more are planned for the near future. ACSL is a specification language for C (comparable with JML for Java, for those who know about JML). Some people call it a BISL, for “Behavioral Interface...

Read More