Tag Archives: value-eva

A simple Eva tutorial, part 3
André Maroneze on 11 April 2017

On the previous post we’ve seen how to run Eva, but at the end we had a NON TERMINATING FUNCTION for a function that is supposed to always terminate, a likely indication that a definitive undefined behavior has been found in the analysis. In this post, we will see how...

Read More

A simple Eva tutorial, part 2
André Maroneze on 17 March 2017

On the previous post we’ve seen some recommendations about using Frama-C/Eva, and some tips about parsing. In this post, we will see how to run Eva, and how to quickly setup it for a more precise result. We will reuse the save file produced at the end of the parsing,...

Read More

A simple Eva tutorial, part 1
André Maroneze on 7 March 2017

(with the collaboration of T. Antignac, Q. Bouillaguet, F. Kirchner and B. Yakobowski) This is the first of a series of posts on a new Eva tutorial primarily aimed at beginners (some of the later posts contain more advanced content). Reminder: Eva is the new name of the Value analysis...

Read More

Frama-C Silicon has been released!
André Maroneze on 13 December 2016

Frama-C 14 (Silicon) has just been released. In this post, we present a few additions that should help everyday usage of Value EVA. Value is now EVA The Value analysis plug-in has been renamed EVA, for Evolved Value Analysis. It has a new architecture that allows plugging abstract domains, among...

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