Tag Archives: OCaml

Holiday stuff
Pascal Cuoq on 8 August 2011

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 More

This time for real: verifying function cosine
Pascal Cuoq on 3 March 2011

This 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 More

On memcpy (part 2: the OCaml source code approach)
Pascal Cuoq on 31 January 2011

When 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 More

IEEE 754 single-precision numbers in Frama-C
Pascal Cuoq on 20 November 2010

Every 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