--- layout: fc_discuss_archives title: Message 87 from Frama-C-discuss on January 2014 ---
Hello Dharmalingam, Le 25/01/2014 21:17, Dharmalingam Ganesan a ?crit : > For this below function, the value plugin says the > > [value] Values at end of function myFun: > i ? [--..--] > > > In my understanding [--, --] refers to all possible integers. But, the value of i for this function can never be below zero. In fact, Value analysis knows about this fact, see below "Frama_C_show_each_i([0..4294967295])". Maybe Value prints "[--..--]" because the whole range of variable "i" is seen? ------------ unsigned int i = 0; void myFun() { i++; Frama_C_show_each_i(i); } ----------- $ frama-c -val unint.c -main myFun -lib-entry [kernel] preprocessing with "gcc -C -E -I. unint.c" [value] Analyzing an incomplete application starting at myFun [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization i ? [--..--] unint.c:6:[value] assigning non deterministic value for the first time [value] Called Frama_C_show_each_i([0..4294967295]) unint.c:8:[value] Assertion got status valid. unint.c:3:[value] Function myFun: postcondition got status valid. [value] Recording results for myFun [value] done for function myFun [value] ====== VALUES COMPUTED ====== [value] Values at end of function myFun: i ? [--..--] In below int.c program (with an "int" instead of "unsigned int"), the Value analysis computes the correct range for i: --------------- #include <limits.h> int i = 0; void myFun() { if (i == INT_MAX) { i = 0; } i++; Frama_C_show_each_i(i); } void main(void) { while (Frama_C_nondet(0,1)) { myFun(); } } ---------------- $ frama-c -val `frama-c -print-share-path`/builtin.c -slevel 10 int.c [...] [value] ====== VALUES COMPUTED ====== [value] Values at end of function Frama_C_nondet: Frama_C_entropy_source ? [--..--] [value] Values at end of function myFun: i ? [1..2147483647] [value] Values at end of function main: Frama_C_entropy_source ? [--..--] i ? [0..2147483647] Best regards, david