Skip to content

Commit

Permalink
Merge pull request #467 from tautschnig/return-fixes
Browse files Browse the repository at this point in the history
fixup! Consistently resize instead of just reserving in codet classes
  • Loading branch information
Daniel Kroening authored Jan 24, 2017
2 parents c13164c + 0ebb484 commit 02aea58
Show file tree
Hide file tree
Showing 6 changed files with 10 additions and 15 deletions.
7 changes: 3 additions & 4 deletions src/analyses/flow_insensitive_analysis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -341,15 +341,14 @@ bool flow_insensitive_analysis_baset::do_function_call(

goto_programt temp;

exprt rhs=side_effect_expr_nondett(code.lhs().type());

goto_programt::targett r=temp.add_instruction();
r->make_return();
r->code=code_returnt();
r->code=code_returnt(rhs);
r->function=f_it->first;
r->location_number=0;

exprt rhs=side_effect_expr_nondett(code.lhs().type());
r->code.move_to_operands(rhs);

goto_programt::targett t=temp.add_instruction(END_FUNCTION);
t->code.set(ID_identifier, code.function());
t->function=f_it->first;
Expand Down
5 changes: 1 addition & 4 deletions src/cpp/cpp_typecheck_compound_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -692,10 +692,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
namespacet(symbol_table).lookup(args[i].get(ID_C_identifier)).symbol_expr());
}

code_returnt code_return;
code_return.return_value() = expr_call;

func_symb.value = code_return;
func_symb.value=code_returnt(expr_call);
}
else
{
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/goto_program2code.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -556,7 +556,7 @@ goto_programt::const_targett goto_program2codet::convert_return(
goto_programt::const_targett upper_bound,
codet &dest)
{
code_returnt ret=to_code_return(target->code);
const code_returnt &ret=to_code_return(target->code);

// add return instruction unless original code was missing a return
if(!ret.has_return_value() ||
Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/goto_convert.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1622,7 +1622,7 @@ void goto_convertt::convert_return(

// remove void-typed return value
if(!result_is_used)
new_code.operands().resize(0);
new_code.return_value().make_nil();
}

if(targets.has_return_value)
Expand Down
7 changes: 3 additions & 4 deletions src/goto-programs/goto_convert_functions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -186,13 +186,12 @@ void goto_convert_functionst::add_return(

#endif

side_effect_expr_nondett rhs(f.type.return_type());

goto_programt::targett t=f.body.add_instruction();
t->make_return();
t->code=code_returnt();
t->code=code_returnt(rhs);
t->source_location=source_location;

side_effect_expr_nondett rhs(f.type.return_type());
t->code.move_to_operands(rhs);
}

/*******************************************************************\
Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/goto_convert_new_switch_case.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1508,7 +1508,7 @@ void goto_convertt::convert_return(

// remove void-typed return value
if(!result_is_used)
new_code.operands().resize(0);
new_code.return_value().make_nil();
}

if(targets.has_return_value)
Expand Down

0 comments on commit 02aea58

Please sign in to comment.