--- layout: fc_discuss_archives title: Message 66 from Frama-C-discuss on April 2012 ---
Hello, I am doing some Value analysis (with Frama-C Nitrogen) on a code that has the same structure that the attached example. Roughly, this code is made of two for loops, j and k, one inside the other. * First basic analysis I run: frama-c -cpp-command 'gcc -E -C -I. ' -val -slevel 100 /usr/local/share/frama-c/builtin.c array_loop.c The loop bounds are correctly computed, with acceptable approximation. [value] Values for function F: min ? {15} max ? {35} j ? {35} k ? [34..50] * Addition of an array access Now, if I add a simple array access, that simply reads k: frama-c -cpp-command 'gcc -E -C -I. -DOUT_ACCESS' -val -slevel 100 /usr/local/share/frama-c/builtin.c array_loop.c Then the loop bound for k is wrongly approximated, k ? [34..143]. The 143 upper bound is clearly far from the real bound, 50. [value] Values for function F: Frama_C_entropy_source ? [--..--] min ? {15} max ? {35} j ? {35} k ? [34..143] The point I don't understand is why adding a *read* access on k variable makes the bound computation on k so bad? I am not modifying k in any way, so that for me Value analysis should give the same approximation (k ? [34..50]). Of course, if I increase slevel to 620 ( j range * k range == (35-15) * 31) ) the k value is correctly computed. I am asking this question because the real code I am analysing has the same overall structure (the two loops with the same numerical bound in a first step) but with a lot of linear computations inside them : it computes the value of several variables, the new ones form the previous ones, reading the 'in' array and writing the 'out' one. I need to increase a *lot* slevel, up to 10,000, to get a correct result on k bound. Using the 620 slevel value does not compute the correct bound on k. I don't understand why. Best regards, david -------------- next part -------------- A non-text attachment was scrubbed... Name: array_loop.c Type: text/x-csrc Size: 1101 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120427/5d255684/attachment.c>