Frama-C I do not expect that many people are diligently working at this time of year, and this is my excuse for posting this series of productivity-wasting links. Some of them are even on-topic. For those who missed it, GNU/Linux Magazine/France has a summer special [removed dead link] on the C...
Read MoreThis post follows that post where a typical double-precision implementation for a cosine function is shown. That implementation is not a correctly rounded implementation but its double result is precise to a level close to what the double-precision floating-point representation allows. It uses low-level tricks that make it faster on...
Read MoreWhen picking up the title for the previous post on function memcpy I anticipated this second part would describe the Frama_C_memcpy built-in function. The subtitle "part 1: the source code approach" seemed a good idea since the first part was about using C source code to tell the analyzer what...
Read MoreEvery once in a while, someone asks about single-precision floating-point support in Frama-C. Until recently it was often in the context of the value analysis, but actually, thanks to a lot of interesting new results obtained in the context of this project people working on deductive verification within Frama-C can...
Read More