--- layout: fc_discuss_archives title: Message 60 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [PROVENANCE INTERNET] Re: Frama-C: Detecting unreachable code?



Sorry, branch coverage will do, but we're still talking about testing.

On 23/01/2014 09:52, Nicky Williams wrote:
> Of course, static analysis can only detect unreachable code.
> To be sure that THERE IS NO unreachable code you need to do path
> testing, eg. with the pathcrawler plugin (and to achieve full coverage
> with no timeouts).
> Nicky Williams
>
> On 23/01/2014 09:36, Pascal Cuoq wrote:
>>
>>
>>
>> On Thu, Jan 23, 2014 at 9:25 AM, Nicholas Mc Guire <der.herr at hofr.at
>> <mailto:der.herr at hofr.at>> wrote:
>>
>>     On Thu, 23 Jan 2014, David MENTRE wrote:
>>
>>     just for completenes here is the code used in the above runs:
>>     int main(int i)
>>     {
>>       if (0 <= i  && i <= 10)
>>       {
>>          return -1;
>>       }
>>
>>       if (i == 5)
>>       {
>>          /* can never reach here? */
>>          return -2;
>>       }
>>
>>       return 0;
>>     }
>>
>>
>> Use option -slevel 20 -val in order for Frama-C's value analysis to
>> separate the execution paths where 0 > i, 0 <= i, ...:
>>
>> $ frama-c -val -slevel 20 t.c
>> ...
>> [value] ====== VALUES COMPUTED ======
>> [value] Values at end of function main:
>>   __retres ? {-1; 0}
>>
>> There is only one value analysis option to know until you are an
>> advanced user, and it is this one. It is the first and only
>> non-administrative option used in the tutorial of the value analysis.
>>
>>
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr
>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140123/477f3fb6/attachment.html>