--- layout: fc_discuss_archives title: Message 123 from Frama-C-discuss on November 2013 ---
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>