--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on January 2014 ---
On Thu, Jan 23, 2014 at 9:25 AM, Nicholas Mc Guire <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. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140123/8c38f617/attachment.html>