Tag Archives: value

Unspecified behaviors and derived analyses
Pascal Cuoq on 17 October 2010

Prologue The C standard(s) specifies a minimum of things that all C compilers must agree on. For the sake of efficiency, many syntactically correct constructs are left without an unambiguous meaning. The worst way for a construct not to have an unambiguous meaning is to be undefined behavior. An example...

Read More

Value analysis tutorial, part 3: answering one quiz
Pascal Cuoq on 15 October 2010

This is another episode in the advanced value analysis tutorial. The first episode was here and the second one here. There were a couple of questions left unanswered at the break. This post answers the first one. Quiz 1: continuing the study of the first five calls to Skein_256_Update what...

Read More

Value analysis tutorial, part 2
Pascal Cuoq on 7 October 2010

In order to create a tradition of providing solutions to previous quizzes, this post is a partial answer to the question in this one about Frama-C's value analysis. To recap: at the end of the Boron tutorial we arrive at the main function below. This function is useful as an...

Read More

Progress of the value analysis tutorial
Pascal Cuoq on 30 September 2010

Boron's value analysis manual has the beginning of a captivating tutorial and I figure that the suspense must be unbearable. I on the other hand already know how it ends. But I'm not telling yet. Neener-neener! Okay maybe later on this blog. The new manual (with an expanded tutorial) will...

Read More