I'm currently discovering frama-c's features, and especially WP & Value's analysis tools. My final goal is to be able to use frama-c on larger codes that involves several layers with :
a lot of function calls
use of complex data structures
static and/or global variables
So far I've been trying to apply a bottom-up method i.e starting specifying functions that does not includes any function calls and analyze their behaviors by isolating them thanks to -lib-entry and -main kernel options. By doing that I make sure that if pre conditions are assumed to be true, then the whole function contract is verified. As soon as I tried to specify upper layers that invokes those functions, things gets complicated. First I often have to specify the behavior of the called functions which is not always easy because those functions may deal with variables/functions out of the scope of the current function.
Let me give you an easy example:
Let's say that in file1.h we define a data structure "my_struct" that contains a field number and a field parity.
In file1.c I have two functions :
A first function "check_parity" that just tests if the parity field of the static variable _sVar is correct.
A second function "correct_parity" that calls the first function, and corrects the parity if the field was not correct.
In file2.c, I have a fonction "outside_caller" that just calls correct_parity(). My objective is to be able to specify outside_caller the same way I'm specifying correct_parity. Bellow is the corresponding source code :
Here the main issue is that in order to specify outside_caller(), I need to access _sVar which is out of scope in file2.c. That implies to deal with a ghost variable (g_sVar) that is declared in file1.h and updated in correct_parity function. In order to make the caller (correct_parity) able to use the callees contracts, the ghost variable g_sVar must be used inside the contracts of the callees.
In this configuration, the callees are specified with g_sVar ghost variable, except for requires and assings clauses for 2 reasons :
I need to check _sVar R/W accesses with \valid & \valid_read since its a pointer
When I tried to specify assigns clauses of the callees with g_sVar, I was not able to verify the corresponding clause.
But by doing so, I somehow made the specification of the caller invalid, as you can se on WP's output.
Why does it seems the more functions calls I have, the more it becomes complicated to prove the behavior of the functions ? Is there a proper way to deal with multiple function calls and static variables ?
Thank you a lot in advance !
PS: I'm working with Magnesium-20151002 version, on a VM running with Ubuntu 14.04, 64-bit machine. I know that getting started with WhyML and Why3 could help me a lot but so far I haven't been able to install Why3 ide neither on windows nor on Ubuntu following each step of this tutorial
First of all, please note that -main and -lib-entry aren't that useful for WP (you mentioned that you are also interested in EVA/Value Analysis, but your question is directed towards WP).
Your issue with static variables is a known one, and the easiest way to deal with it is indeed to declare a ghost variable in the header. But then you must express your contracts in terms of the ghost variable and not the static one.
Otherwise, the callers will not be able to make use of these contracts, since they do not know anything about _sVar. As a rule of thumb, it is better to put the contract in the header: this way, you're bound to only use identifiers that are visible outside of the translation unit.
Regarding function calls, the main point is that any function that is called by the function you're trying to prove with WP must come with a contract that at least contain an assigns clause (and possibly more precise specifications, depending on how much the effects of the callee are relevant for the property that you want to prove on the caller). The important thing to remember here is that, from WP's point of view, after the call, only what is explicitly stated in the callee's contract through ensures is true, plus the fact that any location not in the assigns clause has been left unchanged.