Frama-C Today, the New York Times has an homage to Peter G. Neumann. Many people cite Albert Einstein’s aphorism “Everything should be made as simple as possible but no simpler.” Only a handful however have had the opportunity to discuss the concept with the physicist over breakfast. One of those is...
Read MoreOctober is National Cyber Security Awareness Month (if you are in the United States; otherwise it is Another Country's Cyber Security Awareness Month). In celebration here is a short list of recent cyber-security failures: An iPhone user navigating to a malicious webpage can see eir personal information (address book browsing...
Read MoreOne thing leading to another, I recently ended up wondering why, according to an individual close to the situation, the C snippet below is considered defined in C99. struct X { int a[5]; } f(); int *p = f().a; printf(\%p" p); The programming Q&A website StackOverflow had never failed me...
Read MoreIf you liked my earlier proposal for a finer-grained restrict (1 2 3 4) you might like this slightly more serious proposal for named constants in C on Jens Gustedt's blog. Or not. Here is a simple test to tell if you are likely to be interested: if you can...
Read MoreIn a recent post I showed how to use Frama-C's value analysis to prove a particular liveness property true or false of a particular C program. My colleague Sébastien Bardin reliably informs me that the ideas for reducing a liveness property to a reachability property were all in the article...
Read More