--- layout: fc_discuss_archives title: Message 55 from Frama-C-discuss on January 2014 ---
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. If you use frama-c-gui, you'll see the code mark as dead (red background). * Note that you code is a bit too specific, as we always have "i == 0" (i is a non volatile, global variable, initialized at 0 at the beginning of the program). I would rather use this example: """ int main(int i) { if (0 <= i && i <= 10) { return -1; } if (i == 5) { /* can never reach here? */ return -2; } return 0; } """ In that case, Value analysis rightly found the code dead with parameter -slevel 2 (allow at most 2 different analysis paths, see doc for details): frama-c-gui -val -slevel 2 unreachable.c $ frama-c -val -slevel 2 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 ? {-1; 0} <---------------------- *HERE* Never -2 * Or you could also use option -lib-entry on your original code: $ frama-c -val -slevel 2 -lib-entry unreachable.c [kernel] preprocessing with "gcc -C -E -I. unreachable.c" [value] Analyzing an incomplete application starting at main [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization i ? [--..--] <----- *HERE* Unknown value for i when main() is called [value] Recording results for main [value] done for function main [value] ====== VALUES COMPUTED ====== [value] Values at end of function main: __retres ? {-1; 0} <----- *HERE* Never -2 Best regards, david