--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on April 2012 ---
Hi again, On Fri, Apr 6, 2012 at 11:24 AM, Pierre Karpman <Pierre.Karpman at rennes.supelec.fr> wrote: > although arr[i] is not used at mark1, I'd still like to know what the value > analysis can say about it. This can be done e.g. in the GUI by asking to > evaluate the expression "arr[i]" at this statement, which will give me the > result "arr[i] == 0"; this is confusing because the right way to interpret > the result would be "if this expression were to be in the source; if the > program didn't fail, then it would have this value", but there isn't any > hint about which conditions are necessary for the program not to > pretend-fail when we pretend-evaluate it, as there would be in the form of > an assert statement if the expression was actually in the source. > I will probably add the checks I need in my code, then. The GUI is indeed missing a warning telling that the requested expression may not evaluate in all cases. We will probably add this for the next release. For your plugin, you can also do a few things. As you have probably noticed, the function that evaluates expressions take a ~with_alarms parameter as argument. This argument is supposed to indicate what happens when a possible error is detected. One possibility is <nothing>, which corresponds to CilE.warn_none_mode. An another possibility is to use the CilE.Acall constructor, with a function that prints your own warning, or set a reference meaning "an alarm has occurred". In both cases (and unless your user-defined function raises an exception), the functions will return what happens when evaluation is defined. Hope this helps, -- Boris