--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on June 2011 ---
Thanks to both of you for these answers. I'm gonna spend some time on this learning curve and will very likely come back later on Thanks again Fran?ois 2011/6/9 Pascal Cuoq <pascal.cuoq at gmail.com> > > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110609/f3a19903/attachment.htm>