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] Could it possible to change the if statement state then re-do value analysis programmatically?

  • Subject: [Frama-c-discuss] Could it possible to change the if statement state then re-do value analysis programmatically?
  • From: cs.yang.yibiao at gmail.com (Yibiao Yang)
  • Date: Tue, 7 Jan 2014 11:49:05 +0800
  • In-reply-to: <7f1u0lv415.fsf@cea.fr>
  • References: <CAA1cxuh=XQ1Fie2OVv4D7FjHwzMwmtGPi7CXcqXHmH4Oyusfuw@mail.gmail.com> <7f1u0lv415.fsf@cea.fr>
Dear Matthieu,

Thank you very much.
It is very useful.

Besides, I am also interest in:
1. identify this kind of statement that cause other statements to be dead code.
2. add this kind of assertion programatically for this kind of
statement. (this one is very easy if I can get the first statement
from the currently value state information.)

I don't know how to achieve the first goal by using the information of
value state. So currently, I am using code transformation to realize
the first goal.

e.g. transform this kind of statement "if(x > 8)" to "if(var)". (Here,
var is a newly created global variable.), therefore, it would prevent
the state to be propagated to the if and else branches.

However, this solution is not good enough while compared with adding
the assertion "assert exp;" for "if(exp) " statement.

-david


On 6 January 2014 17:43, Matthieu Lemerre <matthieu.lemerre at cea.fr> wrote:
>
> Hello,
>
> The best way to do that is to use ACSL assertions. For instance:
>
> ...
> /*@ assert x > 8; */
> if(x > 8){
>  ...
> }
>
> This ACSL assertion will reduce the value of x, and that will make the
> test evaluate to true.
>
> In some cases it is possible that the reduction is not sufficient. In
> this case, I would advise using adding "assert(\false)" in the else
> branch:
>
> ...
> /*@ assert x > 8; */
> if(x > 8){
>  ...
> }
> else
> {
>  /*@ assert \false; */
> }
>
> This latter assertion would prevent state to be propagated in the else
> branch.
>
> Matthieu
>
> Yibiao Yang <cs.yang.yibiao at gmail.com> writes:
>
>> Dear all,
>>
>> For a given if statement,  we can get the evaluated condition value by using :
>>
>> (* the api is:  Db.Value.condition_truth_value : Cil_types.stmt ->
>> bool * bool *)
>> let (flag1, flag2) = Db.Value.condition_truth_value stmt in
>>
>> For my source code, flag1 is false  but i can make sure the condition
>> can be true, Could it possible to set the flag1 and flag2 to be true
>> then re-do the value analysis?
>>
>> How can I customize these values for value analysis programmatically?
>> Or could it possible to change the abstract interpretation and the
>> state of the statement (e.g. the if condition) programmatically?
>>
>> Thank you very much.
>>
>> -david
>>
>> _______________________________________________
>> 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