--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on January 2014 ---
[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



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