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] Control flow graphs and code coverage

Hello,

> On Jan 16, 2016, at 8:22 PM, SF Markus Elfring <elfring at users.sourceforge.net> wrote:
> 
> Hello,
> 
> I have read the user manual for your evolving software. Now I would like to
> find a bit more out from technology areas which are involved here.
> 
> * Would you like to share any more information about the use of advanced
>  control flow graphs?
> 
> * Do extended versions get any special names?
> 
> * How can the amount of source code which is used between statements
>  like "goto" (in the C programming language) be modelled by such
>  a software design approach?
> 
>  Use case:
>  Do you try to improve capabilities for static source analysis in the way
>  that issues which are similar to the description of consequences from
>  a special "goto fail;" in the article "An interesting SSL implementation bug"
>  can be better detected?
>  http://blog.frama-c.com/index.php?post/2014/02/23/CVE-2013-5914
> 
> * Do you know any plug-ins (or add-ons) which collaborate with related
>  software tools?
> 
For the use of “go to” statement in C, in critical software development, the convention is that, programers cannot use “go to” statement. 
However, you can use static code analysis (static analyzer) as you’ve mentioned to detect this kind of bug, i.e. “goto fail”. In principle, it is detected by building the control flow graph (CFG) of the program and see the dead code fragment. For example, the “goto fail” bug, the problem with the code of Apple’s sslKeyExchange.c source file is that there are two repeated “goto” statements and under some circumstances the seconde “goto” will be triggered, then the return error code “err” is zero, meaning that the code after the second “goto” is unreachable, dead code. 

Any static analyzer provides a function to give the CFG of a program. Roundly speaking, CFG is the essential input for all analysis including value analysis, pointer analysis, … (called data flow analysis)

For example, Polyspace of Mathworks, Asstree (or AbsInt), GrammaTech Codesonar can detect dead code. Or even you can use any compiler or tool that constructs CFG of a program and then look at the dead code (i.e., LLVM)

Hope that helps.

---
Chan Ngo
INRIA,
(+33)02 99 84 72 84
chan.ngo at inria.fr
http://people.rennes.inria.fr/Chan.Ngo


> Regards,
> Markus
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss