--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on October 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Unable to prove the example code in ACSL documentation



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.