Tag Archives: value-builtins

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