--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on January 2014 ---
On Thu, Jan 2, 2014 at 4:31 PM, David Yang <abiao.yang at gmail.com> wrote: > > Could it possible to modify the state of specified statement then > re-run the value analysis at some program point? > If you mean propagating an abstract state forward from a chosen statement, dropping all the branches the propagation to which was pending and the call stack that represented more pending work, then yes, it is possible to do so programmatically. What the value analysis already does is to compute the initial state where globals without initializers contain 0 and so on, to assign this initial state to the first statement of the main function and to launch a dataflow algorithm from there. You could programmatically assign any abstract state to any statement of any function and pass that to the same dataflow algorithm. On the other hand, this will not work as you may expect if the abstract state in question does not represent the entirety of the future work remaining to do, for the reason that the other data structure representing future work (other states attached to other statements at the time of the interruption, call stack,...) will not be restored. /* example */ > int main(int *A, int n){ > /* other stmts */ > int res = A[8] + 6; /* stmt 3 */ > /* other stmts */ > > return res; > } > > In this purely linear example where you are interested by a statement of the main function, it could work. Pascal -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140103/24c90dd1/attachment.html>