--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on April 2012 ---
On Sat, Apr 7, 2012 at 9:03 PM, Pascal Cuoq <pascal.cuoq at gmail.com> wrote: > I do not feel strongly about this, but currently the "Evaluate expression" > can be considered specified as manipulating ACSL for the following reasons: > > - The dialog window says "Enter an ACSL expression to evaluate". It says so because we currently do not have any facility for parsing a string into a C expr/lval etc. Thus, the ACSL parsers are used instead. But any ACSL expression which cannot be translated back into a C one is refused -- even one which Value would correctly evaluate in an assertion or a requires. Both an "evaluate as C" and "evaluate as ACSL" option would be useful. However, both require a very non-trivial amount of work, and no one has had the courage to tackle the issue. Patches, preferably not ones that add a blinking disclaimer, are welcome. > - If program variable x of type int is in [MIN_INT .. -1] in some point > and you evaluate -x in the GUI at that point, you get [1..MAX_INT+1]. My disclaimer in the previous message was there for a reason. No real attempt to give values the "good" type is done, so most integer expressions get type long long. If you declare your variable x directly with this type, computations on it will overflow. Alternatively, you can multiply your original x by itself enough times. -- Boris