Tag Archives: link

Google forking WebKit
Pascal Cuoq on 4 April 2013

Blink as seen from the inside As you have undoubtedly heard if you follow at all this sort of thing, as of April 3, Google is forking WebKit. Its Chrome browser will henceforth rely on its own variation of the popular rendering engine, Blink. This is big news. If I...

Read More

Reading indeterminate contents might as well be undefined
Pascal Cuoq on 13 March 2013

Warning: on a punctiliousness scale ranging from zero to ten, this post is a good nine-and-a-half. There was no tag for that, so I tagged it both “C99” and “C11”. The faithful reader will know what to expect. There is a bit of C90, too. To summarize, it may appear...

Read More

Correct rounding or mathematically-correct rounding?
Pascal Cuoq on 3 March 2013

CRlibm is a high-quality library of floating-point elementary functions. We used it as reference a long time ago in this blog while looking at lesser elementary function implementations and the even lesser properties we could verify about them. A bold choice The CRlibm documentation contains this snippet: […] it may...

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

From Facebook to Silent Circle, through the “metrics” Frama-C plug-in
Pascal Cuoq on 16 February 2013

From Facebook to Silent Circle Some computers at Facebook were recently compromised because of a zero-day in Java. Nothing unexpected. Last december instead of writing a full blog post I lazily linked to Robert Graham predicting this sort of thing for the year 2013. Speaking of Facebook do you know...

Read More