File tree Expand file tree Collapse file tree 3 files changed +11
-15
lines changed Expand file tree Collapse file tree 3 files changed +11
-15
lines changed Original file line number Diff line number Diff line change @@ -210,11 +210,9 @@ bool flow_insensitive_analysis_baset::do_function_call(
210
210
211
211
goto_programt temp;
212
212
213
- exprt rhs =
214
- side_effect_expr_nondett (code.lhs ().type (), l_call->source_location );
213
+ goto_programt::targett r = temp. add ( goto_programt::make_return ( code_returnt (
214
+ side_effect_expr_nondett (code.lhs ().type (), l_call->source_location )))) ;
215
215
216
- goto_programt::targett r =
217
- temp.add (goto_programt::make_return (code_returnt (rhs)));
218
216
r->function =f_it->first ;
219
217
r->location_number =0 ;
220
218
Original file line number Diff line number Diff line change @@ -1834,18 +1834,16 @@ void goto_checkt::goto_check(
1834
1834
if (local_bitvector_analysis->dirty (variable))
1835
1835
{
1836
1836
// need to mark the dead variable as dead
1837
- exprt address_of_expr=address_of_exprt (variable);
1838
1837
exprt lhs=ns.lookup (CPROVER_PREFIX " dead_object" ).symbol_expr ();
1839
- address_of_expr =
1840
- typecast_exprt::conditional_cast (address_of_expr , lhs.type ());
1841
- const if_exprt rhs (
1838
+ exprt address_of_expr = typecast_exprt::conditional_cast (
1839
+ address_of_exprt (variable) , lhs.type ());
1840
+ if_exprt rhs (
1842
1841
side_effect_expr_nondett (bool_typet (), i.source_location ),
1843
- address_of_expr,
1844
- lhs,
1845
- lhs.type ());
1842
+ std::move (address_of_expr),
1843
+ lhs);
1846
1844
goto_programt::targett t =
1847
1845
new_code.add (goto_programt::make_assignment (
1848
- code_assignt (lhs, rhs), i.source_location ));
1846
+ code_assignt (std::move ( lhs), std::move ( rhs) ), i.source_location ));
1849
1847
t->code .add_source_location ()=i.source_location ;
1850
1848
}
1851
1849
}
Original file line number Diff line number Diff line change @@ -45,11 +45,11 @@ void build_havoc_code(
45
45
m_it++)
46
46
{
47
47
exprt lhs=*m_it;
48
- exprt rhs =
49
- side_effect_expr_nondett (lhs.type (), loop_head->source_location );
48
+ side_effect_expr_nondett rhs (lhs.type (), loop_head->source_location );
50
49
51
50
goto_programt::targett t = dest.add (goto_programt::make_assignment (
52
- code_assignt (lhs, rhs), loop_head->source_location ));
51
+ code_assignt (std::move (lhs), std::move (rhs)),
52
+ loop_head->source_location ));
53
53
t->function =loop_head->function ;
54
54
t->code .add_source_location ()=loop_head->source_location ;
55
55
}
You can’t perform that action at this time.
0 commit comments