From 358f880cc5c65bc6ef083ac1e5397e18ffd0fcce Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Thu, 12 Nov 2020 15:22:20 +0000 Subject: [PATCH] More updates. --- 2020-frama-c/9200-alternatives.html | 2 ++ 2020-frama-c/notes.txt | 33 +++++++++++++++------------------ 2 files changed, 17 insertions(+), 18 deletions(-) diff --git a/2020-frama-c/9200-alternatives.html b/2020-frama-c/9200-alternatives.html index f594042..5969c22 100644 --- a/2020-frama-c/9200-alternatives.html +++ b/2020-frama-c/9200-alternatives.html @@ -17,4 +17,6 @@
  • CompCert is INRIA's verified C compiler (not open source). + +
  • RefinedC diff --git a/2020-frama-c/notes.txt b/2020-frama-c/notes.txt index b7254f7..7cb905c 100644 --- a/2020-frama-c/notes.txt +++ b/2020-frama-c/notes.txt @@ -1,7 +1,7 @@ -16th Nov 2020 +Monday 16th Nov 2020 Formally proving tiny bits of qemu using Frama-C -[in medias res] + In early October I was talking to one of the developers of Frama-C, which is a modular framework for verifying C programs. It's been on @@ -14,6 +14,19 @@ tool. I will provide links to tutorials etc at the end. += OVERVIEW OF FRAMA-C ECOSYSTEM = + +The name stands for "Framework for Static Analysis of the C language". + +It's modular, with a core program that reads C source code +and turns it into Abstract Syntax Trees. And a set of plugins +to do static analysis by annotating these syntax trees. +Plugins can cooperate, so analysis can be passed between +plugins. + +The following slides are taken from David Mentré‘s 2016 presentation. + + I decided to spend a day or two last month seeing if I could formally prove some code inside qemu, and I arbitrarily picked one of the smallest pieces of code in the "util/" subdirectory: @@ -92,22 +105,6 @@ Frama-C parsed the C code and the formal specification and machine checked it, and it's correct - the code is bug-free. -= OVERVIEW OF FRAMA-C ECOSYSTEM = - -Let's interrupt this and talk about Frama-C. The name stands -for "Framework for Static Analysis of the C language". - -It's modular, with a core program that reads C source code -and turns it into Abstract Syntax Trees. And a set of plugins -to do static analysis by annotating these syntax trees. -Plugins can cooperate, so analysis can be passed between -plugins. - -The following slides are taken from David Mentré‘s 2016 presentation. - - -= BACK TO RANGE.C = - Going back to what we proved so far: /*@ -- 1.8.3.1