Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Looking for paper describing Frama-C internals

  • Subject: [Frama-c-discuss] Looking for paper describing Frama-C internals
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Mon, 20 Sep 2010 15:27:50 +0200
  • In-reply-to: <AANLkTi=++JuFCmovHMW6hRZXa05GP-XdC7oRApjP0oX-@mail.gmail.com>
  • References: <AANLkTi=++JuFCmovHMW6hRZXa05GP-XdC7oRApjP0oX-@mail.gmail.com>
> I would like to know more about Frama-C internals, especially
> regarding algorithms used for abstract analysis

For that part, and after a quick look at the unpublished material
that we have in store, I am afraid I have to say we have nothing
worth reading.

However, if we had something, it would probably be structured thus:

A/ Abstract domains

1/ Integers
  intervals + congruences
2/ Precise addresses
  finite maps from bases to integers. Ex: {‌{ &a + { 2; } }‌}
3/ Imprecise addresses
  Sets of bases. Ex: garbled mix of ...
4/ Origins
  Ex: Misaligned read, Merge, Library function, ...
5/ Possibly undefined value lying in memory
  Same as what we have built in 4/ with additional flags for
uninitialized and dangling pointers
6/ Offsetmaps
  Arrays of bits, consecutive slices of which may contain values from 5/
7/ Unrelational memory states
  Maps from bases to 6/
8/ Relational memory states
  A state as defined in 7/ plus relations of the kind "pointers p and
q point to the same area, and that area contains ..."

B/ Dataflow algorithm

1/ without using option -slevel: basic dataflow propagation from
Kildall 73 / Cousot 77.
2/ with -slevel

Regarding A/6/, you can find a bit of the problem explained, and a
description for a data structure that is still being implemented and
not actually used yet in the value analysis, in the JFLA 2010 article:
http://jfla.inria.fr/2010/actes/PDF/bonichon_cuoq.pdf

> and general
> architecture of Frama-C.

I am surprised that Julien did not point you in particular to the ICFP
Experience Report on Frama-C in 2009. There is a good overview of the
architecture there. Do you need us to make it temporarily available
somewhere?

Pascal