--- layout: fc_discuss_archives title: Message 63 from Frama-C-discuss on August 2015 ---
Hello David, On Fri, Aug 28, 2015 at 3:55 PM, David MENTRE <dmentre at linux-france.org> wrote: > > void main(int param) > { > c = 3; > > [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. > Option -deps show the dependencies, when the function under consideration terminates, of the values of the variables when the function terminates with respect to the values of variables when the function begins. b FROM c for function main() would mean that b is computed from the value c had when main() was entered. This is not the case because the first thing does is to assign c, so as a consequence, b is really from âwhatever c was computed from when it was assigned at the beginning of main()â. The assignment is in fact âc = 3;â, meaning that c is computed from nothing, and this is why when the end of main() is reached, b has been computed from nothing. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150828/88620791/attachment.html>