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] Value analysis aborted

Hello,

the behavior you are describing happens when the value analysis
has to interpret an assignment of the form

*e = ...;

and it doesn't have any information at all about the value of e.

While not an error in itself, this is terrible for precision:
knowing nothing about e, it has to consider that the assignment
changes any variable. Usually, there is no point in continuing
the analysis after that (and therefore it stops, as you have seen).

In fact, I have done my best to prevent this happening,
and it can be considered a bug when it does.

The last such bug that could cause this message to be displayed
was fixed in February, according to the message below, and
the patch is available:

-* Value      [2011/02/14] Fixed bug when passing bitfield
	      as argument to function. (jrrt)

http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2011-February/002527.html

What version were you using, and if it's less that Carbon + value patchlevel 1,
could you upgrade and see if it fixes it?

Pascal