--- layout: fc_discuss_archives title: Message 62 from Frama-C-discuss on August 2015 ---
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