added function call to working queue in the full-slicer #702
Conversation
Signed-off-by: Lucas Cordeiro <[email protected]>
| status() << "Adding CPROVER library" << eom; | ||
| // add the library | ||
| status() << "Adding CPROVER library (" | ||
| << config.ansi_c.arch << ")" << eom; |
There was a problem hiding this comment.
This is a very useful change, but I'd appreciate if it could be placed in a separate PR - it's entirely unrelated to the topic of this PR.
There was a problem hiding this comment.
Implemented as suggested. I have just created another PR to handle this change: #703
| @@ -402,6 +402,8 @@ void full_slicert::operator()( | |||
| const exprt &s=to_code_dead(e_it->first->code).symbol(); | |||
| decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second); | |||
| } | |||
| else if(e_it->first->is_function_call()) | |||
| add_to_queue(queue, e_it->second, e_it->first); | |||
There was a problem hiding this comment.
This implies that all function calls are preserved, even when not on any path to the actual slicing criterion. I do agree that a variant of this is required for soundness (a major improvement would require changes as found, e.g., in Jens Krinke's PhD thesis), but ideally that would be limited to only those function calls on the call graph where the criterion can possibly be reached.
Signed-off-by: Lucas Cordeiro <[email protected]>
lucasccordeiro
force-pushed
the
fix-full-slice-05
branch
from
77d8249 to
187ba08
Compare
|
This is a duplicate of #898, which addresses a similar issue. |
Note the tests are marked THOROUGH as they take a little too long. This should be solved by diffblue#702.
Note the tests are marked THOROUGH as they take a little too long. This should be solved by #702.
Note the tests are marked THOROUGH as they take a little too long. This should be solved by #702.
Note the tests are marked THOROUGH as they take a little too long. This should be solved by #702.
Note the tests are marked THOROUGH as they take a little too long. This should be solved by #702.
After building the CFG data structure, function calls must be added to the working queue in the full-slicer for not slicing incorrectly programs that contain only function prototypes.