Reputation: 83
When using the program slicer of Frama-C version Oxygen, I have the problem that the resulting slice uses undeclared variables. I searched for existing postings to this topic before and found this: http://bts.frama-c.com/print_bug_page.php?bug_id=806
There it is mentioned that the bug was fixed in the Nitrogen version of Frama-C. Maybe this change was not carried over to Oxygen? Like in the description of the existing posting it only happens for blocks with just one statement. I cannot attach the example source code since it is from a customer project.
Upvotes: 0
Views: 92
Reputation: 10148
I have checked the exact steps described in the bug report you mention with Frama-C Oxygen (and csmith 2.0.0 for Csmith's runtime library), and everything works fine: it's very likely that you're experiencing another issue, but without the code, it's impossible to say more.
Upvotes: 2