Frama-C If I told you that when n is a positive power of two and d an arbitrary number, both represented as double, the condition (n - 1) * d + d == n * d in strictly-IEEE-754-implementing C is always true, would you start looking for a counter-example, or start...
Read MoreNearly 15 months ago, according to a past article, this blog celebrated its 15-month anniversary, and celebrated with the announcement of minor milestones having been reached: 100 articles and 50 comments. Fifteen months after that, the current count is nearly 200 articles and 200 comments. Also, the blog managed to...
Read MoreThe 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. List.map) these lists...
Read MoreCorrect and wrong definitions for the constant FLT_EPSILON If I google “FLT_EPSILON”, the topmost result is this page with this definition: FLT_EPSILON the minimum positive number such that 1.0 + FLT_EPSILON != 1.0. No no no no no. I don't know where this definition originates from but it is obviously...
Read MoreTwo earlier posts showed two different approaches in order to round a float to the nearest integer. The first was to truncate to integer after having added the right quantity (either 0.5 if the programmer is willing to take care of a few dangerous inputs beforehand or the predecessor of...
Read More