--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on January 2014 ---
Dear Pascal, Thank you very much for your suggestion. I solved this problem, by using another method: transforming the source code. I will going to transform the similarly expression "A[8]" to "A[a_val]", Here, a_val is a new global variable created by myself. After that, the statements below that statement can be correctly analyzed. Thank you very much. -david On 3 January 2014 20:52, Pascal Cuoq <pascal.cuoq at gmail.com> wrote: > 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 > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss