--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on January 2014 ---
Hello, The best way to do that is to use ACSL assertions. For instance: ... /*@ assert x > 8; */ if(x > 8){ ... } This ACSL assertion will reduce the value of x, and that will make the test evaluate to true. In some cases it is possible that the reduction is not sufficient. In this case, I would advise using adding "assert(\false)" in the else branch: ... /*@ assert x > 8; */ if(x > 8){ ... } else { /*@ assert \false; */ } This latter assertion would prevent state to be propagated in the else branch. Matthieu Yibiao Yang <cs.yang.yibiao at gmail.com> writes: > Dear all, > > For a given if statement, we can get the evaluated condition value by using : > > (* the api is: Db.Value.condition_truth_value : Cil_types.stmt -> > bool * bool *) > let (flag1, flag2) = Db.Value.condition_truth_value stmt in > > For my source code, flag1 is false but i can make sure the condition > can be true, Could it possible to set the flag1 and flag2 to be true > then re-do the value analysis? > > How can I customize these values for value analysis programmatically? > Or could it possible to change the abstract interpretation and the > state of the statement (e.g. the if condition) programmatically? > > Thank you very much. > > -david > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss