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

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