Tag Archives: OCaml

OCaml's option -compact can optimize for code size and speed
Pascal Cuoq on 11 October 2013

The OCaml compiler can generate native code for various architectures. One of the few code generation options is named -compact: $ ocamlopt -help Usage: ocamlopt <options> <files> Options are: ... -compact Optimize code size rather than speed ... One of the effects, perhaps the only effect(?), of this option is...

Read More

A 63-bit floating-point type for 64-bit OCaml
Pascal Cuoq on 9 May 2013

The OCaml runtime The OCaml runtime allows polymorphism through the uniform representation of types. Every OCaml value is represented as a single word, so that it is possible to have a single implementation for, say, “list of things”, with functions to access (e.g. List.length) and build (e.g. these lists...

Read More

Portable modulo signed arithmetic operations
Pascal Cuoq on 26 February 2013

In a recent post, John Regehr reports on undefined behaviors in Coq! In Coq! Coq! Exclamation point! Coq is a proof assistant. It looks over your shoulder and tells you what remains to be done while you are elaborating a mathematical proof. Coq has been used to check that the...

Read More

Funny floating-point bugs in Frama-C Oxygen's front-end
Pascal Cuoq on 19 November 2012

In a previous post almost exactly one year ago before Frama-C Oxygen was released I mentioned that the then future release would incorporate a custom decimal-to-binary floating-point conversion function. The reason was that the system's strtof() and strtod() functions could not be trusted. This custom conversion function is written in...

Read More

Never forget to sanitize your input
Virgile Prevosto on 19 September 2012

This post is a follow up of this one A facetious colleague pointed out to me that the print_stmt function that is used to display the CFG in the post mentioned above behaves incorrectly when used over code that include string constants such as the one below: void f(const char...

Read More