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] Information hiding: how to handle module's private static variables in Frama-C?

  • Subject: [Frama-c-discuss] Information hiding: how to handle module's private static variables in Frama-C?
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Wed, 27 Nov 2013 10:30:03 +0100
Hello,

At work we have a situation where we want to use C static variables
(variables visible only to a C file) to hide some internal state of a
module. However, we have an issue with the assigns clause: as this
variable is private to the module, it is not visible outside it and
thus cannot be used in the assigns clause of calling functions. But
those calling functions needs nonetheless to refer to it, otherwise
the assigns clause is not proved. How would you handle this properly
in Frama-C?

The attached files illustrate my point. Variable "a" is static to file
q18_a.c. It is used in an internal function of the module incr_a(),
called through function f() which is part of module public API.

The public contract of f() visible in q18_a.h and the module specific
assigns clause for "a" is kept in the private contract of f(), in file
q18_a.c. So far so good. Everything is proved with WP and RTE.

Now, function g() in q18_b.c calls f() (and thus indirectly assigns to
"a"). However, I cannot put "assigns \nothing;" into g()'s contract
(unproved because "a" *is* assigned), neither "assigns a;" because "a"
is not visible (and anyway I don't want to do that as "a" should be
private to q18_a.c module).

Both C files are called with:
  frama-c-gui -wp -wp-rte  q18_b.c q18_a.c

What is the proper way to handle such design in Frama-C?

Best regards,
david
-------------- next part --------------
A non-text attachment was scrubbed...
Name: q18_a.c
Type: text/x-csrc
Size: 244 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131127/fb6a9e9f/attachment-0002.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: q18_a.h
Type: text/x-chdr
Size: 85 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131127/fb6a9e9f/attachment-0001.h>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: q18_b.c
Type: text/x-csrc
Size: 178 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131127/fb6a9e9f/attachment-0003.c>