--- layout: fc_discuss_archives title: Message 62 from Frama-C-discuss on August 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Meaning of "FROM \nothing" for function calls in -deps analysis?



Hello,

Considering following code:

"""in_out.c"""
int b, c, d, e;

void double_assign(void)
{
   int x = d;
   e = b;
   e = c;
}

void loop_branch(int a)
{
   if (a)
     b = c;
   else
     while (1)
       d = e;
}

void main(int param)
{
   c = 3;
   loop_branch(param);
   double_assign();
}
"""

"frama-c -deps in_out.c" produces:
"""
[from] Function double_assign:
   e FROM c
[from] Function loop_branch:
   b FROM c
[from] Function main:
   b FROM \nothing
   c FROM \nothing
   e FROM \nothing
"""

For main(), why -deps gives "b FROM \nothing" and "e FROM \nothing"? I 
would have expected "e FROM c" and "b FROM c" due to calls to 
loop_branch() and double_assign() and corresponding -deps analysis of 
those functions.

I found no explanation in §6.1 of Value analysis manual or in whole 
chapter 6.

I also tried various options from the "from" plug-in without success.

Best regards,
david