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
- Follow-Ups:
- [Frama-c-discuss] Looking for paper describing Frama-C internals
- From: Julien.Signoles at cea.fr (Julien Signoles)
- [Frama-c-discuss] Looking for paper describing Frama-C internals
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Looking for paper describing Frama-C internals
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Looking for paper describing Frama-C internals
- References:
- [Frama-c-discuss] Looking for paper describing Frama-C internals
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Looking for paper describing Frama-C internals
- Prev by Date: [Frama-c-discuss] Looking for paper describing Frama-C internals
- Next by Date: [Frama-c-discuss] Looking for paper describing Frama-C internals
- Previous by thread: [Frama-c-discuss] Looking for paper describing Frama-C internals
- Next by thread: [Frama-c-discuss] Looking for paper describing Frama-C internals
- Index(es):