Frama-C La critique du langage ne peut éluder ce fait que nos paroles nous engagent et que nous devons leur être fidèles. — Albert Camus This post was originally written for the SecOPERA project’s blog. A crucial, but often neglected aspect of formal software evaluation process, is how we specify the...
Read MoreMotivated by some recent discussions concerning a hard-to-parse code base, this post presents a few techniques used by Frama-C developers to quickly understand and debug parsing-related errors. We are constantly improving parsing and error messages, so hopefully some of these tips will become unnecessary in the future. Origin of parsing...
Read MoreThis page redirects to the Frama-C Days 2024 Slides Gallery
Read MoreAfter 5 years of absence, the Frama-C Days are back! On June 13 and 14, will be held the Frama-C Days at Maison de la Radio et de la Musique in Paris. What to expect? Many exciting interventions from both academic and industrial users of the Frama-C environment, for sharing...
Read MoreA machdep (for machine-dependent) in Frama-C is a set of architecture-specific configurations, which include: integer sizes, predefined macros, compiler type, standard library constants, etc. They are essential when analyzing embedded, non-portable code. Thanks to some C11 features, the machdep generation mechanism has been revised in Frama-C, allowing users to more...
Read More