--- layout: fc_discuss_archives title: Message 62 from Frama-C-discuss on May 2010 ---
> ????Question is: how can I stop frama-c from making this approximation and > instead to feed me the result of s ? {1; 2; 3; 4; 5; 107; 108; 110; ?}? There are two ways: 1) You can recompile after having changed the constant 7 at the top of file src/ai/ival.ml into something else. Example: using 17 instead of 7: s ? {1; 2; 3; 4; 5; 107; 108; 110; } 2) You can change your program to: void main(void) { int i; int s=0; int index=Frama_C_interval(0,7); /*@ assert index==0 || index==1 || index==2 || index==3 || index==4 || index==5 || index==6 || index==7 ; */ s=big.p[index]; Frama_C_show_each_s(s); } and use the commandline: bin/toplevel.byte -val t.c share/builtin.c -slevel 17 You get: ... [value] Called Frama_C_show_each_s({1; }) [value] Called Frama_C_show_each_s({2; }) [value] Called Frama_C_show_each_s({3; }) [value] Called Frama_C_show_each_s({4; }) [value] Called Frama_C_show_each_s({5; }) [value] Called Frama_C_show_each_s({110; }) [value] Called Frama_C_show_each_s({107; }) [value] Called Frama_C_show_each_s({108; }) Note that I needed to insert the Frama_C_show_each_s call to prove that the values of s were computed with precision. The precision is still lost when the results are synthesized for recording, but there are programmatic hooks to access the separate values before they are thrown away. Both methods have their own disadvantages: Method 1) requires you to recompile, you can't report bugs in the modified version, and performance is not guaranteed when you modify the constant 7 too much. It may also work okay: it is just that we have not tested the value analysis with large constants. Method 2) does not require you to recompile, is officially supported, but at this time you have little control over the repartition of the superposed states that you allow with option -slevel. If your program contains a lot of conditionals, the conditionals may eat all the slevels you have the resources to throw at them. Pascal