--- layout: fc_discuss_archives title: Message 99 from Frama-C-discuss on December 2009 ---
>> A correct specification for f2 as it is written would be assigns var1, var2; > So you always need to manually propagate > the assigns clause of every function which > is called by the function in focus? Yes. The contract of a function is intended to allow the person (or program) who read it to know what the function does, or at least a summary of what it does. It doesn't matter to the person (or program, but the fact that it can be a program is completely incidental) reading the contract that global var1 is modified in a callee of f2. He/she/it doesn't want to know. All that matters is that var1 may be modified each time f2 is called. > does you agree that it would be the case to > implement in Why some kind of automatically > propagation of the refered (indirectly) assigns clauses? No. The normal usage of these tools is to write the specification first, and the code later. It doesn't make sense to ask for some automatic computation of assigns clauses from the code when the code is available, because in normal usage the code is *not* available at the time the assigns are written. This said, someone mentioned automatically inferring assigned locations from the source code when source code is available with some sort of automatic "value analysis" (have you heard of it?): http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-December/001679.html Assigns clauses can be expressed in ways that do not allow easy propagation: consider the case where f1 receives a pointer p and assigns *p. That's a low-level specification. Its caller f2 doesn't have to tell you that it calls f1 for doing its assignments (this dirty little secret is its to keep), and it wouldn't help you to know that *p is modified without the value of p, which is an expression of f2 containing local variables of f2... What you want is the high-level specification of f2, which is that it modifies var1, var2. Pascal PS: Yes, everyone on this list is writing specifications for existing code. C came out almost 40 years ago, Open-Source Frama-C less than two years ago. I said "normal usage" but it's fine to write specifications for existing code, as long as you remain aware of what you are doing. -------------- section suivante -------------- Une pi?ce jointe non texte a ?t? nettoy?e... Nom: non disponible Type: application/ms-tnef Taille: 3958 octets Desc: non disponible Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091210/e2838a56/attachment-0001.bin