More precise deps when calldeps computation

ID0001633: This issue was created automatically from Mantis Issue 1633. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001633	Frama-C	Plug-in > from	public	2014-01-27	2017-03-06

Reporter	Anne	Assigned To	yakobowski	Resolution	suspended
Priority	normal	Severity	feature	Reproducibility	have not tried
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Fluorine-20130601	Target Version	-	Fixed in Version	-

Description :

When both -calldeps (for precise computation) and -deps (for the synthesis) options are used, it would be great to use to calldeps results to produce the deps. For instance, in the example below, f is called only once, and its calldeps are precise, but the deps merge all the deps from the 'inc' function. One would expect deps and calldeps to be the same when there is only one call to a function.

Additional Information :

Results:

from] ====== DEPENDENCIES COMPUTED ====== These dependencies hold at termination for the executions that terminate: [from] Function inc: X FROM X; Y; p (and SELF) Y FROM X; Y; p (and SELF) [from] Function f: X FROM X; Y (and SELF) Y FROM X; Y (and SELF) [from] Function main: X FROM X; Y (and SELF) Y FROM X; Y (and SELF) [from] ====== END OF DEPENDENCIES ====== [from] ====== DISPLAYING CALLWISE DEPENDENCIES ====== [from] call to inc at calldeps.c:3 (by f): Y FROM Y; p [from] call to inc at calldeps.c:4 (by main): X FROM X; p [from] call to f at calldeps.c:4 (by main): Y FROM Y [from] entry point: X FROM X Y FROM Y [from] ====== END OF CALLWISE DEPENDENCIES ======

Steps To Reproduce :

Example:

int X, Y; void inc (int * p) { (*p)++; } void f (void) { inc (&Y); } void main (void) { inc (&X); f (); }

$ frama-c -deps -calldeps calldeps.c