--- layout: fc_discuss_archives title: Message 82 from Frama-C-discuss on September 2013 ---
> > On Sun, Sep 8, 2013 at 7:23 PM, David Yang <abiao.yang at gmail.com<http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss>> > wrote: > > > >* the code below the line 5 is dead code. I understand that it is because > *>* the default context-width is 2. So line 5 is out of bound memory > access. > *> > >* But i want to analysis the function by not treat all code to be dead > code > *>* and continue the value analysis procedure. > *> > This is not possible in Frama-C's value analysis. More precisely, there are > no values worth continuing the execution with after an undefined behavior, > such as an out-of-bounds memory access, because ?undefined behavior? means > that anything is possible. This is discussed as one of the points in this > article: https://www.dropbox.com/s/el2lidf5v71ogm6/p.pdf > If you want the value analysis not to treat the code as dead code, tell it > that variable A points to an array of size at least the value of variable > size. There are several ways to do that. You may find that the best results > are obtained with separate analyses for each size. Dear Pascal, Thank you very much for replying me. I choose to programmatically construct a new function with a new statement to call that the function by using following api functions. Cil.emptyFunction ... Cil.mkStmt ... At the same time I initialized those argument programmatically. Best regards. David. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130912/7d3f2afb/attachment.html>