--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on June 2011 ---
> I compiled my sources with gcc -save-temps > and run frama-c-gui - val myfile.i providing only the i file I'm interested > in. > > I get a "Degeneration occurred"? banner in the window title bar.. and seem > to be unable to get any usable result from this point. Here are a couple of suggestions to go further: - if you use the batch version frama-c instead of the GUI version frama-c-gui, you will get a partial analysis log that can provide indices. - you are in the same situation as Sali Sene in the discussion thread "[Frama-c-discuss] Value analysis aborted" at the bottom of http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2011-May/thread.html You are in a situation that I did my best to prevent, and it's a bug that this happened. - the situation is that the program writes at a completely unknown address. The reason why this shouldn't happen is that it should be impossible to have a completely unknown value for the evaluation of any expression. The origin of your problem is the first completely unknown value during the analysis of the program (once you have a completely unknown value, it is normal that it contaminates any computations that involve it). The "completely unknown" value is denoted as "{{ANYTHING}}". In the case of Sali Sene, it had something to do with function pointers, but it was not easy to reproduce on a simple case for the precise reason that I tried to make it impossible to happen. Therefore, no fix is available yet, but there is still hope. - I am very much looking forward to your reduced examples where you show "{{ANYTHING}}" appearing during the analysis. If you can produce these reduced (or even, if the code's license allows, unreduced) examples, I will probably be able to fix the issue. Frama_C_dump_each() is your friend: it shows the entire state at the time of the call. An {{ANYTHING}} anywhere in this state is abnormal behavior. Pascal