--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on May 2011 ---
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