Tag Archives: unspecified-behavior

Reading indeterminate contents might as well be undefined
Pascal Cuoq on 13 March 2013

Warning: on a punctiliousness scale ranging from zero to ten, this post is a good nine-and-a-half. There was no tag for that, so I tagged it both “C99” and “C11”. The faithful reader will know what to expect. There is a bit of C90, too. To summarize, it may appear...

Read More

When is it valid to compare two pointers in C?
Pascal Cuoq on 14 April 2011

This post is about the circumstances in which the value analysis considers comparing pointers is safe, and those in which it considers the comparison is dangerous and emits an alarm. The alarm, an enigmatic assert \pointer_comparable(…, …);, uses an unaxiomatized ACSL predicate. If you use the value analysis regularly, you...

Read More

Unspecified behaviors and derived analyses, part 2
Pascal Cuoq on 4 December 2010

Context This post is a sequel and conclusion to this remark. Example of derived analysis: slicing When writing a Frama-C plug-in to assist in reverse-engineering source code it does not really make sense to expect the user to check the alarms that are emitted by the value analysis. Consider for...

Read More

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