diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 9f87400877a..be765796ebb 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -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", @@ -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); @@ -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); } @@ -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; @@ -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()) { @@ -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()); } } @@ -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()) diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 08df3629f9f..38786b66c58 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -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) @@ -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; @@ -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; } @@ -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) @@ -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) diff --git a/src/goto-programs/scope_tree.cpp b/src/goto-programs/scope_tree.cpp index 48797fc80c9..e8c3061bf17 100644 --- a/src/goto-programs/scope_tree.cpp +++ b/src/goto-programs/scope_tree.cpp @@ -10,8 +10,9 @@ #include -void scope_treet::add(const codet &destructor, - std::optional declaration) +void scope_treet::add( + const codet &destructor, + std::optional declaration) { auto previous_node = get_current_node(); using declaration_optt = std::optional; @@ -28,8 +29,8 @@ optionalt &scope_treet::get_destructor(node_indext index) return scope_graph[index].destructor_value; } -optionalt - &scope_treet::get_declaration(node_indext index) +optionalt & +scope_treet::get_declaration(node_indext index) { PRECONDITION(index < scope_graph.size()); return scope_graph[index].declaration; @@ -115,7 +116,6 @@ node_indext scope_treet::get_current_node() const scope_treet::scope_nodet::scope_nodet( codet destructor, std::optional declaration) - : destructor_value(std::move(destructor)), - declaration(std::move(declaration)) + : destructor_value(std::move(destructor)), declaration(std::move(declaration)) { } diff --git a/src/goto-programs/scope_tree.h b/src/goto-programs/scope_tree.h index d41cd5054cd..59c4be81c2d 100644 --- a/src/goto-programs/scope_tree.h +++ b/src/goto-programs/scope_tree.h @@ -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 declaration); + void add( + const codet &destructor, + std::optional declaration); /// Fetches the destructor value for the passed-in node index. optionalt &get_destructor(node_indext index);