Skip to content

Clean up code for pointer function parameters #853

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Feb 21, 2018
Merged

Clean up code for pointer function parameters #853

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7f4a79e
Tidy up C symbol factory code
Apr 21, 2017
cf4eeb2
Move code into code block instead of copying it
Apr 21, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 13 additions & 11 deletions src/ansi-c/c_nondet_symbol_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,15 +61,15 @@ static exprt c_get_nondet_bool(const typet &type)

class symbol_factoryt
{
std::vector<symbolt const *> &symbols_created;
std::vector<const symbolt *> &symbols_created;
symbol_tablet &symbol_table;
const source_locationt &loc;
const bool assume_non_null;
namespacet ns;

public:
symbol_factoryt(
std::vector<symbolt const *> &_symbols_created,
std::vector<const symbolt *> &_symbols_created,
symbol_tablet &_symbol_table,
const source_locationt &loc,
const bool _assume_non_null):
Expand Down Expand Up @@ -125,7 +125,7 @@ exprt symbol_factoryt::allocate_object(
// <target_expr> = &tmp$<temporary_counter>
code_assignt assign(target_expr, aoe);
assign.add_source_location()=loc;
assignments.add(assign);
assignments.move(assign);

return aoe;
}
Expand Down Expand Up @@ -171,7 +171,7 @@ void symbol_factoryt::gen_nondet_init(
else
{
// Add the following code to assignments:
// IF !(NONDET(_Bool) == FALSE) THEN GOTO <label1>
// IF !NONDET(_Bool) THEN GOTO <label1>
// <expr> = <null pointer>
// GOTO <label2>
// <label1>: <expr> = &tmp$<temporary_counter>;
Expand All @@ -186,7 +186,7 @@ void symbol_factoryt::gen_nondet_init(
null_check.then_case()=set_null_inst;
null_check.else_case()=non_null_inst;

assignments.add(null_check);
assignments.move(null_check);
}
}
// TODO(OJones): Add support for structs and arrays
Expand All @@ -202,7 +202,7 @@ void symbol_factoryt::gen_nondet_init(
code_assignt assign(expr, rhs);
assign.add_source_location()=loc;

assignments.add(assign);
assignments.move(assign);
}
}

Expand Down Expand Up @@ -233,13 +233,15 @@ exprt c_nondet_symbol_factory(
main_symbol.name=identifier;
main_symbol.base_name=base_name;
main_symbol.type=type;
main_symbol.location=loc;

symbol_exprt main_symbol_expr=main_symbol.symbol_expr();

symbolt *main_symbol_ptr;
bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
assert(!moving_symbol_failed);

std::vector<symbolt const *> symbols_created;
symbol_exprt main_symbol_expr=(*main_symbol_ptr).symbol_expr();
std::vector<const symbolt *> symbols_created;
symbols_created.push_back(main_symbol_ptr);

symbol_factoryt state(
Expand All @@ -252,11 +254,11 @@ exprt c_nondet_symbol_factory(

// Add the following code to init_code for each symbol that's been created:
// <type> <identifier>;
for(symbolt const *symbol_ptr : symbols_created)
for(const symbolt * const symbol_ptr : symbols_created)
{
code_declt decl(symbol_ptr->symbol_expr());
decl.add_source_location()=loc;
init_code.add(decl);
init_code.move(decl);
}

init_code.append(assignments);
Expand All @@ -273,7 +275,7 @@ exprt c_nondet_symbol_factory(
from_integer(0, index_type())));
input_code.op1()=symbol_ptr->symbol_expr();
input_code.add_source_location()=loc;
init_code.add(input_code);
init_code.move(input_code);
}

return main_symbol_expr;
Expand Down
5 changes: 5 additions & 0 deletions src/util/std_code.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,6 +78,11 @@ class code_blockt:public codet
o.push_back(*it);
}

void move(codet &code)
{
move_to_operands(code);
}

void add(const codet &code)
{
copy_to_operands(code);
Expand Down