Skip to content

Commit 27227cc

Browse files
added support for array_copy in the full-slice option
Do not slice away array_copy expressions during the implicit call in the full-slicert class. We do not process array_copy in value_set_fit.
1 parent 5ecb15e commit 27227cc

File tree

2 files changed

+7
-0
lines changed

2 files changed

+7
-0
lines changed

src/goto-instrument/full_slicer.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -337,6 +337,10 @@ static bool implicit(goto_programt::const_targett target)
337337
{
338338
// some variables are used during symbolic execution only
339339

340+
const irep_idt &statement=target->code.get_statement();
341+
if(statement==ID_array_copy)
342+
return true;
343+
340344
if(!target->is_assign())
341345
return false;
342346

src/pointer-analysis/value_set_fi.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1729,6 +1729,9 @@ void value_set_fit::apply_code(
17291729
else if(statement==ID_fence)
17301730
{
17311731
}
1732+
else if(statement==ID_array_copy)
1733+
{
1734+
}
17321735
else if(statement==ID_input || statement==ID_output)
17331736
{
17341737
// doesn't do anything

0 commit comments

Comments
 (0)