--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on September 2010 ---
> 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