--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on September 2009 ---
>The value analysis considers that f1 don't terminate. > >test1.c:14:[kernel] warning: out of bounds read. assert \valid(adr+8); >test1.c:16:[kernel] warning: non termination detected in function f1 > > >/*@ requires \valid(adr+ (0..100)); > requires \valid(adr+8); >*/ >int f1(const char * const adr) This is covered page 55 of the Value Analysis manual, 7.1.2, paragraph "Limitations", first limitation. The manual is at http://frama-c.cea.fr/download/value-analysis-Beryllium.pdf For generating an initial state that is general enough that you can reduce it with your assertions, you may be interested in paragraph 5.2.4, page 42, "Tweaking the automatic generation of initial values". However, once you do that, you will find that reducing the generated initial state with "\valid..." preconditions is not supported (that is, you get false alarms as documented in the second limitation of 7.1.2, paragraph "Limitations"). Pascal