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

Am 16.01.2016 um 21:20 schrieb Chan Ngo:
> 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.

The are some software design difficulties and challenges to consider also
for this special statement.
A few coding style documents recommend its reuse to make software implementations
even more robust eventually.

Example "Chapter 7: Centralized exiting of functions":
https://git.kernel.org/cgit/linux/kernel/git/torvalds/linux.git/tree/Documentation/CodingStyle?id=4b10df7f2c8b3c6de12375b85456c6fd275af6d0#n389


> In principle, it is detected by building the control flow graph (CFG)
> of the program and see the dead code fragment.

Do you know any extensions for such a data structure which are developed
during software research activities?


> 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.

This issue got some attention for a while.


I became interested to clarify details which are also shown here a bit more.

1. How do you think about consequences from the selection of popular
   short identifiers in a programming language like "C"?

   * Does the identifier length indicate anything?

   * Will it help to reuse logograms and ideograms there from the evolving
     support for the Unicode standard?

   * Does a bit of psychology matter for safer communication and the evolution
     of thinking processes here?
     Is it occasionally nicer to specify "go to success" instead of stressing
     the possibility for failure around such jump labels and status variables?

2. Is another search pattern variant interesting here?

   * Would you like to look at the amount of source code which is used in the
     control flow between statements like "goto"?

   * How often will the determination matter for optimisation approaches
     if a branch or code path is "empty" (or contains only comments together
     with additional white-space characters)?


> Any static analyzer provides a function to give the CFG of a program.

Do you suggest the reuse of any standard data formats for advanced
software analysis?

How many progress do you see in the development of plug-ins (or add-ons)?


> Roundly speaking, CFG is the essential input for all analysis including
> value analysis, pointer analysis, … (called data flow analysis)

Are there any relationships to a technology like computation tree logic?

Regards,
Markus