Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to modify the value state of a statement for re-running the value analysis

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>