While working with Frama-C, i encountered some strange dependencies. These occur when functions are called multiple times and pointers are passed as parameters. The following code shows the problem broken down to the minimum:
int sourceA = 1, sourceB = 1;
int targetA, targetB;
int deref_ptr(int* ptr){
return *ptr;
}
int main(int argc, char* argv[]){
targetA = deref_ptr(&sourceA);
targetB = deref_ptr(&sourceB);
return 0;
}
Frama-C computes the following dependencies using the EVA plugin.
[kernel] Parsing test.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
sourceA ∈ {1}
sourceB ∈ {1}
targetA ∈ {0}
targetB ∈ {0}
[eva] done for function main
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
2 functions analyzed (out of 2): 100% coverage.
In these functions, 6 statements reached (out of 6): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
0 alarms generated by the analysis.
----------------------------------------------------------------------------
No logical properties have been reached by the analysis.
----------------------------------------------------------------------------
[from] Computing for function deref_ptr
[from] Done for function deref_ptr
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function deref_ptr:
\result FROM sourceA; sourceB; ptr
[from] Function main:
targetA FROM sourceA; sourceB
targetB FROM sourceA; sourceB
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
The dependencies of the main function are of interest here. The expectation was that targetA depends on sourceA and targetB depends on sourceB. But in addition Frama-C computes dependencies from the respective other call of the deref_ptr function. Can this behavior be influenced so that targetA only depends on sourceA (same for targetB and sourceB)?
It would have helped to have the exact command line with which you launched Frama-C. Judging from the result, this is probably frama-c -deps example.c, but please note that details on the options you used usually matter a lot.
That said, -deps indeed merges information from all the calls of each function. If you look at frama-c -from-help, though, you'll notice that there is another option for computing dependencies: -calldeps, whose description is:
force callsite-wise dependencies (opposite option is -no-calldeps)
And indeed, frama-c -calldeps example.c gives you the desired result:
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] call to deref_ptr at example.c:10 (by main):
\result FROM sourceA; ptr
[from] call to deref_ptr at example.c:11 (by main):
\result FROM sourceB; ptr
[from] entry point:
targetA FROM sourceA
targetB FROM sourceB
\result FROM \nothing
[from] ====== END OF CALLWISE DEPENDENCIES ======