Skip to content

Include list where using a std::list and drop forall_expr_list macro #1851

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.

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 1 commit into from
Feb 19, 2018
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
8 changes: 6 additions & 2 deletions src/analyses/uninitialized_domain.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@ Date: January 2010
#include <util/std_expr.h>
#include <util/std_code.h>

#include <list>

void uninitialized_domaint::transform(
locationt from,
locationt to,
Expand Down Expand Up @@ -43,10 +45,12 @@ void uninitialized_domaint::transform(
std::list<exprt> read=expressions_read(*from);
std::list<exprt> written=expressions_written(*from);

forall_expr_list(it, written) assign(*it);
for(const auto &expr : written)
assign(expr);

// we only care about the *first* uninitalized use
forall_expr_list(it, read) assign(*it);
for(const auto &expr : read)
assign(expr);
}
}
}
Expand Down
2 changes: 2 additions & 0 deletions src/ansi-c/ansi_c_parse_tree.h
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]

#include "ansi_c_declaration.h"

#include <list>

class ansi_c_parse_treet
{
public:
Expand Down
2 changes: 2 additions & 0 deletions src/ansi-c/c_typecast.h
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
#include <util/namespace.h>
#include <util/expr.h>

#include <list>

// try a type cast from expr.type() to type
//
// false: typecast successful, expr modified
Expand Down
2 changes: 2 additions & 0 deletions src/ansi-c/printf_formatter.h
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,8 @@ Author: Daniel Kroening, [email protected]
#include <util/expr.h>
#include <util/namespace.h>

#include <list>

class printf_formattert
{
public:
Expand Down
4 changes: 2 additions & 2 deletions src/cbmc/bmc.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -139,8 +139,8 @@ void bmct::do_conversion()
{
status() << "converting constraints" << eom;

forall_expr_list(it, bmc_constraints)
prop_conv.set_to_true(*it);
for(const auto &constraint : bmc_constraints)
prop_conv.set_to_true(constraint);
}
// hook for cegis to freeze synthesis program vars
freeze_program_variables();
Expand Down
2 changes: 1 addition & 1 deletion src/cbmc/bmc.h
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ class bmct:public safety_checkert
virtual ~bmct() { }

// additional stuff
expr_listt bmc_constraints;
std::list<exprt> bmc_constraints;

void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }

Expand Down
2 changes: 2 additions & 0 deletions src/cpp/cpp_parse_tree.h
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]

#include "cpp_item.h"

#include <list>

class cpp_parse_treet
{
public:
Expand Down
2 changes: 2 additions & 0 deletions src/cpp/cpp_token_buffer.h
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]

#include "cpp_token.h"

#include <list>

class cpp_token_buffert
{
public:
Expand Down
2 changes: 2 additions & 0 deletions src/goto-instrument/accelerate/acceleration_utils.h
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Author: Matt Lewis
#ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H
#define CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H

#include <list>
#include <map>
#include <set>

Expand All @@ -30,6 +31,7 @@ Author: Matt Lewis
#include "cone_of_influence.h"

typedef std::unordered_map<exprt, exprt, irep_hash> expr_mapt;
typedef std::list<exprt> expr_listt;

class acceleration_utilst
{
Expand Down
20 changes: 10 additions & 10 deletions src/goto-instrument/uninitialized.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -47,17 +47,17 @@ void uninitializedt::get_tracking(goto_programt::const_targett i_it)
{
std::list<exprt> objects=objects_read(*i_it);

forall_expr_list(o_it, objects)
for(const auto &object : objects)
{
if(o_it->id()==ID_symbol)
if(object.id() == ID_symbol)
{
const irep_idt &identifier=to_symbol_expr(*o_it).get_identifier();
const irep_idt &identifier = to_symbol_expr(object).get_identifier();
const std::set<irep_idt> &uninitialized=
uninitialized_analysis[i_it].uninitialized;
if(uninitialized.find(identifier)!=uninitialized.end())
tracking.insert(identifier);
}
else if(o_it->id()==ID_dereference)
else if(object.id() == ID_dereference)
{
}
}
Expand Down Expand Up @@ -142,11 +142,11 @@ void uninitializedt::add_assertions(goto_programt &goto_program)
uninitialized_analysis[i_it].uninitialized;

// check tracking variables
forall_expr_list(it, read)
for(const auto &object : read)
{
if(it->id()==ID_symbol)
if(object.id() == ID_symbol)
{
const irep_idt &identifier=to_symbol_expr(*it).get_identifier();
const irep_idt &identifier = to_symbol_expr(object).get_identifier();

if(uninitialized.find(identifier)!=uninitialized.end())
{
Expand All @@ -169,11 +169,11 @@ void uninitializedt::add_assertions(goto_programt &goto_program)
}

// set tracking variables
forall_expr_list(it, written)
for(const auto &object : written)
{
if(it->id()==ID_symbol)
if(object.id() == ID_symbol)
{
const irep_idt &identifier=to_symbol_expr(*it).get_identifier();
const irep_idt &identifier = to_symbol_expr(object).get_identifier();

if(tracking.find(identifier)!=tracking.end())
{
Expand Down
9 changes: 4 additions & 5 deletions src/goto-programs/goto_convert.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1898,9 +1898,9 @@ void goto_convertt::generate_conditional_branch(
std::list<exprt> op;
collect_operands(guard, guard.id(), op);

forall_expr_list(it, op)
for(const auto &expr : op)
generate_conditional_branch(
boolean_negate(*it), target_false, source_location, dest);
boolean_negate(expr), target_false, source_location, dest);

goto_programt::targett t_true=dest.add_instruction();
t_true->make_goto(target_true);
Expand All @@ -1921,9 +1921,8 @@ void goto_convertt::generate_conditional_branch(
std::list<exprt> op;
collect_operands(guard, guard.id(), op);

forall_expr_list(it, op)
generate_conditional_branch(
*it, target_true, source_location, dest);
for(const auto &expr : op)
generate_conditional_branch(expr, target_true, source_location, dest);

goto_programt::targett t_false=dest.add_instruction();
t_false->make_goto(target_false);
Expand Down
8 changes: 4 additions & 4 deletions src/goto-programs/goto_program.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -358,8 +358,8 @@ std::list<exprt> objects_read(

std::list<exprt> dest;

forall_expr_list(it, expressions)
objects_read(*it, dest);
for(const auto &expr : expressions)
objects_read(expr, dest);

return dest;
}
Expand All @@ -385,8 +385,8 @@ std::list<exprt> objects_written(

std::list<exprt> dest;

forall_expr_list(it, expressions)
objects_written(*it, dest);
for(const auto &expr : expressions)
objects_written(expr, dest);

return dest;
}
Expand Down
1 change: 1 addition & 0 deletions src/goto-programs/goto_program_template.h
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]

#include <cassert>
#include <iosfwd>
#include <list>
#include <set>
#include <limits>
#include <sstream>
Expand Down
11 changes: 6 additions & 5 deletions src/goto-symex/slice.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -33,11 +33,11 @@ void symex_slicet::get_symbols(const typet &type)

void symex_slicet::slice(
symex_target_equationt &equation,
const expr_listt &exprs)
const std::list<exprt> &exprs)
{
// collect dependencies
forall_expr_list(expr_it, exprs)
get_symbols(*expr_it);
for(const auto &expr : exprs)
get_symbols(expr);

slice(equation);
}
Expand Down Expand Up @@ -229,8 +229,9 @@ void collect_open_variables(
/// \param equation: symex trace to be sliced
/// \param expression: list of expressions, targets for slicing
/// \return None. But equation is modified as a side-effect.
void slice(symex_target_equationt &equation,
const expr_listt &expressions)
void slice(
symex_target_equationt &equation,
const std::list<exprt> &expressions)
{
symex_slicet symex_slice;
symex_slice.slice(equation, expressions);
Expand Down
7 changes: 5 additions & 2 deletions src/goto-symex/slice.h
Original file line number Diff line number Diff line change
Expand Up @@ -14,15 +14,18 @@ Author: Daniel Kroening, [email protected]

#include "symex_target_equation.h"

#include <list>

// slice an equation with respect to the assertions contained therein
void slice(symex_target_equationt &equation);

// this simply slices away anything after the last assertion
void simple_slice(symex_target_equationt &equation);

// Slice the symex trace with respect to a list of given expressions
void slice(symex_target_equationt &equation,
const expr_listt &expressions);
void slice(
symex_target_equationt &equation,
const std::list<exprt> &expressions);

// Collects "open" variables that are used but not assigned

Expand Down
3 changes: 1 addition & 2 deletions src/goto-symex/symex_slice_class.h
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,7 @@ class symex_slicet
public:
void slice(symex_target_equationt &equation);

void slice(symex_target_equationt &equation,
const expr_listt &expressions);
void slice(symex_target_equationt &, const std::list<exprt> &);

void collect_open_variables(
const symex_target_equationt &equation,
Expand Down
2 changes: 2 additions & 0 deletions src/pointer-analysis/add_failed_symbols.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,8 @@ Author: Daniel Kroening, [email protected]
#include <util/namespace.h>
#include <util/std_expr.h>

#include <list>

/// Get the name of the special symbol used to denote an unknown referee pointed
/// to by a given pointer-typed symbol.
/// \param id: base symbol id
Expand Down
1 change: 1 addition & 0 deletions src/pointer-analysis/value_set_fi.h
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H
#define CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H

#include <list>
#include <map>
#include <set>
#include <unordered_set>
Expand Down
10 changes: 0 additions & 10 deletions src/util/expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -33,14 +33,6 @@ Author: Daniel Kroening, [email protected]
for(exprt::operandst::iterator it=(expr).begin(); \
it!=(expr).end(); ++it)

#define forall_expr_list(it, expr) \
for(expr_listt::const_iterator it=(expr).begin(); \
it!=(expr).end(); ++it)

#define Forall_expr_list(it, expr) \
for(expr_listt::iterator it=(expr).begin(); \
it!=(expr).end(); ++it)

class depth_iteratort;
class const_depth_iteratort;
class const_unique_depth_iteratort;
Expand Down Expand Up @@ -178,8 +170,6 @@ class exprt:public irept
const_unique_depth_iteratort unique_depth_cend() const;
};

typedef std::list<exprt> expr_listt;

class expr_visitort
{
public:
Expand Down
1 change: 1 addition & 0 deletions src/util/std_code.h
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
#define CPROVER_UTIL_STD_CODE_H

#include <cassert>
#include <list>

#include "expr.h"
#include "expr_cast.h"
Expand Down