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] precision for expression evaluation in acondition

  • Subject: [Frama-c-discuss] precision for expression evaluation in acondition
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
  • Date: Tue, 15 Mar 2011 21:09:42 +0100
  • References: <AANLkTink3Q_fvtMV55j1sOosg4VO8=337kvMCAurOW0k@mail.gmail.com> <AANLkTi=cSeyA9QuG6W2dnAHbDpcCrxy_C=g7g=maHeX-@mail.gmail.com>
Hello Xavier,

I don't know the value analysis very well but maybe it is related
to the fact that you do not provide an initial value for toto.
If I modify your programm like     

   int toto;
   printf("%d\n", toto); 

then I get the value 

1606415944

The C Standard says in Section 6.7.8 (?10)

    If an object that has automatic storage duration is not initialized
explicitly, its value is indeterminate.


Jens


-----Original Message-----
From: frama-c-discuss-bounces at lists.gforge.inria.fr on behalf of xavier
kauffmann
Sent: Tue 15.03.2011 19:08
To: Frama-c-discuss at lists.gforge.inria.fr
Subject: Re: [Frama-c-discuss] precision for expression evaluation in
acondition
 
My appologies there was a mistake in the first mail, here is the correction:

I have the following code:

int main(int bar)
{
  int toto;
  if (bar == 1234)
  {
    toto = 0;
  }
  else
  {
    toto = 1;
    toto = 2;
    toto = 3;
  }
  return toto;
}

On windows xp, FramaC Boron with the following command:
frama-c-gui -slevel 100 -val test.c

when evaluating bar at the toto = 0; line I get:
Before statement:
bar ? {1234; }
At next statement:
bar ? [--..--]
but when evaluating bar at the toto = 2; line I get:
Before statement:
bar ? [--..--]
At next statement:
bar ? [--..--]
when I was hoping for something like
bar ? [--..--] - {1234}
based on the evaluation of bar at the toto = 1; and toto = 3; lines
(I assume here that the next statement is return toto; and not toto = 3;
and the before statement int toto; and not toto = 1;)

Is there a way to get these exclusions from the value analysis?
Even if there is only one line in the else branch?

If possible I'm looking for a way to evaluate an expression at the
statement, not before or after.
If the statement modifies the expression it does not work but if it is not
related to it, shouldn't the value analysis be able to provide a value or
range for this expression?

Thank you

On Tue, Mar 15, 2011 at 6:36 PM, xavier kauffmann <
xavier.kauffmann at gmail.com> wrote:

> Hello,
>
> I have the following code:
>
> int main(int bar)
> {
>   int toto;
>   if (bar == 1234)
>   {
>     toto = 0;
>   }
>   else
>   {
>     toto = 1;
>     toto = 2;
>     toto = 3;
>   }
>   return toto;
> }
>
> On windows xp, FramaC Boron with the following command:
> frama-c-gui -slevel 100 -val test.c
>
> when evaluating bar at the toto = 1; line I get:
> Before statement:
> bar ? {1234; }
> At next statement:
> bar ? [--..--]
> but when evaluating bar at the toto = 2; line I get:
> Before statement:
> bar ? [--..--]
> At next statement:
> bar ? [--..--]
> when I was hoping for something like
>  bar ? [--..--] - {1234}
> based on the evaluation of bar at the toto = 1 and toto = 3 lines
>
> Is there a way to get these exclusions from the value analysis?
> Even if there is only one line in the else branch?
>
> If possible I'm looking for a way to evaluate an expression at the
> statement, not before or after.
> If the statement modifies the expression it does not work but if it is not
> related to it, shouldn't the value analysis be able to provide a value or
> range for this expression?
>
> Thank you
>
> -Xavier
>
>
>
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/ms-tnef
Size: 4196 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110315/34c37c6b/attachment-0001.bin>