Skip to content

Commit 1542852

Browse files
committed
Fix code style issues
Signed-off-by: František Nečas <[email protected]>
1 parent a0b0d0f commit 1542852

8 files changed

+30
-21
lines changed

src/2ls/graphml_witness_ext.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,6 @@ class graphml_witness_extt:public graphml_witnesst
3030
void operator()(const summary_checker_baset &summary_checker);
3131

3232
protected:
33-
3433
void add_edge(
3534
const graphmlt::node_indext &from,
3635
const dynamic_cfg_nodet &from_cfg_node,

src/2ls/summary_checker_nonterm.cpp

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -172,10 +172,12 @@ void summary_checker_nontermt::check_properties(
172172
}
173173
SSA.current_unwinding=store_unwinding;
174174

175-
property_map.insert({property_id, property_infot(
176-
n_it->loophead->location,
177-
"assertion",
178-
property_statust::UNKNOWN)});
175+
property_map.insert({
176+
property_id,
177+
property_infot(
178+
n_it->loophead->location,
179+
"assertion",
180+
property_statust::UNKNOWN)});
179181
cover_goals.goal_map[property_id].conjuncts.push_back(
180182
disjunction(loop_check_operands));
181183
ls_guards.push_back(not_exprt(lsguard));
@@ -278,10 +280,12 @@ void summary_checker_nontermt::check_properties_linear(
278280
exprt::operandst loop_exit_cond;
279281
exprt::operandst neg_loop_exit_cond;
280282

281-
property_map.insert({property_id, property_infot(
282-
n_it->loophead->location,
283-
"assertion",
284-
property_statust::UNKNOWN)});
283+
property_map.insert({
284+
property_id,
285+
property_infot(
286+
n_it->loophead->location,
287+
"assertion",
288+
property_statust::UNKNOWN)});
285289

286290
unsigned const_number=0;
287291
for(local_SSAt::objectst::const_iterator

src/domains/strategy_solver_binsearch2.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -92,8 +92,11 @@ bool strategy_solver_binsearch2t::iterate(invariantt &_inv)
9292
#endif
9393
improve_rows.insert(row);
9494
symb_values.insert({row, tpolyhedra_domain.get_row_symb_value(row)});
95-
lower_values.insert({row, simplify_const(
96-
solver.get(tpolyhedra_domain.strategy_value_exprs[row][0]))});
95+
lower_values.insert({
96+
row,
97+
simplify_const(
98+
solver.get(
99+
tpolyhedra_domain.strategy_value_exprs[row][0]))});
97100
blocking_constraint.push_back(
98101
literal_exprt(!tpolyhedra_domain.strategy_cond_literals[row]));
99102
if(inv[row].is_neg_inf())

src/domains/strategy_solver_binsearch3.cpp

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -86,9 +86,12 @@ bool strategy_solver_binsearch3t::iterate(invariantt &_inv)
8686
debug() << "improve row " << row << eom;
8787
#endif
8888
improve_rows.insert(row);
89-
symb_values.insert({row,tpolyhedra_domain.get_row_symb_value(row)});
90-
lower_values.insert({row, simplify_const(
91-
solver.get(tpolyhedra_domain.strategy_value_exprs[row][0]))});
89+
symb_values.insert({row, tpolyhedra_domain.get_row_symb_value(row)});
90+
lower_values.insert({
91+
row,
92+
simplify_const(
93+
solver.get(
94+
tpolyhedra_domain.strategy_value_exprs[row][0]))});
9295
blocking_constraint.push_back(
9396
literal_exprt(!tpolyhedra_domain.strategy_cond_literals[row]));
9497
if(inv[row].is_neg_inf())

src/ssa/dynobj_instance_analysis.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -263,9 +263,10 @@ void dynobj_instance_domaint::output(
263263
}
264264
}
265265

266-
void dynobj_instance_analysist::initialize(const irep_idt &function_id,
267-
const goto_programt &goto_program)
266+
void dynobj_instance_analysist::initialize(
267+
const irep_idt &function_id,
268+
const goto_programt &goto_program)
268269
{
269270
forall_goto_program_instructions(i_it, goto_program)
270271
get_state(i_it).make_bottom();
271-
}
272+
}

src/ssa/malloc_ssa.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ inline static optionalt<typet> c_sizeof_type_rec(const exprt &expr)
3535
{
3636
forall_operands(it, expr)
3737
{
38-
if (auto maybe_t=c_sizeof_type_rec(*it))
38+
if(auto maybe_t=c_sizeof_type_rec(*it))
3939
return maybe_t;
4040
}
4141
}

src/ssa/may_alias_analysis.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -124,8 +124,7 @@ void may_alias_analysist::initialize(
124124
const irep_idt &function_id,
125125
const goto_functionst::goto_functiont &goto_function)
126126
{
127-
128127
ait<may_alias_domaint>::initialize(function_id, goto_function);
129128
forall_goto_program_instructions(i_it, goto_function.body)
130129
get_state(i_it).make_bottom();
131-
}
130+
}

src/ssa/may_alias_analysis.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ Author: Viktor Malik, [email protected]
2020
class may_alias_domaint:public ai_domain_baset
2121
{
2222
public:
23-
may_alias_domaint(): has_values(false) {};
23+
may_alias_domaint(): has_values(false) {}
2424

2525
void transform(
2626
const irep_idt &,

0 commit comments

Comments
 (0)