--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on May 2011 ---
Hello David, > It seems that the "n1 < n2" expression is a bit too complicated for > the value analysis plugin. > [...] > I tried to add an "//@ assert n1 < n2 || n1 >= n2;" The situation is a little bit like adding //@ assert x1 - x0 >= 0.125; in this example: http://blog.frama-c.com/index.php?post/2011/03/26/Helping-the-value-analysis-2 It doesn't work because the relation between two variables that you are offering is not in the general pattern of the information that the value analysis represents. It generally is able to represent precisely more simple properties such as "x >= 12" or "x <= 17" or the conjunction of properties that it can represent (such as the conjunction of the above). If you are writing assertions for the purpose of helping it, you should offer them in a format that matches its internal representation for memory states. Pascal