--- layout: fc_discuss_archives title: Message 60 from Frama-C-discuss on January 2014 ---
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>