user1786344
user1786344

Reputation: 83

Undeclared variables in sliced program

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

Answers (1)

Virgile
Virgile

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

Related Questions