--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on October 2014 ---
Well, this is known issue on modularity of specifications and proofs. A general method would be to have two specifications for module B. Typically, you can have a #define around the static variable ?X? to make it ?static? in concrete code, but public in ?proof? header. The more general solution is based on refinement: one specification for B is concrete and is used for proving properties inside B : functions assigns the (private) static variables in B. The second specification for B is abstract, and is used for asserting Pre-Post for other modules to call functions in B. In this second spec, functions in B assign dummy (ghost) public variables that model the internal state of all variables in B. What is missing in this methodology is a way to make both specifications consistent with each other. L.