--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on September 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



> 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