--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on January 2014 ---
On Thu, 23 Jan 2014, Pascal Cuoq wrote: > On Thu, Jan 23, 2014 at 9:25 AM, Nicholas Mc Guire <[1]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. > hmm... not quite the reported value was in the mail from David MENTRE <snip> [value] ====== VALUES COMPUTED ====== [value] Values at end of function main: __retres ??? {-1} <---------------- *HERE* <snip> but that would actually be wrong - the {-1; 0} I can get but never the {-1} - so it seems Im still missing something here ? thx! hofrat