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] Need help on C-code slicing

  • Subject: [Frama-c-discuss] Need help on C-code slicing
  • From: francois.armand at orange.fr (François Armand)
  • Date: Thu, 9 Jun 2011 18:08:50 +0200
  • In-reply-to: <BANLkTikG=kiiqsZCCZvic1FW=Vc2cn2J6w@mail.gmail.com>
  • References: <BANLkTi=eKHMSg8Sdq88OwqqO890tjdg+Cw@mail.gmail.com> <BANLkTikG=kiiqsZCCZvic1FW=Vc2cn2J6w@mail.gmail.com>
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>