--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on June 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Need help on C-code slicing



> 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