Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie global variables and functions

>> 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