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] Getting completely imprecise results in value analysis

  • Subject: [Frama-c-discuss] Getting completely imprecise results in value analysis
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Fri, 15 Jul 2011 14:03:05 +0200
Several persons on the list have said they were getting completely
imprecise results {‌{ ANYTHING }‌} during the value analysis of
some large and unavailable programs. They also were unable to
reduce the issue to a smaller program that developers could have
investigated.

While working on something unrelated, I stumbled on one way
to get {‌{ ANYTHING }‌}. This is the only understood way to get
this behavior at this time. People who get this behavior are
invited to check whether their large, unavailable programs are
in fact doing this:

short retshort(void)
{
  return 12;
}

int pin;

int main (int c, char **v)
{
  pin = (*((int (*)())retshort))();
  return (1+pin);
}

With Carbon 20110201+ patchlevel1:

/usr/local/Frama-C_Carbon/bin/frama-c -val get_top.c
...
[value] Values for function main:
          pin[bits 0 to 15] ? {12; }
          __retres ? {‌{ ANYTHING }‌}

It was known that the value analysis was too lenient when
it came to function pointer casts, but not that this could
have this particular consequence.

Note that the C99 standard
allows casting a function pointer to another function pointer
type, and casting it BACK TO THE ORIGINAL TYPE
before calling the function, and nothing else. Programs that
only do that are analyzed correctly and without {‌{ ANYTHING }‌}.

In the next release, the above program will emit an alarm
and be diagnosed as non terminating.

Programs where the apparent call to retshort() is the
consequence of an approximation by the value analysis,
but which in fact use function pointers more carefully,
will have the alarm and calls to function(s) with a better
matching return type will be taken into account.

Pascal