--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on March 2011 ---
My appologies there was a mistake in the first mail, here is the correction: I have the following code: int main(int bar) { int toto; if (bar == 1234) { toto = 0; } else { toto = 1; toto = 2; toto = 3; } return toto; } On windows xp, FramaC Boron with the following command: frama-c-gui -slevel 100 -val test.c when evaluating bar at the toto = 0; line I get: Before statement: bar ? {1234; } At next statement: bar ? [--..--] but when evaluating bar at the toto = 2; line I get: Before statement: bar ? [--..--] At next statement: bar ? [--..--] when I was hoping for something like bar ? [--..--] - {1234} based on the evaluation of bar at the toto = 1; and toto = 3; lines (I assume here that the next statement is return toto; and not toto = 3; and the before statement int toto; and not toto = 1;) Is there a way to get these exclusions from the value analysis? Even if there is only one line in the else branch? If possible I'm looking for a way to evaluate an expression at the statement, not before or after. If the statement modifies the expression it does not work but if it is not related to it, shouldn't the value analysis be able to provide a value or range for this expression? Thank you On Tue, Mar 15, 2011 at 6:36 PM, xavier kauffmann < xavier.kauffmann at gmail.com> wrote: > Hello, > > I have the following code: > > int main(int bar) > { > int toto; > if (bar == 1234) > { > toto = 0; > } > else > { > toto = 1; > toto = 2; > toto = 3; > } > return toto; > } > > On windows xp, FramaC Boron with the following command: > frama-c-gui -slevel 100 -val test.c > > when evaluating bar at the toto = 1; line I get: > Before statement: > bar ? {1234; } > At next statement: > bar ? [--..--] > but when evaluating bar at the toto = 2; line I get: > Before statement: > bar ? [--..--] > At next statement: > bar ? [--..--] > when I was hoping for something like > bar ? [--..--] - {1234} > based on the evaluation of bar at the toto = 1 and toto = 3 lines > > Is there a way to get these exclusions from the value analysis? > Even if there is only one line in the else branch? > > If possible I'm looking for a way to evaluate an expression at the > statement, not before or after. > If the statement modifies the expression it does not work but if it is not > related to it, shouldn't the value analysis be able to provide a value or > range for this expression? > > Thank you > > -Xavier > > > > -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? nettoy?e... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110315/4ca7277c/attachment.htm>