Skip to content

Commit

Permalink
Applied formatter
Browse files Browse the repository at this point in the history
  • Loading branch information
Enrico Steffinlongo committed Dec 4, 2023
1 parent 8714ce6 commit b9bcca0
Show file tree
Hide file tree
Showing 4 changed files with 30 additions and 30 deletions.
30 changes: 14 additions & 16 deletions src/goto-programs/goto_convert.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -160,7 +160,7 @@ void goto_convertt::build_declaration_hops(
const auto existing_flag = label_flags.find(inputs.label);
if(existing_flag != label_flags.end())
return existing_flag->second;
const symbolt& new_flag = get_fresh_aux_symbol(
const symbolt &new_flag = get_fresh_aux_symbol(
bool_typet{},
id2string(inputs.label),
"going_to",
Expand All @@ -174,7 +174,8 @@ void goto_convertt::build_declaration_hops(
flag_creation.instructions.push_back(
goto_programt::make_decl(new_flag.symbol_expr(), hidden));
const auto make_clear_flag = [&]() -> goto_programt::instructiont {
return goto_programt::make_assignment(new_flag.symbol_expr(), false_exprt{}, hidden);
return goto_programt::make_assignment(
new_flag.symbol_expr(), false_exprt{}, hidden);
};
flag_creation.instructions.push_back(make_clear_flag());
program.destructive_insert(program.instructions.begin(), flag_creation);
Expand All @@ -187,8 +188,8 @@ void goto_convertt::build_declaration_hops(

{
// Set flag before the goto.
auto set_flag = goto_programt::make_assignment(flag.symbol_expr(),
true_exprt{}, hidden);
auto set_flag =
goto_programt::make_assignment(flag.symbol_expr(), true_exprt{}, hidden);
program.insert_before_swap(inputs.goto_instruction, set_flag);
}

Expand All @@ -204,13 +205,14 @@ void goto_convertt::build_declaration_hops(

// TODO - TYPE CHECK FOR VAR ARRAYS!

bool add_if =
declaration->if_conditions_added.find(flag.name) ==
declaration->if_conditions_added.end();
bool add_if = declaration->if_conditions_added.find(flag.name) ==
declaration->if_conditions_added.end();
if(add_if)
{
auto if_goto = goto_programt::make_goto(target, flag.symbol_expr(), hidden);
program.instructions.insert(std::next(declaration->instruction), std::move(if_goto));
auto if_goto =
goto_programt::make_goto(target, flag.symbol_expr(), hidden);
program.instructions.insert(
std::next(declaration->instruction), std::move(if_goto));
declaration->if_conditions_added.insert(flag.name);
}
target = declaration->instruction;
Expand Down Expand Up @@ -258,7 +260,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
else if(i.is_incomplete_goto())
{
const irep_idt &goto_label = i.code().get(ID_destination);
const auto l_it=targets.labels.find(goto_label);
const auto l_it = targets.labels.find(goto_label);

if(l_it == targets.labels.end())
{
Expand Down Expand Up @@ -318,10 +320,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
inputs.label_instruction = l_it->second.first;
inputs.label_scope_index = label_target;
inputs.end_scope_index = intersection_result.common_ancestor;
build_declaration_hops(
dest,
label_flags,
inputs);
build_declaration_hops(dest, label_flags, inputs);
//WATCHVAR(i.get_target()->to_string());
}
}
Expand Down Expand Up @@ -683,8 +682,7 @@ void goto_convertt::convert_block(
const source_locationt &end_location=code.end_location();

// this saves the index of the destructor stack
node_indext old_stack_top =
targets.scope_stack.get_current_node();
node_indext old_stack_top = targets.scope_stack.get_current_node();

// now convert block
for(const auto &b_code : code.statements())
Expand Down
14 changes: 7 additions & 7 deletions src/goto-programs/goto_convert_class.h
Original file line number Diff line number Diff line change
Expand Up @@ -431,14 +431,14 @@ class goto_convertt:public messaget
{
break_set=true;
break_target=_break_target;
break_stack_node= scope_stack.get_current_node();
break_stack_node = scope_stack.get_current_node();
}

void set_continue(goto_programt::targett _continue_target)
{
continue_set=true;
continue_target=_continue_target;
continue_stack_node= scope_stack.get_current_node();
continue_stack_node = scope_stack.get_current_node();
}

void set_default(goto_programt::targett _default_target)
Expand All @@ -457,14 +457,14 @@ class goto_convertt:public messaget
{
throw_set=true;
throw_target=_throw_target;
throw_stack_node= scope_stack.get_current_node();
throw_stack_node = scope_stack.get_current_node();
}

void set_leave(goto_programt::targett _leave_target)
{
leave_set=true;
leave_target=_leave_target;
leave_stack_node= scope_stack.get_current_node();
leave_stack_node = scope_stack.get_current_node();
}
} targets;

Expand Down Expand Up @@ -503,7 +503,7 @@ class goto_convertt:public messaget
default_set=targets.default_set;
break_target=targets.break_target;
default_target=targets.default_target;
break_stack_node=targets.scope_stack.get_current_node();
break_stack_node = targets.scope_stack.get_current_node();
cases=targets.cases;
cases_map=targets.cases_map;
}
Expand Down Expand Up @@ -535,7 +535,7 @@ class goto_convertt:public messaget
{
throw_set=targets.throw_set;
throw_target=targets.throw_target;
throw_stack_node=targets.scope_stack.get_current_node();
throw_stack_node = targets.scope_stack.get_current_node();
}

void restore(targetst &targets)
Expand All @@ -557,7 +557,7 @@ class goto_convertt:public messaget
{
leave_set=targets.leave_set;
leave_target=targets.leave_target;
leave_stack_node=targets.scope_stack.get_current_node();
leave_stack_node = targets.scope_stack.get_current_node();
}

void restore(targetst &targets)
Expand Down
12 changes: 6 additions & 6 deletions src/goto-programs/scope_tree.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,9 @@

#include <util/std_code.h>

void scope_treet::add(const codet &destructor,
std::optional<goto_programt::targett> declaration)
void scope_treet::add(
const codet &destructor,
std::optional<goto_programt::targett> declaration)
{
auto previous_node = get_current_node();
using declaration_optt = std::optional<declaration_statet>;
Expand All @@ -28,8 +29,8 @@ optionalt<codet> &scope_treet::get_destructor(node_indext index)
return scope_graph[index].destructor_value;
}

optionalt<scope_treet::declaration_statet>
&scope_treet::get_declaration(node_indext index)
optionalt<scope_treet::declaration_statet> &
scope_treet::get_declaration(node_indext index)
{
PRECONDITION(index < scope_graph.size());
return scope_graph[index].declaration;
Expand Down Expand Up @@ -115,7 +116,6 @@ node_indext scope_treet::get_current_node() const
scope_treet::scope_nodet::scope_nodet(
codet destructor,
std::optional<declaration_statet> declaration)
: destructor_value(std::move(destructor)),
declaration(std::move(declaration))
: destructor_value(std::move(destructor)), declaration(std::move(declaration))
{
}
4 changes: 3 additions & 1 deletion src/goto-programs/scope_tree.h
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,9 @@ class scope_treet
/// current node.
/// \param destructor Code which is called when the current scope is left.
/// \param declaration Code which is called when the scope is entered by goto.
void add(const codet &destructor, std::optional<goto_programt::targett> declaration);
void add(
const codet &destructor,
std::optional<goto_programt::targett> declaration);

/// Fetches the destructor value for the passed-in node index.
optionalt<codet> &get_destructor(node_indext index);
Expand Down

0 comments on commit b9bcca0

Please sign in to comment.