--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on August 2008 ---
On Aug 29, 2008, at 12:00 PM, David DELMAS wrote: > __fun_cpt FROM h; __fun_cpt; (and default:false) Hi David, we agree that there is a little fuzziness in what the analyzer does with your "assigns" clause in this example. Let us first look at the tools that you making use of here. One is ACSL's "assigns" clause in a function contract. The other is the (automatically computed from the results of the value analysis) -deps analysis. ACSL assigns clauses are intended to specify functional dependencies. In this context, there is no difference between a function f that a/ assigning a new value to variable y that happens to be computed from the previous value of y and b/ possibly not assigning variable y in the function, so that it would have retained its previous value after the function call. Both are specified in exactly the same way: "assigns y \from y;". The value of y after a call to f depends functionally of the value of y before the call. The analysis that is launched with the -deps command-line option, on the other hand, distinguishes between a/ and b/, because it has a notion of "possibly not having been assigned" for a variable, which is printed as "default:true". The message "default:false" on the other hand guarantees that the variable is assigned during the execution of the function. For functions for which the source code is not available, it is desirable to use the "assigns" clauses, if present, for the -deps analysis. For this reason, a module was written inside Frama-C for translating the assigns clauses into dependencies in the -deps format. The reason the Frama-C implementers thought it would be okay to have default:false in an example such as yours is that if a variable, such as __fun_cpt in your example, might not be assigned, it would appear in the "assigns" clause, and therefore be mentioned as an explicit dependency on the right-hand side (as it is in your example). There is a slight problem with this approach, which I think is the reason you are asking about this example. Some implementations for function fun can satisfy the assigns clause without satisfying the translation of this clause into the -deps format. For instance, consider the following implementation for function fun int fun(int x) { if (__fun_cpt) __fun_cpt++; return (x + fun_cpt); } This implementation satisfies the contract in your example. But if the -deps analysis is launched on this implementation of fun, the resulting dependencies contain __fun_cpt FROM __fun_cpt (and default:true) This may disturb you because this dependency is different (and indeed is not included in) the dependency that was computed from the contract when the implementation was not available. We agree that this needs to be fixed. But was this the problem that you had with the treatment of your example? In your example, the "default:false" that puzzles you comes from the fact that fun is called systematically by main2, and that the function fun has the dependency __fun_cpt FROM __fun_cpt; (and default:false) (this is just to evaluate the urgency of this fix, and whether you consider your question answered). Pascal -------------- section suivante -------------- Une pièce jointe HTML a été enlevée... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20080829/c85e3991/attachment.htm