--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on January 2014 ---
On Thu, 23 Jan 2014, David MENTRE wrote: > Hello Dharmalingam, > > Le 23/01/2014 03:54, Dharmalingam Ganesan a ??crit : >> I'm wondering whether Frama-C can report unreachable code without any annotation, for example, see the below code? > > * Yes using Value analysis plug-in: > > $ frama-c -val unreachable.c > [kernel] preprocessing with "gcc -C -E -I. unreachable.c" > [value] Analyzing a complete application starting at main > [value] Computing initial state > [value] Initial state computed > [value] Values of globals at initialization > i ??? {0} > [value] Recording results for main > [value] done for function main > [value] ====== VALUES COMPUTED ====== > [value] Values at end of function main: > __retres ??? {-1} <---------------- *HERE* > > Value analysis determines your function always returns -1. > Interesting - Don't see that result ! hofrat at debian:~/frama-c$ frama-c -version Version: Nitrogen-20111001 Compilation date: Wed May 16 13:02:51 UTC 2012 Share path: /usr/share/frama-c (may be overridden with FRAMAC_SHARE variable) Library path: /usr/lib/frama-c (may be overridden with FRAMAC_LIB variable) Plug-in paths: /usr/lib/frama-c/plugins (may be overridden with FRAMAC_PLUGIN variable) hofrat at debian:~/frama-c$ frama-c -val unreachable.c [kernel] preprocessing with "gcc -C -E -I. unreachable.c" [value] Analyzing a complete application starting at main [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization [value] Recording results for main [value] done for function main [value] ====== VALUES COMPUTED ====== [value] Values for function main: __retres ? {-2; -1; 0} and florine also did not produce that result hofrat at rtl15:~/frama-c$ frama-c -version Version: Fluorine-20130401 Compilation date: Sun Jan 12 12:52:44 EST 2014 Share path: /usr/local/share/frama-c (may be overridden with FRAMAC_SHARE variable) Library path: /usr/local/lib/frama-c (may be overridden with FRAMAC_LIB variable) Plug-in paths: /usr/local/lib/frama-c/plugins (may be overridden with FRAMAC_PLUGIN variable) hofrat at rtl15:~/frama-c$ frama-c -val unreachable.c [kernel] preprocessing with "gcc -C -E -I. unreachable.c" [value] Analyzing a complete application starting at main [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization [value] Recording results for main [value] done for function main [value] ====== VALUES COMPUTED ====== [value] Values at end of function main: __retres ? {-2; -1; 0} what version is this result from ? or did I miss something essential ? thx! ofrat 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; }