--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on April 2012 ---
>> 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. I think that the issue is that the GUI evaluates ACSL expressions. ACSL, unlike C, is total: *p == *p is true regardless of the validity of p and of the initializedness of *p. because it is an instance of an axiom. When you pass arr[i] in the GUI, you shouldn't get just arr[0], because "arr[i] == 0", for instance, is a valid ACSL assertion, and one that shouldn't get the status "true". Instead, the value analysis should say that it can't tell the value of arr[0]. In the value analysis proper, there is a filtering step before calling Cvalue.Model.find to keep only the valid locations in the argument location (and emit the appropriate alarm if the location is not entirely valid). I guess you could say that the API for calling Cvalue.Model.find is that it should only be applied to arguments that have been filtered thus. But since Cvalue.Model.find has a ~with_alarms argument already, we could make it emit alarms when it notices that the location passed is not completely valid. That would be less surprising for plug-in authors who call Cvalue.Model.find directly. In fact, you could call it a bug that Cvalue.Model.find does not already do that, but this cannot be observed from the commandline version of Frama-C (to the best of my knowledge) for the aforementioned reason that out of bounds accesses are handled in a preliminary step when it's the value analysis calling Cvalue.Model.find. I am reluctant to use the B-word for usages that have not been defined as the commandline usage has in the value analysis manual and in the blog. Pascal