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] different range in the loop depending de type

  • Subject: [Frama-c-discuss] different range in the loop depending de type
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Sat, 7 Nov 2009 12:13:48 +0100
  • References: <1257544602.12758.5.camel@valin>
Hello St?phane,

> Depending the type of i, the range is not the same.
> The range of i in the loop is [0..10] (for int) or [0..15] for char or
> short.
_____

void main(void)
{
char i=0;
int j=0;
while (i<10) i++;
while (j<10) j++;
}

[value] ====== VALUES COMPUTED ======
[value] Values for function main:
i IN {10; 11; 12; 13; 14; 15; }
j IN {10; }
_____

It's interesting that you noticed this behavior,
because I fixed a comparable problem on short
notice this summer for an intern who had to demo
his plug-in the following week.

Note that the AST for the two loops is different:
  i = (char)0;
  j = 0;
  while ((int )i < 10) {i = (char )((int )i + 1);}
  while (j < 10) {j ++;}

CIL transforms the code thus because the C standard
specifies that operators such as ++ do not operate on
types smaller than int, and that values of these types
are implicitly promoted to int in these conditions.

Meanwhile, in the absence of any loop-related
option, the value analysis tries to keep computations
short at the price of precision by using a technique
called "widening". In order to limit the loss of precision,
however, various heuristics are used, including a
syntactic one for the j loop that recognizes that 
j IN [0..10] is a good candidate for the loop invariant.

This heuristic does not currently recognize the condition
((int )i < 10) as one where it would be valuable to try
the same kind of invariant.

I have filed this issue as "feature wish" in the Bug Tracking
System, so that it is not forgotten.
http://bts.frama-c.com/view.php?id=325

Pascal