Frama-C 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 MoreThis 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 MoreContext 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 MorePrologue 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