(s));
@@ -315,7 +315,7 @@ class ait:public ai_baset
sequential_fixedpoint(goto_functions, ns);
}
-private:
+private:
// to enforce that domainT is derived from ai_domain_baset
void dummy(const domainT &s) { const statet &x=s; (void)x; }
diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp
index adefb37fb06..347bcd0a0b2 100644
--- a/src/analyses/call_graph.cpp
+++ b/src/analyses/call_graph.cpp
@@ -19,7 +19,7 @@ Function: call_grapht::call_grapht
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -35,7 +35,7 @@ Function: call_grapht::call_grapht
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -56,7 +56,7 @@ Function: call_grapht::add
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -83,7 +83,7 @@ Function: call_grapht::add
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -102,7 +102,7 @@ Function: call_grapht::output_dot
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -119,7 +119,7 @@ void call_grapht::output_dot(std::ostream &out) const
<< " [arrowhead=\"vee\"];"
<< "\n";
}
-
+
out << "}\n";
}
@@ -131,7 +131,7 @@ Function: call_grapht::output
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -154,7 +154,7 @@ Function: call_grapht::output_xml
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
diff --git a/src/analyses/call_graph.h b/src/analyses/call_graph.h
index beceb50b792..935f6a94f9d 100644
--- a/src/analyses/call_graph.h
+++ b/src/analyses/call_graph.h
@@ -28,7 +28,7 @@ class call_grapht
grapht graph;
void add(const irep_idt &caller, const irep_idt &callee);
-
+
protected:
void add(const irep_idt &function,
const goto_programt &body);
diff --git a/src/analyses/cfg_dominators.h b/src/analyses/cfg_dominators.h
index 8fda453a7eb..c80754e4f1f 100644
--- a/src/analyses/cfg_dominators.h
+++ b/src/analyses/cfg_dominators.h
@@ -136,7 +136,7 @@ void cfg_dominators_templatet::fixedpoint(P &program)
typename cfgt::nodet &n=cfg[cfg.entry_map[entry_node]];
n.dominators.insert(entry_node);
- for(typename cfgt::edgest::const_iterator
+ for(typename cfgt::edgest::const_iterator
s_it=(post_dom?n.in:n.out).begin();
s_it!=(post_dom?n.in:n.out).end();
++s_it)
@@ -151,7 +151,7 @@ void cfg_dominators_templatet
::fixedpoint(P &program)
bool changed=false;
typename cfgt::nodet &node=cfg[cfg.entry_map[current]];
if(node.dominators.empty())
- for(typename cfgt::edgest::const_iterator
+ for(typename cfgt::edgest::const_iterator
p_it=(post_dom?node.out:node.in).begin();
!changed && p_it!=(post_dom?node.out:node.in).end();
++p_it)
@@ -163,11 +163,11 @@ void cfg_dominators_templatet
::fixedpoint(P &program)
}
// compute intersection of predecessors
- for(typename cfgt::edgest::const_iterator
+ for(typename cfgt::edgest::const_iterator
p_it=(post_dom?node.out:node.in).begin();
p_it!=(post_dom?node.out:node.in).end();
++p_it)
- {
+ {
const target_sett &other=cfg[p_it->first].dominators;
if(other.empty())
continue;
@@ -198,7 +198,7 @@ void cfg_dominators_templatet
::fixedpoint(P &program)
if(changed) // fixed point for node reached?
{
- for(typename cfgt::edgest::const_iterator
+ for(typename cfgt::edgest::const_iterator
s_it=(post_dom?node.in:node.out).begin();
s_it!=(post_dom?node.in:node.out).end();
++s_it)
@@ -229,7 +229,7 @@ void cfg_dominators_templatet
::output(std::ostream &out) const
it!=cfg.entry_map.end(); ++it)
{
unsigned n=it->first->location_number;
-
+
if(post_dom)
out << n << " post-dominated by ";
else
@@ -238,7 +238,7 @@ void cfg_dominators_templatet
::output(std::ostream &out) const
d_it!=it->second.dominators.end();)
{
out << (*d_it)->location_number;
- if (++d_it!=it->second.dominators.end())
+ if (++d_it!=it->second.dominators.end())
out << ", ";
}
out << "\n";
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index 7e66937efee..66fb6ef71b3 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -85,7 +85,7 @@ void constant_propagator_domaint::transform(
std::cout << "before:\n";
output(std::cout,ai,ns);
#endif
-
+
if(from->is_decl())
{
const code_declt &code_decl=to_code_decl(from->code);
@@ -105,7 +105,7 @@ void constant_propagator_domaint::transform(
}
else if(from->is_goto())
{
- exprt g;
+ exprt g;
if(from->get_target()==to)
g = simplify_expr(from->guard, ns);
else
@@ -121,7 +121,7 @@ void constant_propagator_domaint::transform(
else if(from->is_function_call())
{
const exprt &function=to_code_function_call(from->code).function();
-
+
if(function.id()==ID_symbol)
{
const irep_idt &identifier=to_symbol_expr(function).get_identifier();
@@ -168,14 +168,14 @@ bool constant_propagator_domaint::two_way_propagate_rec(
std::cout << "two_way_propagate_rec: " << from_expr(ns,"",expr) << '\n';
#endif
bool change = false;
-
+
if(expr.id()==ID_and)
{
// need a fixed point here to get the most out of it
do
{
change = false;
-
+
forall_operands(it, expr)
if(two_way_propagate_rec(*it, ns))
change = true;
@@ -184,10 +184,10 @@ bool constant_propagator_domaint::two_way_propagate_rec(
}
else if(expr.id()==ID_equal)
{
- const exprt &lhs = expr.op0();
+ const exprt &lhs = expr.op0();
const exprt &rhs = expr.op1();
- // two-way propagation
+ // two-way propagation
valuest copy_values = values;
assign_rec(copy_values, lhs, rhs, ns);
if(!values.is_constant(rhs) || values.is_constant(lhs))
@@ -238,12 +238,12 @@ Function: constant_propagator_domaint::valuest::is_constant
bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
{
- if(expr.id()==ID_side_effect &&
- to_side_effect_expr(expr).get_statement()==ID_nondet)
+ if(expr.id()==ID_side_effect &&
+ to_side_effect_expr(expr).get_statement()==ID_nondet)
return false;
- if(expr.id()==ID_side_effect &&
- to_side_effect_expr(expr).get_statement()==ID_malloc)
+ if(expr.id()==ID_side_effect &&
+ to_side_effect_expr(expr).get_statement()==ID_malloc)
return false;
if(expr.id()==ID_symbol)
@@ -278,16 +278,16 @@ bool constant_propagator_domaint::valuest::is_constant_address_of(const exprt &e
if(expr.id()==ID_index)
return is_constant_address_of(to_index_expr(expr).array()) &&
is_constant(to_index_expr(expr).index());
-
+
if(expr.id()==ID_member)
return is_constant_address_of(to_member_expr(expr).struct_op());
-
+
if(expr.id()==ID_dereference)
return is_constant(to_dereference_expr(expr).pointer());
if(expr.id()==ID_string_constant)
return true;
-
+
return true;
}
@@ -341,7 +341,7 @@ void constant_propagator_domaint::valuest::output(
if(is_bottom)
out << " bottom\n";
- for(replace_symbolt::expr_mapt::const_iterator
+ for(replace_symbolt::expr_mapt::const_iterator
it=replace_const.expr_map.begin();
it!=replace_const.expr_map.end();
++it)
@@ -383,7 +383,7 @@ Function: constant_propagator_domaint::valuest::merge
bool constant_propagator_domaint::valuest::merge(const valuest &src)
{
- //nothing to do
+ //nothing to do
if(src.is_bottom)
return false;
@@ -394,11 +394,11 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src)
is_bottom = src.is_bottom;
return true;
}
-
+
bool changed = false;
//set everything to top that is not in src
- for(replace_symbolt::expr_mapt::const_iterator
+ for(replace_symbolt::expr_mapt::const_iterator
it=replace_const.expr_map.begin();
it!=replace_const.expr_map.end();
)
@@ -413,12 +413,12 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src)
else ++it;
}
- for(replace_symbolt::expr_mapt::const_iterator
+ for(replace_symbolt::expr_mapt::const_iterator
it=src.replace_const.expr_map.begin();
it!=src.replace_const.expr_map.end();
++it)
- {
- replace_symbolt::expr_mapt::iterator
+ {
+ replace_symbolt::expr_mapt::iterator
c_it = replace_const.expr_map.find(it->first);
if(c_it != replace_const.expr_map.end())
@@ -457,15 +457,15 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src)
{
if(src.is_bottom || is_bottom)
return false;
-
+
bool changed = false;
- for(replace_symbolt::expr_mapt::const_iterator
+ for(replace_symbolt::expr_mapt::const_iterator
it=src.replace_const.expr_map.begin();
it!=src.replace_const.expr_map.end();
++it)
{
- replace_symbolt::expr_mapt::iterator
+ replace_symbolt::expr_mapt::iterator
c_it = replace_const.expr_map.find(it->first);
if(c_it != replace_const.expr_map.end())
@@ -513,7 +513,7 @@ Function: constant_propagator_ait::replace
Inputs:
- Outputs:
+ Outputs:
Purpose:
@@ -533,7 +533,7 @@ Function: constant_propagator_ait::replace
Inputs:
- Outputs:
+ Outputs:
Purpose:
@@ -568,8 +568,8 @@ void constant_propagator_ait::replace(
{
s_it->second.values.replace_const(to_code_function_call(it->code).function());
simplify_expr(to_code_function_call(it->code).function(), ns);
-
- exprt::operandst &args =
+
+ exprt::operandst &args =
to_code_function_call(it->code).arguments();
for(exprt::operandst::iterator o_it = args.begin();
@@ -593,14 +593,14 @@ Function: constant_propagator_ait::replace_types_rec
Inputs:
- Outputs:
+ Outputs:
Purpose:
\*******************************************************************/
void constant_propagator_ait::replace_types_rec(
- const replace_symbolt &replace_const,
+ const replace_symbolt &replace_const,
exprt &expr)
{
replace_const(expr.type());
@@ -608,4 +608,3 @@ void constant_propagator_ait::replace_types_rec(
Forall_operands(it, expr)
replace_types_rec(replace_const, *it);
}
-
diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h
index 7c7d7086373..36170c71a74 100644
--- a/src/analyses/constant_propagator.h
+++ b/src/analyses/constant_propagator.h
@@ -24,22 +24,22 @@ class constant_propagator_domaint:public ai_domain_baset
{
public:
valuest():is_bottom(true) { }
-
+
// maps variables to constants
replace_symbol_extt replace_const;
bool is_bottom;
-
+
void output(std::ostream &, const namespacet &) const;
-
+
bool merge(const valuest &src);
bool meet(const valuest &src);
-
+
inline void set_to_bottom()
{
replace_const.clear();
is_bottom = true;
}
-
+
inline void set_to(const irep_idt &lhs_id, const exprt &rhs_val)
{
replace_const.expr_map[lhs_id] = rhs_val;
@@ -59,7 +59,7 @@ class constant_propagator_domaint:public ai_domain_baset
{
return set_to_top(expr.get_identifier());
}
-
+
inline void set_to_top()
{
replace_const.clear();
@@ -68,7 +68,7 @@ class constant_propagator_domaint:public ai_domain_baset
};
valuest values;
-
+
protected:
void assign(
valuest &dest,
@@ -115,7 +115,7 @@ class constant_propagator_ait:public ait
const namespacet &);
void replace_types_rec(
- const replace_symbolt &replace_const,
+ const replace_symbolt &replace_const,
exprt &expr);
};
diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
index 8ed4da40997..883ea1ef188 100644
--- a/src/analyses/custom_bitvector_analysis.cpp
+++ b/src/analyses/custom_bitvector_analysis.cpp
@@ -21,7 +21,7 @@ Function: custom_bitvector_domaint::set_bit
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -35,15 +35,15 @@ void custom_bitvector_domaint::set_bit(
case SET_MUST:
set_bit(must_bits[identifier], bit_nr);
break;
-
+
case CLEAR_MUST:
clear_bit(must_bits[identifier], bit_nr);
break;
-
+
case SET_MAY:
set_bit(may_bits[identifier], bit_nr);
break;
-
+
case CLEAR_MAY:
clear_bit(may_bits[identifier], bit_nr);
break;
@@ -58,7 +58,7 @@ Function: custom_bitvector_domaint::set_bit
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -79,7 +79,7 @@ Function: custom_bitvector_domaint::object2id
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -92,7 +92,7 @@ irep_idt custom_bitvector_domaint::object2id(const exprt &src)
else if(src.id()==ID_dereference)
{
const exprt &op=to_dereference_expr(src).pointer();
-
+
if(op.id()==ID_address_of)
{
return object2id(to_address_of_expr(op).object());
@@ -124,7 +124,7 @@ Function: custom_bitvector_domaint::assign_lhs
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -144,7 +144,7 @@ Function: custom_bitvector_domaint::assign_lhs
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -158,7 +158,7 @@ void custom_bitvector_domaint::assign_lhs(
must_bits.erase(identifier);
else
must_bits[identifier]=vectors.must_bits;
-
+
if(vectors.may_bits==0)
may_bits.erase(identifier);
else
@@ -173,7 +173,7 @@ Function: custom_bitvector_domaint::get_rhs
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -184,10 +184,10 @@ custom_bitvector_domaint::vectorst
bitst::const_iterator may_it=may_bits.find(identifier);
if(may_it!=may_bits.end()) vectors.may_bits=may_it->second;
-
+
bitst::const_iterator must_it=must_bits.find(identifier);
if(must_it!=must_bits.end()) vectors.must_bits=must_it->second;
-
+
return vectors;
}
@@ -199,7 +199,7 @@ Function: custom_bitvector_domaint::get_rhs
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -223,7 +223,7 @@ custom_bitvector_domaint::vectorst
vectorst v_false=get_rhs(to_if_expr(rhs).false_case());
return merge(v_true, v_false);
}
-
+
return vectorst();
}
@@ -235,7 +235,7 @@ Function: custom_bitvector_analysist::get_bit_nr
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -250,9 +250,9 @@ unsigned custom_bitvector_analysist::get_bit_nr(
return get_bit_nr(to_index_expr(string_expr).array());
else if(string_expr.id()==ID_string_constant)
{
- irep_idt value=string_expr.get(ID_value);
+ irep_idt value=string_expr.get(ID_value);
return bits(value);
- }
+ }
else
return bits("(unknown)");
}
@@ -265,7 +265,7 @@ Function: custom_bitvector_domaint::aliases
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -282,7 +282,7 @@ std::set custom_bitvector_analysist::aliases(
else if(src.id()==ID_dereference)
{
exprt pointer=to_dereference_expr(src).pointer();
-
+
std::set pointer_set=
local_may_alias_factory(loc).get(loc, pointer);
@@ -295,9 +295,9 @@ std::set custom_bitvector_analysist::aliases(
{
result.insert(dereference_exprt(*p_it));
}
-
+
result.insert(src);
-
+
return result;
}
else if(src.id()==ID_typecast)
@@ -316,7 +316,7 @@ Function: custom_bitvector_domaint::transform
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -340,15 +340,15 @@ void custom_bitvector_domaint::transform(
// may alias other stuff
std::set lhs_set=cba.aliases(code_assign.lhs(), from);
-
+
vectorst rhs_vectors=get_rhs(code_assign.rhs());
-
+
for(std::set::const_iterator
l_it=lhs_set.begin(); l_it!=lhs_set.end(); l_it++)
{
assign_lhs(*l_it, rhs_vectors);
}
-
+
// is it a pointer?
if(code_assign.lhs().type().id()==ID_pointer)
{
@@ -386,7 +386,7 @@ void custom_bitvector_domaint::transform(
{
const code_function_callt &code_function_call=to_code_function_call(instruction.code);
const exprt &function=code_function_call.function();
-
+
if(function.id()==ID_symbol)
{
const irep_idt &identifier=to_symbol_expr(function).get_identifier();
@@ -400,9 +400,9 @@ void custom_bitvector_domaint::transform(
{
unsigned bit_nr=
cba.get_bit_nr(code_function_call.arguments()[1]);
-
+
modet mode;
-
+
if(identifier=="__CPROVER_set_must")
mode=SET_MUST;
else if(identifier=="__CPROVER_clear_must")
@@ -413,9 +413,9 @@ void custom_bitvector_domaint::transform(
mode=CLEAR_MAY;
else
assert(false);
-
+
exprt lhs=code_function_call.arguments()[0];
-
+
if(lhs.is_constant() &&
to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all
{
@@ -443,10 +443,10 @@ void custom_bitvector_domaint::transform(
else
{
dereference_exprt deref(lhs);
-
+
// may alias other stuff
std::set lhs_set=cba.aliases(deref, from);
-
+
for(std::set::const_iterator
l_it=lhs_set.begin(); l_it!=lhs_set.end(); l_it++)
{
@@ -458,11 +458,11 @@ void custom_bitvector_domaint::transform(
}
}
break;
-
+
case OTHER:
{
const irep_idt &statement=instruction.code.get_statement();
-
+
if(statement=="set_may" ||
statement=="set_must" ||
statement=="clear_may" ||
@@ -472,9 +472,9 @@ void custom_bitvector_domaint::transform(
unsigned bit_nr=
cba.get_bit_nr(instruction.code.op1());
-
+
modet mode;
-
+
if(statement=="set_must")
mode=SET_MUST;
else if(statement=="clear_must")
@@ -485,9 +485,9 @@ void custom_bitvector_domaint::transform(
mode=CLEAR_MAY;
else
assert(false);
-
+
exprt lhs=instruction.code.op0();
-
+
if(lhs.is_constant() &&
to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all
{
@@ -515,10 +515,10 @@ void custom_bitvector_domaint::transform(
else
{
dereference_exprt deref(lhs);
-
+
// may alias other stuff
std::set lhs_set=cba.aliases(deref, from);
-
+
for(std::set::const_iterator
l_it=lhs_set.begin(); l_it!=lhs_set.end(); l_it++)
{
@@ -528,12 +528,12 @@ void custom_bitvector_domaint::transform(
}
}
break;
-
+
case GOTO:
if(has_get_must_or_may(instruction.guard))
{
exprt guard=instruction.guard;
-
+
if(to!=from->get_target()) guard.make_not();
exprt result=eval(guard, cba);
@@ -556,7 +556,7 @@ Function: custom_bitvector_domaint::output
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -570,14 +570,14 @@ void custom_bitvector_domaint::output(
const custom_bitvector_analysist &cba=
static_cast(ai);
-
+
for(bitst::const_iterator it=may_bits.begin();
it!=may_bits.end();
it++)
{
out << it->first << " MAY:";
bit_vectort b=it->second;
-
+
for(unsigned i=0; b!=0; i++, b>>=1)
if(b&1)
{
@@ -616,7 +616,7 @@ Function: custom_bitvector_domaint::merge
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -667,7 +667,7 @@ bool custom_bitvector_domaint::merge(
if(old!=a_it->second) changed=true;
}
}
-
+
// erase blank ones
erase_blank_vectors(may_bits);
erase_blank_vectors(must_bits);
@@ -708,7 +708,7 @@ Function: custom_bitvector_domaint::has_get_must_or_may
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -717,7 +717,7 @@ bool custom_bitvector_domaint::has_get_must_or_may(const exprt &src)
if(src.id()=="get_must" ||
src.id()=="get_may")
return true;
-
+
forall_operands(it, src)
if(has_get_must_or_may(*it)) return true;
@@ -732,7 +732,7 @@ Function: custom_bitvector_domaint::eval
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -748,7 +748,7 @@ exprt custom_bitvector_domaint::eval(
custom_bitvector_analysis.get_bit_nr(src.op1());
exprt pointer=src.op0();
-
+
if(pointer.is_constant() &&
to_constant_expr(pointer).get_value()==ID_NULL) // NULL means all
{
@@ -761,7 +761,7 @@ exprt custom_bitvector_domaint::eval(
{
if(get_bit(b_it->second, bit_nr)) return true_exprt();
}
-
+
return false_exprt();
}
else if(src.id()=="get_must")
@@ -797,7 +797,7 @@ exprt custom_bitvector_domaint::eval(
exprt tmp=src;
Forall_operands(it, tmp)
*it=eval(*it, custom_bitvector_analysis);
-
+
return tmp;
}
}
@@ -810,7 +810,7 @@ Function: custom_bitvector_analysist::instrument
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -826,7 +826,7 @@ Function: custom_bitvector_analysist::check
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -841,7 +841,7 @@ void custom_bitvector_analysist::check(
forall_goto_functions(f_it, goto_functions)
{
if(!f_it->second.body.has_assertion()) continue;
-
+
if(f_it->first=="__actual_thread_spawn")
continue;
@@ -852,7 +852,7 @@ void custom_bitvector_analysist::check(
{
exprt result;
irep_idt description;
-
+
if(i_it->is_assert())
{
if(!custom_bitvector_domaint::has_get_must_or_may(i_it->guard))
@@ -862,7 +862,7 @@ void custom_bitvector_analysist::check(
exprt tmp=eval(i_it->guard, i_it);
result=simplify_expr(tmp, ns);
-
+
description=i_it->source_location.get_comment();
}
else
@@ -875,7 +875,7 @@ void custom_bitvector_analysist::check(
out << "SUCCESS";
else if(result.is_false())
out << "FAILURE";
- else
+ else
out << "UNKNOWN";
out << "\">\n";
out << xml(i_it->source_location);
@@ -905,7 +905,7 @@ void custom_bitvector_analysist::check(
if(!use_xml)
out << '\n';
}
-
+
if(!use_xml)
out << "SUMMARY: " << pass << " pass, " << fail << " fail, "
<< unknown << " unknown\n";
diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h
index 9433b919408..b700c0b35ed 100644
--- a/src/analyses/custom_bitvector_analysis.h
+++ b/src/analyses/custom_bitvector_analysis.h
@@ -17,7 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
/*******************************************************************\
Class: custom_bitvector_domaint
-
+
Purpose:
\*******************************************************************/
@@ -65,9 +65,9 @@ class custom_bitvector_domaint:public ai_domain_baset
locationt to);
typedef unsigned long long bit_vectort;
-
+
typedef std::map bitst;
-
+
struct vectorst
{
bit_vectort may_bits, must_bits;
@@ -75,7 +75,7 @@ class custom_bitvector_domaint:public ai_domain_baset
{
}
};
-
+
static vectorst merge(const vectorst &a, const vectorst &b)
{
vectorst result;
@@ -83,16 +83,16 @@ class custom_bitvector_domaint:public ai_domain_baset
result.must_bits=a.must_bits&b.must_bits;
return result;
}
-
+
bitst may_bits, must_bits;
-
+
void assign_lhs(const exprt &, const vectorst &);
void assign_lhs(const irep_idt &, const vectorst &);
vectorst get_rhs(const exprt &) const;
vectorst get_rhs(const irep_idt &) const;
bool is_bottom;
-
+
custom_bitvector_domaint():is_bottom(true)
{
}
@@ -102,7 +102,7 @@ class custom_bitvector_domaint:public ai_domain_baset
const exprt &src,
custom_bitvector_analysist &) const;
-protected:
+protected:
typedef enum { SET_MUST, CLEAR_MUST, SET_MAY, CLEAR_MAY } modet;
void set_bit(const exprt &, unsigned bit_nr, modet);
@@ -112,24 +112,24 @@ class custom_bitvector_domaint:public ai_domain_baset
{
dest|=(1ll<
+class custom_bitvector_analysist:public ait
{
public:
void instrument(goto_functionst &);
@@ -144,7 +144,7 @@ class custom_bitvector_analysist:public ait
typedef numbering bitst;
bitst bits;
-
+
protected:
virtual void initialize(const goto_functionst &_goto_functions)
{
@@ -154,7 +154,7 @@ class custom_bitvector_analysist:public ait
friend class custom_bitvector_domaint;
local_may_alias_factoryt local_may_alias_factory;
-
+
std::set aliases(const exprt &, locationt loc);
};
diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp
index 44bcf2211eb..2e20389259d 100644
--- a/src/analyses/dependence_graph.cpp
+++ b/src/analyses/dependence_graph.cpp
@@ -379,4 +379,3 @@ void dependence_grapht::add_dep(
nodes[n_from].out[n_to].add(kind);
nodes[n_to].in[n_from].add(kind);
}
-
diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h
index 1b07b4ec140..cb25b7ff88b 100644
--- a/src/analyses/dependence_graph.h
+++ b/src/analyses/dependence_graph.h
@@ -177,4 +177,3 @@ class dependence_grapht:
};
#endif
-
diff --git a/src/analyses/dirty.cpp b/src/analyses/dirty.cpp
index aa1f4db55e1..bc4327581cd 100644
--- a/src/analyses/dirty.cpp
+++ b/src/analyses/dirty.cpp
@@ -53,7 +53,7 @@ void dirtyt::find_dirty(const exprt &expr)
find_dirty_address_of(address_of_expr.object());
return;
}
-
+
forall_operands(it, expr)
find_dirty(*it);
}
diff --git a/src/analyses/dirty.h b/src/analyses/dirty.h
index 709366ad33a..a200690b963 100644
--- a/src/analyses/dirty.h
+++ b/src/analyses/dirty.h
@@ -47,13 +47,13 @@ class dirtyt
{
return dirty;
}
-
+
protected:
void build(const goto_functiont &goto_function);
// variables whose address is taken
id_sett dirty;
-
+
void find_dirty(const exprt &expr);
void find_dirty_address_of(const exprt &expr);
};
diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp
index 1cc15cd43c8..7d610c3198a 100644
--- a/src/analyses/escape_analysis.cpp
+++ b/src/analyses/escape_analysis.cpp
@@ -20,7 +20,7 @@ Function: escape_domaint::is_tracked
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -32,7 +32,7 @@ bool escape_domaint::is_tracked(const symbol_exprt &symbol)
identifier=="__CPROVER_dead_object" ||
identifier=="__CPROVER_deallocated")
return false;
-
+
return true;
}
@@ -44,7 +44,7 @@ Function: escape_domaint::get_function
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -59,7 +59,7 @@ irep_idt escape_domaint::get_function(const exprt &lhs)
irep_idt identifier=to_symbol_expr(lhs).get_identifier();
return identifier;
}
-
+
return irep_idt();
}
@@ -71,7 +71,7 @@ Function: escape_domaint::assign_lhs_cleanup
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -85,7 +85,7 @@ void escape_domaint::assign_lhs_cleanup(
if(is_tracked(symbol_expr))
{
irep_idt identifier=symbol_expr.get_identifier();
-
+
if(cleanup_functions.empty())
cleanup_map.erase(identifier);
else
@@ -102,7 +102,7 @@ Function: escape_domaint::assign_lhs_aliases
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -137,7 +137,7 @@ Function: escape_domaint::get_rhs_cleanup
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -154,7 +154,7 @@ void escape_domaint::get_rhs_cleanup(
const escape_domaint::cleanup_mapt::const_iterator m_it=
cleanup_map.find(identifier);
-
+
if(m_it!=cleanup_map.end())
cleanup_functions.insert(m_it->second.cleanup_functions.begin(),
m_it->second.cleanup_functions.end());
@@ -179,7 +179,7 @@ Function: escape_domaint::get_rhs_aliases
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -194,7 +194,7 @@ void escape_domaint::get_rhs_aliases(
{
irep_idt identifier=symbol_expr.get_identifier();
alias_set.insert(identifier);
-
+
for(aliasest::const_iterator it=aliases.begin();
it!=aliases.end();
it++)
@@ -225,7 +225,7 @@ Function: escape_domaint::get_rhs_aliases_address_of
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -256,7 +256,7 @@ Function: escape_domaint::transform
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -277,7 +277,7 @@ void escape_domaint::transform(
case ASSIGN:
{
const code_assignt &code_assign=to_code_assign(instruction.code);
-
+
std::set cleanup_functions;
get_rhs_cleanup(code_assign.rhs(), cleanup_functions);
assign_lhs_cleanup(code_assign.lhs(), cleanup_functions);
@@ -308,7 +308,7 @@ void escape_domaint::transform(
{
const code_function_callt &code_function_call=to_code_function_call(instruction.code);
const exprt &function=code_function_call.function();
-
+
if(function.id()==ID_symbol)
{
const irep_idt &identifier=to_symbol_expr(function).get_identifier();
@@ -326,7 +326,7 @@ void escape_domaint::transform(
// may alias other stuff
std::set lhs_set;
get_rhs_aliases(lhs, lhs_set);
-
+
for(std::set::const_iterator
l_it=lhs_set.begin(); l_it!=lhs_set.end(); l_it++)
{
@@ -338,7 +338,7 @@ void escape_domaint::transform(
}
}
break;
-
+
case END_FUNCTION:
// This is the edge to the call site.
break;
@@ -355,7 +355,7 @@ Function: escape_domaint::output
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -382,13 +382,13 @@ void escape_domaint::output(
out << ' ' << *c_it;
out << '\n';
}
-
+
for(aliasest::const_iterator a_it1=aliases.begin();
a_it1!=aliases.end();
a_it1++)
{
bool first=true;
-
+
for(aliasest::const_iterator a_it2=aliases.begin();
a_it2!=aliases.end();
a_it2++)
@@ -413,7 +413,7 @@ Function: escape_domaint::merge
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -443,9 +443,9 @@ bool escape_domaint::merge(
a_cleanup.insert(b_cleanup.begin(), b_cleanup.end());
if(a_cleanup.size()!=old_size) changed=true;
}
-
+
// kill empty ones
-
+
for(cleanup_mapt::iterator a_it=cleanup_map.begin();
a_it!=cleanup_map.end();
) // no a_it++
@@ -455,13 +455,13 @@ bool escape_domaint::merge(
else
a_it++;
}
-
+
// do union
for(aliasest::const_iterator it=b.aliases.begin();
it!=b.aliases.end(); it++)
{
irep_idt b_root=b.aliases.find(it);
-
+
if(!aliases.same_set(*it, b_root))
{
aliases.make_union(*it, b_root);
@@ -478,7 +478,7 @@ bool escape_domaint::merge(
aliases.isolate(it);
}
#endif
-
+
return changed;
}
@@ -490,18 +490,18 @@ Function: escape_domaint::check_lhs
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
void escape_domaint::check_lhs(
const exprt &lhs,
- std::set &cleanup_functions)
+ std::set &cleanup_functions)
{
if(lhs.id()==ID_symbol)
{
const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
-
+
// pointer with aleanup function?
const escape_domaint::cleanup_mapt::const_iterator m_it=
cleanup_map.find(identifier);
@@ -511,7 +511,7 @@ void escape_domaint::check_lhs(
// count the aliases
unsigned count=0;
-
+
for(aliasest::const_iterator
a_it=aliases.begin();
a_it!=aliases.end();
@@ -540,7 +540,7 @@ Function: escape_analysist::insert_cleanup
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -553,14 +553,14 @@ void escape_analysist::insert_cleanup(
const namespacet &ns)
{
source_locationt source_location=location->source_location;
-
+
for(std::set::const_iterator c_it=cleanup_functions.begin();
c_it!=cleanup_functions.end();
c_it++)
{
symbol_exprt function=ns.lookup(*c_it).symbol_expr();
const code_typet &function_type=to_code_type(function.type());
-
+
goto_function.body.insert_before_swap(location);
code_function_callt code;
code.lhs().make_nil();
@@ -575,7 +575,7 @@ void escape_analysist::insert_cleanup(
if(arg.type()!=param_type) arg.make_typecast(param_type);
code.arguments().push_back(arg);
}
-
+
location->make_function_call(code);
location->source_location=source_location;
}
@@ -589,7 +589,7 @@ Function: escape_analysist::instrument
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -604,7 +604,7 @@ void escape_analysist::instrument(
get_state(i_it);
const goto_programt::instructiont &instruction=*i_it;
-
+
switch(instruction.type)
{
case ASSIGN:
@@ -620,14 +620,14 @@ void escape_analysist::instrument(
case DEAD:
{
const code_deadt &code_dead=to_code_dead(instruction.code);
-
+
std::set cleanup_functions1;
-
+
escape_domaint &d=operator[](i_it);
const escape_domaint::cleanup_mapt::const_iterator m_it=
d.cleanup_map.find("&"+id2string(code_dead.get_identifier()));
-
+
// does it have a cleanup function for the object?
if(m_it!=d.cleanup_map.end())
{
@@ -637,12 +637,12 @@ void escape_analysist::instrument(
}
std::set cleanup_functions2;
-
+
d.check_lhs(code_dead.symbol(), cleanup_functions2);
insert_cleanup(f_it->second, i_it, code_dead.symbol(), cleanup_functions1, true, ns);
insert_cleanup(f_it->second, i_it, code_dead.symbol(), cleanup_functions2, false, ns);
-
+
for(unsigned i=0; i aliasest;
aliasest aliases;
-
+
struct cleanupt
{
std::set cleanup_functions;
};
-
+
typedef std::map cleanup_mapt;
cleanup_mapt cleanup_map;
-
+
bool is_bottom;
-protected:
+protected:
void assign_lhs_cleanup(const exprt &, const std::set &);
void get_rhs_cleanup(const exprt &, std::set &);
void assign_lhs_aliases(const exprt &, const std::set &);
@@ -81,13 +81,13 @@ class escape_domaint:public ai_domain_baset
void get_rhs_aliases_address_of(const exprt &, std::set &);
irep_idt get_function(const exprt &);
void check_lhs(const exprt &, std::set &);
-
+
friend class escape_analysist;
-
+
bool is_tracked(const symbol_exprt &);
};
-class escape_analysist:public ait
+class escape_analysist:public ait
{
public:
void instrument(
@@ -102,7 +102,7 @@ class escape_analysist:public ait
friend class escape_domaint;
numbering bits;
-
+
void insert_cleanup(
goto_functionst::goto_functiont &,
goto_programt::targett,
diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp
index 43df95892ee..e4782b76e73 100644
--- a/src/analyses/flow_insensitive_analysis.cpp
+++ b/src/analyses/flow_insensitive_analysis.cpp
@@ -43,7 +43,7 @@ exprt flow_insensitive_abstract_domain_baset::get_guard(
tmp.make_not();
return tmp;
}
-
+
return from->guard;
}
@@ -67,13 +67,13 @@ exprt flow_insensitive_abstract_domain_baset::get_return_lhs(locationt to) const
if(to->is_end_function())
return static_cast(get_nil_irep());
-
+
// must be the function call
assert(to->is_function_call());
const code_function_callt &code=
to_code_function_call(to_code(to->code));
-
+
return code.lhs();
}
@@ -163,7 +163,7 @@ void flow_insensitive_analysis_baset::output(
const irep_idt &identifier,
std::ostream &out) const
{
- get_state().output(ns, out);
+ get_state().output(ns, out);
}
/*******************************************************************\
@@ -182,15 +182,15 @@ flow_insensitive_analysis_baset::locationt flow_insensitive_analysis_baset::get_
working_sett &working_set)
{
assert(!working_set.empty());
-
+
// working_sett::iterator i=working_set.begin();
// locationt l=i->second;
// working_set.erase(i);
-
+
// pop_heap(working_set.begin(), working_set.end());
locationt l=working_set.top();
working_set.pop();
-
+
return l;
}
@@ -212,21 +212,21 @@ bool flow_insensitive_analysis_baset::fixedpoint(
{
if(goto_program.instructions.empty())
return false;
-
+
working_sett working_set;
-
+
// make_heap(working_set.begin(), working_set.end());
put_in_working_set(
working_set,
goto_program.instructions.begin());
-
+
bool new_data=false;
while(!working_set.empty())
{
locationt l=get_next(working_set);
-
+
if(visit(l, working_set, goto_program, goto_functions))
new_data=true;
}
@@ -253,15 +253,15 @@ bool flow_insensitive_analysis_baset::visit(
const goto_functionst &goto_functions)
{
bool new_data=false;
-
+
#if 0
- std::cout << "Visiting: " << l->function << " " <<
+ std::cout << "Visiting: " << l->function << " " <<
l->location_number << std::endl;
#endif
goto_programt::const_targetst successors;
goto_program.get_successors(l, successors);
-
+
seen_locations.insert(l);
if (statistics.find(l)==statistics.end())
statistics[l]=1;
@@ -277,15 +277,15 @@ bool flow_insensitive_analysis_baset::visit(
if(to_l==goto_program.instructions.end())
continue;
-
+
bool changed=false;
-
+
if(l->is_function_call())
{
// this is a big special case
const code_function_callt &code=
to_code_function_call(to_code(l->code));
-
+
changed=
do_function_call_rec(
l,
@@ -296,17 +296,17 @@ bool flow_insensitive_analysis_baset::visit(
}
else
changed = get_state().transform(ns, l, to_l);
-
+
if(changed || !seen(to_l))
{
- new_data=true;
- put_in_working_set(working_set, to_l);
+ new_data=true;
+ put_in_working_set(working_set, to_l);
}
}
-
+
// if (id2string(l->function).find("debug")!=std::string::npos)
// std::cout << l->function << std::endl; //=="messages::debug")
-
+
// {
// static unsigned state_cntr=0;
// std::string s("pastate"); s += i2string(state_cntr);
@@ -344,33 +344,33 @@ bool flow_insensitive_analysis_baset::do_function_call(
if(!goto_function.body_available())
{
- const code_function_callt &code =
+ const code_function_callt &code =
to_code_function_call(to_code(l_call->code));
-
+
goto_programt temp;
-
+
goto_programt::targett r=temp.add_instruction();
r->make_return();
r->code=code_returnt();
r->function=f_it->first;
r->location_number=0;
-
+
exprt rhs=side_effect_expr_nondett(code.lhs().type());
- r->code.move_to_operands(rhs);
-
- goto_programt::targett t=temp.add_instruction(END_FUNCTION);
+ r->code.move_to_operands(rhs);
+
+ goto_programt::targett t=temp.add_instruction(END_FUNCTION);
t->code.set(ID_identifier, code.function());
t->function=f_it->first;
t->location_number=1;
-
+
locationt l_next=l_call; l_next++;
bool new_data=state.transform(ns, l_call, r);
new_data = state.transform(ns, r, t) || new_data;
new_data = state.transform(ns, t, l_next) || new_data;
-
+
return new_data;
}
-
+
assert(!goto_function.body.instructions.empty());
bool new_data=false;
@@ -378,9 +378,9 @@ bool flow_insensitive_analysis_baset::do_function_call(
{
// get the state at the beginning of the function
locationt l_begin=goto_function.body.instructions.begin();
-
+
// do the edge from the call site to the beginning of the function
- new_data=state.transform(ns, l_call, l_begin);
+ new_data=state.transform(ns, l_call, l_begin);
// do each function at least once
if(functions_done.find(f_it->first)==
@@ -410,9 +410,9 @@ bool flow_insensitive_analysis_baset::do_function_call(
l_next++;
new_data = state.transform(ns, l_end, l_next) || new_data;
}
-
+
return new_data;
-}
+}
/*******************************************************************\
@@ -432,13 +432,13 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
const exprt::operandst &arguments,
statet &state,
const goto_functionst &goto_functions)
-{
+{
bool new_data = false;
-
+
if(function.id()==ID_symbol)
{
const irep_idt &identifier=function.get(ID_identifier);
-
+
if(recursion_set.find(identifier)!=recursion_set.end())
{
// recursion detected!
@@ -446,29 +446,29 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
}
else
recursion_set.insert(identifier);
-
+
goto_functionst::function_mapt::const_iterator it=
goto_functions.function_map.find(identifier);
-
+
if(it==goto_functions.function_map.end())
throw "failed to find function "+id2string(identifier);
-
- new_data =
+
+ new_data =
do_function_call(
l_call,
goto_functions,
it,
arguments,
state);
-
+
recursion_set.erase(identifier);
}
else if(function.id()==ID_if)
{
if(function.operands().size()!=3)
throw "if takes three arguments";
-
- new_data =
+
+ new_data =
do_function_call_rec(
l_call,
function.op1(),
@@ -488,7 +488,7 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
{
// get value set
expr_sett values;
-
+
get_reference_set(function, values);
// now call all of these
@@ -499,19 +499,19 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
if(it->id()==ID_object_descriptor)
{
const object_descriptor_exprt &o=to_object_descriptor_expr(*it);
-
+
// ... but only if they are actually functions.
goto_functionst::function_mapt::const_iterator it=
goto_functions.function_map.find(o.object().get(ID_identifier));
-
+
if (it!=goto_functions.function_map.end())
{
new_data =
do_function_call_rec(
- l_call,
- o.object(),
- arguments,
- state,
+ l_call,
+ o.object(),
+ arguments,
+ state,
goto_functions) || new_data;
}
}
diff --git a/src/analyses/flow_insensitive_analysis.h b/src/analyses/flow_insensitive_analysis.h
index 8906a40b39d..ffe5f3671ad 100644
--- a/src/analyses/flow_insensitive_analysis.h
+++ b/src/analyses/flow_insensitive_analysis.h
@@ -37,15 +37,15 @@ class flow_insensitive_abstract_domain_baset
virtual ~flow_insensitive_abstract_domain_baset()
{
}
-
+
virtual void output(
const namespacet &ns,
std::ostream &out) const
{
}
-
+
typedef hash_set_cont expr_sett;
-
+
virtual void get_reference_set(
const namespacet &ns,
const exprt &expr,
@@ -54,17 +54,17 @@ class flow_insensitive_abstract_domain_baset
// dummy, overload me!
expr_set.clear();
}
-
+
virtual void clear(void)=0;
-
+
protected:
friend class flow_insensitive_analysis_baset;
bool changed;
- // utilities
-
+ // utilities
+
// get guard of a conditional edge
exprt get_guard(locationt from, locationt to) const;
-
+
// get lhs that return value is assigned to
// for an edge that returns from a function
exprt get_return_lhs(locationt to) const;
@@ -75,11 +75,11 @@ class flow_insensitive_analysis_baset
public:
typedef flow_insensitive_abstract_domain_baset statet;
typedef goto_programt::const_targett locationt;
-
+
std::set seen_locations;
-
+
std::map statistics;
-
+
bool seen( const locationt& l )
{
return (seen_locations.find(l)!=seen_locations.end());
@@ -90,7 +90,7 @@ class flow_insensitive_analysis_baset
initialized(false)
{
}
-
+
virtual void initialize(
const goto_programt &goto_program)
{
@@ -99,23 +99,23 @@ class flow_insensitive_analysis_baset
initialized=true;
}
}
-
+
virtual void initialize(
const goto_functionst &goto_functions)
{
if(!initialized)
{
- initialized=true;
+ initialized=true;
}
}
-
+
virtual void update(const goto_programt &goto_program);
-
+
virtual void update(const goto_functionst &goto_functions);
-
+
virtual void operator()(
const goto_programt &goto_program);
-
+
virtual void operator()(
const goto_functionst &goto_functions);
@@ -127,7 +127,7 @@ class flow_insensitive_analysis_baset
{
initialized=false;
}
-
+
virtual void output(
const goto_functionst &goto_functions,
std::ostream &out);
@@ -141,16 +141,16 @@ class flow_insensitive_analysis_baset
protected:
const namespacet &ns;
-
+
virtual void output(
const goto_programt &goto_program,
const irep_idt &identifier,
std::ostream &out) const;
typedef std::priority_queue working_sett;
-
+
locationt get_next(working_sett &working_set);
-
+
void put_in_working_set(
working_sett &working_set,
locationt l)
@@ -162,11 +162,11 @@ class flow_insensitive_analysis_baset
bool fixedpoint(
const goto_programt &goto_program,
const goto_functionst &goto_functions);
-
+
bool fixedpoint(
goto_functionst::function_mapt::const_iterator it,
const goto_functionst &goto_functions);
-
+
void fixedpoint(
const goto_functionst &goto_functions);
@@ -176,21 +176,21 @@ class flow_insensitive_analysis_baset
working_sett &working_set,
const goto_programt &goto_program,
const goto_functionst &goto_functions);
-
+
static locationt successor(locationt l)
{
l++;
return l;
}
-
+
typedef std::set functions_donet;
functions_donet functions_done;
typedef std::set recursion_sett;
recursion_sett recursion_set;
-
+
bool initialized;
-
+
// function calls
bool do_function_call_rec(
locationt l_call,
@@ -207,10 +207,10 @@ class flow_insensitive_analysis_baset
statet &new_state);
// abstract methods
-
+
virtual statet &get_state()=0;
virtual const statet &get_state() const=0;
-
+
typedef flow_insensitive_abstract_domain_baset::expr_sett expr_sett;
virtual void get_reference_set(
@@ -230,13 +230,13 @@ class flow_insensitive_analysist:public flow_insensitive_analysis_baset
}
typedef goto_programt::const_targett locationt;
-
+
virtual void clear()
{
state.clear();
flow_insensitive_analysis_baset::clear();
}
-
+
inline T& get_data() { return state; }
inline const T& get_data() const { return state; }
@@ -245,7 +245,7 @@ class flow_insensitive_analysist:public flow_insensitive_analysis_baset
virtual statet &get_state() { return state; }
- virtual const statet &get_state() const { return state; }
+ virtual const statet &get_state() const { return state; }
void get_reference_set(
const exprt &expr,
@@ -254,7 +254,7 @@ class flow_insensitive_analysist:public flow_insensitive_analysis_baset
state.get_reference_set(ns, expr, expr_set);
}
-private:
+private:
// to enforce that T is derived from abstract_domain_baset
void dummy(const T &s) { const statet &x=dummy1(s); (void)x; }
};
diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp
index 41ba46985e7..0e3e190aa29 100644
--- a/src/analyses/global_may_alias.cpp
+++ b/src/analyses/global_may_alias.cpp
@@ -16,7 +16,7 @@ Function: global_may_alias_domaint::assign_lhs_aliases
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -47,7 +47,7 @@ Function: global_may_alias_domaint::get_rhs_aliases
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -59,7 +59,7 @@ void global_may_alias_domaint::get_rhs_aliases(
{
irep_idt identifier=to_symbol_expr(rhs).get_identifier();
alias_set.insert(identifier);
-
+
for(aliasest::const_iterator it=aliases.begin();
it!=aliases.end();
it++)
@@ -89,7 +89,7 @@ Function: global_may_alias_domaint::get_rhs_aliases_address_of
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -120,7 +120,7 @@ Function: global_may_alias_domaint::transform
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -137,7 +137,7 @@ void global_may_alias_domaint::transform(
case ASSIGN:
{
const code_assignt &code_assign=to_code_assign(instruction.code);
-
+
std::set aliases;
get_rhs_aliases(code_assign.rhs(), aliases);
assign_lhs_aliases(code_assign.lhs(), aliases);
@@ -170,7 +170,7 @@ Function: global_may_alias_domaint::output
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -184,7 +184,7 @@ void global_may_alias_domaint::output(
a_it1++)
{
bool first=true;
-
+
for(aliasest::const_iterator a_it2=aliases.begin();
a_it2!=aliases.end();
a_it2++)
@@ -209,7 +209,7 @@ Function: global_may_alias_domaint::merge
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -225,7 +225,7 @@ bool global_may_alias_domaint::merge(
it!=b.aliases.end(); it++)
{
irep_idt b_root=b.aliases.find(it);
-
+
if(!aliases.same_set(*it, b_root))
{
aliases.make_union(*it, b_root);
@@ -242,6 +242,6 @@ bool global_may_alias_domaint::merge(
aliases.isolate(it);
}
#endif
-
+
return changed;
}
diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h
index 26d5469a2f9..49f6d7f8688 100644
--- a/src/analyses/global_may_alias.h
+++ b/src/analyses/global_may_alias.h
@@ -18,7 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
/*******************************************************************\
Class: global_may_alias_domaint
-
+
Purpose:
\*******************************************************************/
@@ -43,27 +43,27 @@ class global_may_alias_domaint:public ai_domain_baset
const global_may_alias_domaint &b,
locationt from,
locationt to);
-
+
void make_bottom()
{
aliases.clear();
}
-
+
void make_top()
{
aliases.clear();
}
-
+
typedef union_find aliasest;
aliasest aliases;
-
-protected:
+
+protected:
void assign_lhs_aliases(const exprt &, const std::set &);
void get_rhs_aliases(const exprt &, std::set &);
void get_rhs_aliases_address_of(const exprt &, std::set &);
};
-class global_may_alias_analysist:public ait
+class global_may_alias_analysist:public ait
{
protected:
virtual void initialize(const goto_functionst &_goto_functions)
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 40e4fa860cd..8aa43ba9769 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -46,14 +46,14 @@ class goto_checkt
retain_trivial=_options.get_bool_option("retain-trivial");
enable_assert_to_assume=_options.get_bool_option("assert-to-assume");
enable_assertions=_options.get_bool_option("assertions");
- enable_assumptions=_options.get_bool_option("assumptions");
+ enable_assumptions=_options.get_bool_option("assumptions");
error_labels=_options.get_list_option("error-label");
}
typedef goto_functionst::goto_functiont goto_functiont;
void goto_check(goto_functiont &goto_function);
-
+
irep_idt mode;
protected:
@@ -84,20 +84,20 @@ class goto_checkt
const source_locationt &,
const exprt &src_expr,
const guardt &guard);
-
+
goto_programt new_code;
typedef std::set assertionst;
assertionst assertions;
-
+
void invalidate(const exprt &lhs);
-
+
inline static bool has_dereference(const exprt &src)
{
return has_subexpr(src, ID_dereference);
}
bool enable_bounds_check;
- bool enable_pointer_check;
+ bool enable_pointer_check;
bool enable_memory_leak_check;
bool enable_div_by_zero_check;
bool enable_signed_overflow_check;
@@ -138,7 +138,7 @@ void goto_checkt::invalidate(const exprt &lhs)
// clear all assertions about 'symbol'
find_symbols_sett find_symbols_set;
find_symbols_set.insert(to_symbol_expr(lhs).get_identifier());
-
+
for(assertionst::iterator
it=assertions.begin();
it!=assertions.end();
@@ -146,11 +146,11 @@ void goto_checkt::invalidate(const exprt &lhs)
{
assertionst::iterator next=it;
next++;
-
+
if(has_symbol(*it, find_symbols_set) ||
has_dereference(*it))
assertions.erase(it);
-
+
it=next;
}
}
@@ -220,10 +220,10 @@ void goto_checkt::undefined_shift_check(
// Undefined for all types and shifts if distance exceeds width,
// and also undefined for negative distances.
-
+
const typet &distance_type=
ns.follow(expr.distance().type());
-
+
if(distance_type.id()==ID_signedbv)
{
binary_relation_exprt inequality(
@@ -240,15 +240,15 @@ void goto_checkt::undefined_shift_check(
const typet &op_type=
ns.follow(expr.op().type());
-
+
if(op_type.id()==ID_unsignedbv || op_type.id()==ID_signedbv)
- {
+ {
exprt width_expr=
from_integer(to_bitvector_type(op_type).get_width(), distance_type);
if(width_expr.is_nil())
throw "no number for width for operator "+expr.id_string();
-
+
binary_relation_exprt inequality(
expr.distance(), ID_lt, width_expr);
@@ -322,24 +322,24 @@ void goto_checkt::integer_overflow_check(
// First, check type.
const typet &type=ns.follow(expr.type());
-
+
if(type.id()==ID_signedbv && !enable_signed_overflow_check)
return;
if(type.id()==ID_unsignedbv && !enable_unsigned_overflow_check)
return;
-
+
// add overflow subgoal
if(expr.id()==ID_typecast)
{
// conversion to signed int may overflow
-
+
if(expr.operands().size()!=1)
throw "typecast takes one operand";
const typet &old_type=ns.follow(expr.op0().type());
-
+
if(type.id()==ID_signedbv)
{
std::size_t new_width=to_signedbv_type(type).get_width();
@@ -514,7 +514,7 @@ void goto_checkt::integer_overflow_check(
expr,
guard);
}
-
+
return;
}
else if(expr.id()==ID_mod)
@@ -528,7 +528,7 @@ void goto_checkt::integer_overflow_check(
{
// overflow on unary- can only happen with the smallest
// representable number 100....0
-
+
equal_exprt int_min_eq(
expr.op0(), to_signedbv_type(type).smallest_expr());
@@ -540,7 +540,7 @@ void goto_checkt::integer_overflow_check(
expr,
guard);
}
-
+
return;
}
@@ -551,11 +551,11 @@ void goto_checkt::integer_overflow_check(
{
// The overflow checks are binary!
// We break these up.
-
+
for(unsigned i=1; i=3)
{
assert(expr.id()!=ID_minus);
-
+
// break up
exprt tmp=make_binary(expr);
float_overflow_check(tmp, guard);
@@ -751,7 +751,7 @@ void goto_checkt::nan_check(
// first, check type
if(expr.type().id()!=ID_floatbv)
return;
-
+
if(expr.id()!=ID_plus &&
expr.id()!=ID_mult &&
expr.id()!=ID_div &&
@@ -759,9 +759,9 @@ void goto_checkt::nan_check(
return;
// add NaN subgoal
-
+
exprt isnan;
-
+
if(expr.id()==ID_div)
{
assert(expr.operands().size()==2);
@@ -774,7 +774,7 @@ void goto_checkt::nan_check(
ieee_float_equal_exprt(expr.op1(), gen_zero(expr.op1().type())));
exprt div_inf=unary_exprt(ID_isinf, expr.op1(), bool_typet());
-
+
isnan=or_exprt(zero_div_zero, div_inf);
}
else if(expr.id()==ID_mult)
@@ -946,7 +946,7 @@ void goto_checkt::pointer_validity_check(
local_bitvector_analysist::flagst flags=
local_bitvector_analysis->get(t, pointer);
-
+
const typet &dereference_type=pointer_type.subtype();
// For Java, we only need to check for null
@@ -1108,7 +1108,7 @@ void goto_checkt::bounds_check(
+array_type.id_string();
std::string name=array_name(expr.array());
-
+
const exprt &index=expr.index();
object_descriptor_exprt ode;
ode.build(expr, ns);
@@ -1125,7 +1125,7 @@ void goto_checkt::bounds_check(
else
{
mp_integer i;
-
+
if(!to_integer(index, i) && i>=0)
{
// ok
@@ -1275,14 +1275,14 @@ void goto_checkt::add_guarded_claim(
new_expr=exprt(ID_implies, bool_typet());
new_expr.move_to_operands(guard_expr, expr);
}
-
+
if(assertions.insert(new_expr).second)
{
goto_program_instruction_typet type=
enable_assert_to_assume?ASSUME:ASSERT;
-
+
goto_programt::targett t=new_code.add_instruction(type);
-
+
std::string source_expr_string=from_expr(ns, "", src_expr);
t->guard.swap(new_expr);
@@ -1410,7 +1410,7 @@ void goto_checkt::check_rec(
else if(expr.id()==ID_div)
{
div_by_zero_check(to_div_expr(expr), guard);
-
+
if(expr.type().id()==ID_signedbv)
integer_overflow_check(expr, guard);
else if(expr.type().id()==ID_floatbv)
@@ -1497,7 +1497,7 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
}
assertions.clear();
-
+
local_bitvector_analysist local_bitvector_analysis_obj(goto_function);
local_bitvector_analysis=&local_bitvector_analysis_obj;
@@ -1507,7 +1507,7 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
{
t=it;
goto_programt::instructiont &i=*it;
-
+
new_code.clear();
// we clear all recorded assertions if
@@ -1516,7 +1516,7 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
if(retain_trivial ||
i.is_target())
assertions.clear();
-
+
check(i.guard);
// magic ERROR label?
@@ -1539,11 +1539,11 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
t->source_location.set("user-provided", true);
}
}
-
+
if(i.is_other())
{
const irep_idt &statement=i.code.get(ID_statement);
-
+
if(statement==ID_expression)
{
check(i.code);
@@ -1557,10 +1557,10 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
else if(i.is_assign())
{
const code_assignt &code_assign=to_code_assign(i.code);
-
+
check(code_assign.lhs());
check(code_assign.rhs());
-
+
// the LHS might invalidate any assertion
invalidate(code_assign.lhs());
}
@@ -1568,7 +1568,7 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
{
const code_function_callt &code_function_call=
to_code_function_call(i.code);
-
+
// for Java, need to check whether 'this' is null
// on non-static method invocations
if(mode==ID_java &&
@@ -1578,10 +1578,10 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
to_code_type(code_function_call.function().type()).has_this())
{
exprt pointer=code_function_call.arguments()[0];
-
+
local_bitvector_analysist::flagst flags=
local_bitvector_analysis->get(t, pointer);
-
+
if(flags.is_unknown() || flags.is_null())
{
notequal_exprt not_eq_null(pointer, gen_zero(pointer.type()));
@@ -1595,7 +1595,7 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
guardt());
}
}
-
+
forall_operands(it, code_function_call)
check(*it);
@@ -1618,11 +1618,11 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
i.code.op0().operands().size()==1)
{
// must not throw NULL
-
+
exprt pointer=i.code.op0().op0();
if(pointer.type().subtype().get(ID_identifier)!="java::java.lang.AssertionError")
- {
+ {
notequal_exprt not_eq_null(pointer, gen_zero(pointer.type()));
add_guarded_claim(
@@ -1656,7 +1656,7 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
{
assert(i.code.operands().size()==1);
const symbol_exprt &variable=to_symbol_expr(i.code.op0());
-
+
// is it dirty?
if(local_bitvector_analysis->dirty(variable))
{
@@ -1686,7 +1686,7 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
goto_programt::targett t=new_code.add_instruction();
t->make_assignment();
t->code=code_assignt(leak_expr, leak_expr);
-
+
source_locationt source_location;
source_location.set_function(i.function);
@@ -1722,10 +1722,10 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
if(it->source_location.get_column()!=irep_idt())
i_it->source_location.set_column(it->source_location.get_column());
}
-
+
if(i_it->function==irep_idt()) i_it->function=it->function;
}
-
+
// insert new instructions -- make sure targets are not moved
while(!new_code.instructions.empty())
@@ -1756,7 +1756,7 @@ void goto_check(
{
goto_checkt goto_check(ns, options);
goto_check.goto_check(goto_function);
-}
+}
/*******************************************************************\
@@ -1776,7 +1776,7 @@ void goto_check(
goto_functionst &goto_functions)
{
goto_checkt goto_check(ns, options);
-
+
for(goto_functionst::function_mapt::iterator
it=goto_functions.function_map.begin();
it!=goto_functions.function_map.end();
@@ -1784,7 +1784,7 @@ void goto_check(
{
goto_check.goto_check(it->second);
}
-}
+}
/*******************************************************************\
@@ -1804,7 +1804,7 @@ void goto_check(
{
const namespacet ns(goto_model.symbol_table);
goto_checkt goto_check(ns, options);
-
+
for(goto_functionst::function_mapt::iterator
it=goto_model.goto_functions.function_map.begin();
it!=goto_model.goto_functions.function_map.end();
@@ -1812,4 +1812,4 @@ void goto_check(
{
goto_check.goto_check(it->second);
}
-}
+}
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index 0efe8d2ff85..2d84edc27ea 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -1,6 +1,6 @@
/*******************************************************************\
-Module:
+Module:
Author: Daniel Kroening
@@ -1015,7 +1015,7 @@ void goto_rw(goto_programt::const_targett target,
case NO_INSTRUCTION_TYPE:
assert(false);
break;
-
+
case GOTO:
case ASSUME:
case ASSERT:
@@ -1024,7 +1024,7 @@ void goto_rw(goto_programt::const_targett target,
rw_range_sett::READ,
target->guard);
break;
-
+
case RETURN:
{
const code_returnt &code_return=
@@ -1036,7 +1036,7 @@ void goto_rw(goto_programt::const_targett target,
code_return.return_value());
}
break;
-
+
case OTHER:
//if it's printf, mark the operands as read here
if (target->code.get(ID_statement)==ID_printf)
@@ -1045,7 +1045,7 @@ void goto_rw(goto_programt::const_targett target,
rw_set.get_objects_rec(target, rw_range_sett::READ, *it);
}
break;
-
+
case SKIP:
case START_THREAD:
case END_THREAD:
@@ -1056,12 +1056,12 @@ void goto_rw(goto_programt::const_targett target,
case THROW:
case CATCH:
// these don't read or write anything
- break;
+ break;
case ASSIGN:
goto_rw(target, to_code_assign(target->code), rw_set);
break;
-
+
case DEAD:
rw_set.get_objects_rec(
target,
@@ -1077,7 +1077,7 @@ void goto_rw(goto_programt::const_targett target,
rw_range_sett::LHS_W,
to_code_decl(target->code).symbol());
break;
-
+
case FUNCTION_CALL:
goto_rw(target, to_code_function_call(target->code), rw_set);
break;
@@ -1128,4 +1128,3 @@ void goto_rw(const goto_functionst &goto_functions,
goto_rw(body, rw_set);
}
}
-
diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h
index ab324d4e801..54b8bb309f8 100644
--- a/src/analyses/goto_rw.h
+++ b/src/analyses/goto_rw.h
@@ -1,6 +1,6 @@
/*******************************************************************\
-Module:
+Module:
Author: Daniel Kroening
diff --git a/src/analyses/interval_analysis.cpp b/src/analyses/interval_analysis.cpp
index 80183b3516e..f260c10372d 100644
--- a/src/analyses/interval_analysis.cpp
+++ b/src/analyses/interval_analysis.cpp
@@ -34,7 +34,7 @@ void instrument_intervals(
find_symbols(i_it->code, symbols);
find_symbols(i_it->guard, symbols);
}
-
+
Forall_goto_program_instructions(i_it, goto_function.body)
{
if(i_it==goto_function.body.instructions.begin())
@@ -60,7 +60,7 @@ void instrument_intervals(
else
continue; // don't instrument
}
-
+
const interval_domaint &d=interval_analysis[i_it];
exprt::operandst assertion;
@@ -74,7 +74,7 @@ void instrument_intervals(
if(!tmp.is_true())
assertion.push_back(tmp);
}
-
+
if(!assertion.empty())
{
goto_programt::targett t=i_it;
@@ -104,7 +104,7 @@ void interval_analysis(
goto_functionst &goto_functions)
{
ait interval_analysis;
-
+
interval_analysis(goto_functions, ns);
Forall_goto_functions(f_it, goto_functions)
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index 4f8aca54d4b..93a487f6c41 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -90,15 +90,15 @@ void interval_domaint::transform(
case DECL:
havoc_rec(to_code_decl(instruction.code).symbol());
break;
-
+
case DEAD:
havoc_rec(to_code_dead(instruction.code).symbol());
break;
-
+
case ASSIGN:
assign(to_code_assign(instruction.code));
break;
-
+
case GOTO:
{
locationt next=from;
@@ -109,11 +109,11 @@ void interval_domaint::transform(
assume(instruction.guard, ns);
}
break;
-
+
case ASSUME:
assume(instruction.guard, ns);
break;
-
+
case FUNCTION_CALL:
{
const code_function_callt &code_function_call=
@@ -122,7 +122,7 @@ void interval_domaint::transform(
havoc_rec(code_function_call.lhs());
}
break;
-
+
default:;
}
}
@@ -163,7 +163,7 @@ bool interval_domaint::merge(
integer_intervalt previous=it->second;
it->second.join(b_it->second);
if(it->second!=previous) result=true;
-
+
it++;
}
}
@@ -182,7 +182,7 @@ bool interval_domaint::merge(
ieee_float_intervalt previous=it->second;
it->second.join(b_it->second);
if(it->second!=previous) result=true;
-
+
it++;
}
}
@@ -269,27 +269,27 @@ void interval_domaint::assume_rec(
assume_rec(lhs, ID_le, rhs);
return;
}
-
+
if(id==ID_notequal)
return; // won't do split
-
+
if(id==ID_ge)
- return assume_rec(rhs, ID_le, lhs);
-
+ return assume_rec(rhs, ID_le, lhs);
+
if(id==ID_gt)
- return assume_rec(rhs, ID_lt, lhs);
+ return assume_rec(rhs, ID_lt, lhs);
// we now have lhs < rhs or
// lhs <= rhs
assert(id==ID_lt || id==ID_le);
- #ifdef DEBUG
- std::cout << "assume_rec: "
+ #ifdef DEBUG
+ std::cout << "assume_rec: "
<< from_expr(lhs) << " " << id << " "
<< from_expr(rhs) << "\n";
#endif
-
+
if(lhs.id()==ID_symbol && rhs.id()==ID_constant)
{
irep_idt lhs_identifier=to_symbol_expr(lhs).get_identifier();
@@ -315,7 +315,7 @@ void interval_domaint::assume_rec(
else if(lhs.id()==ID_constant && rhs.id()==ID_symbol)
{
irep_idt rhs_identifier=to_symbol_expr(rhs).get_identifier();
-
+
if(is_int(lhs.type()) && is_int(rhs.type()))
{
mp_integer tmp;
@@ -338,7 +338,7 @@ void interval_domaint::assume_rec(
{
irep_idt lhs_identifier=to_symbol_expr(lhs).get_identifier();
irep_idt rhs_identifier=to_symbol_expr(rhs).get_identifier();
-
+
if(is_int(lhs.type()) && is_int(rhs.type()))
{
integer_intervalt &lhs_i=int_map[lhs_identifier];
@@ -459,18 +459,18 @@ exprt interval_domaint::make_expression(const symbol_exprt &src) const
exprt::operandst conjuncts;
- if(interval.upper_set)
+ if(interval.upper_set)
{
exprt tmp=from_integer(interval.upper, src.type());
conjuncts.push_back(binary_relation_exprt(src, ID_le, tmp));
}
- if(interval.lower_set)
+ if(interval.lower_set)
{
exprt tmp=from_integer(interval.lower, src.type());
conjuncts.push_back(binary_relation_exprt(tmp, ID_le, src));
}
-
+
return conjunction(conjuncts);
}
else if(is_float(src.type()))
@@ -483,18 +483,18 @@ exprt interval_domaint::make_expression(const symbol_exprt &src) const
exprt::operandst conjuncts;
- if(interval.upper_set)
+ if(interval.upper_set)
{
exprt tmp=interval.upper.to_expr();
conjuncts.push_back(binary_relation_exprt(src, ID_le, tmp));
}
- if(interval.lower_set)
+ if(interval.lower_set)
{
exprt tmp=interval.lower.to_expr();
conjuncts.push_back(binary_relation_exprt(tmp, ID_le, src));
}
-
+
return conjunction(conjuncts);
}
else
diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h
index 0c3d9aa68c9..b8cc21fa0d9 100644
--- a/src/analyses/interval_domain.h
+++ b/src/analyses/interval_domain.h
@@ -24,13 +24,13 @@ class interval_domaint:public ai_domain_baset
// Trivial, conjunctive interval domain for both float
// and integers. The categorization 'float' and 'integers'
// is done by is_int and is_float.
-
+
virtual void transform(
locationt from,
locationt to,
ai_baset &ai,
const namespacet &ns);
-
+
virtual void output(
std::ostream &out,
const ai_baset &ai,
@@ -40,7 +40,7 @@ class interval_domaint:public ai_domain_baset
const interval_domaint &b,
locationt from,
locationt to);
-
+
// no states
virtual void make_bottom()
{
@@ -48,7 +48,7 @@ class interval_domaint:public ai_domain_baset
float_map.clear();
bottom=true;
}
-
+
// all states
virtual void make_top()
{
@@ -58,14 +58,14 @@ class interval_domaint:public ai_domain_baset
}
exprt make_expression(const symbol_exprt &) const;
-
+
void assume(const exprt &, const namespacet &);
inline static bool is_int(const typet &src)
{
return src.id()==ID_signedbv || src.id()==ID_unsignedbv;
}
-
+
inline static bool is_float(const typet &src)
{
return src.id()==ID_floatbv;
diff --git a/src/analyses/invariant_propagation.cpp b/src/analyses/invariant_propagation.cpp
index 3c244ed0bc4..56e285247e0 100644
--- a/src/analyses/invariant_propagation.cpp
+++ b/src/analyses/invariant_propagation.cpp
@@ -72,12 +72,12 @@ void invariant_propagationt::add_objects(
// get the globals
object_listt globals;
get_globals(globals);
-
+
// get the locals
goto_programt::decl_identifierst locals;
goto_program.get_decl_identifiers(locals);
- // cache the list for the locals to speed things up
+ // cache the list for the locals to speed things up
typedef hash_map_cont object_cachet;
object_cachet object_cache;
@@ -88,7 +88,7 @@ void invariant_propagationt::add_objects(
{
#if 0
invariant_sett &is=(*this)[i_it].invariant_set;
-
+
is.add_objects(globals);
#endif
@@ -103,7 +103,7 @@ void invariant_propagationt::add_objects(
if(e_it==object_cache.end())
{
const symbolt &symbol=ns.lookup(*l_it);
-
+
object_listt &objects=object_cache[*l_it];
get_objects(symbol, objects);
#if 0
@@ -116,7 +116,7 @@ void invariant_propagationt::add_objects(
#endif
}
}
-}
+}
/*******************************************************************\
@@ -137,7 +137,7 @@ void invariant_propagationt::get_objects(
std::list object_list;
get_objects_rec(symbol.symbol_expr(), object_list);
-
+
for(std::list::const_iterator
it=object_list.begin();
it!=object_list.end();
@@ -167,12 +167,12 @@ void invariant_propagationt::get_objects_rec(
t.id()==ID_union)
{
const struct_typet &struct_type=to_struct_type(t);
-
+
const struct_typet::componentst &c=struct_type.components();
-
+
exprt member_expr(ID_member);
member_expr.copy_to_operands(src);
-
+
for(struct_typet::componentst::const_iterator
it=c.begin();
it!=c.end();
@@ -213,7 +213,7 @@ void invariant_propagationt::add_objects(
// get the globals
object_listt globals;
get_globals(globals);
-
+
for(goto_functionst::function_mapt::const_iterator
f_it=goto_functions.function_map.begin();
f_it!=goto_functions.function_map.end();
@@ -222,10 +222,10 @@ void invariant_propagationt::add_objects(
// get the locals
std::set locals;
get_local_identifiers(f_it->second, locals);
-
+
const goto_programt &goto_program=f_it->second.body;
- // cache the list for the locals to speed things up
+ // cache the list for the locals to speed things up
typedef hash_map_cont object_cachet;
object_cachet object_cache;
@@ -236,7 +236,7 @@ void invariant_propagationt::add_objects(
{
#if 0
invariant_sett &is=(*this)[i_it].invariant_set;
-
+
is.add_objects(globals);
#endif
@@ -251,7 +251,7 @@ void invariant_propagationt::add_objects(
if(e_it==object_cache.end())
{
const symbolt &symbol=ns.lookup(*l_it);
-
+
object_listt &objects=object_cache[*l_it];
get_objects(symbol, objects);
#if 0
@@ -265,7 +265,7 @@ void invariant_propagationt::add_objects(
}
}
}
-}
+}
/*******************************************************************\
@@ -287,7 +287,7 @@ void invariant_propagationt::get_globals(
if(it->second.is_lvalue &&
it->second.is_static_lifetime)
get_objects(it->second, dest);
-}
+}
/*******************************************************************\
@@ -317,9 +317,9 @@ bool invariant_propagationt::check_type(const typet &type) const
return true;
else if(type.id()==ID_bool)
return true;
-
+
return false;
-}
+}
/*******************************************************************\
@@ -340,12 +340,12 @@ void invariant_propagationt::initialize(const goto_programt &goto_program)
forall_goto_program_instructions(it, goto_program)
{
invariant_sett &s=state_map[it].invariant_set;
-
+
if(it==goto_program.instructions.begin())
s.make_true();
else
s.make_false();
-
+
s.set_value_sets(value_sets);
s.set_object_store(object_store);
s.set_namespace(ns);
@@ -372,7 +372,7 @@ void invariant_propagationt::initialize(const goto_functionst &goto_functions)
for(goto_functionst::function_mapt::const_iterator f_it=
goto_functions.function_map.begin();
- f_it!=goto_functions.function_map.end();
+ f_it!=goto_functions.function_map.end();
f_it++)
initialize(f_it->second.body);
}
@@ -417,14 +417,14 @@ void invariant_propagationt::simplify(goto_programt &goto_program)
state_mapt::const_iterator s_it=state_map.find(i_it);
if(s_it==state_map.end()) continue;
-
+
const invariant_sett &invariant_set=s_it->second.invariant_set;
-
+
exprt simplified_guard(i_it->guard);
-
+
invariant_set.simplify(simplified_guard);
::simplify(simplified_guard, ns);
-
+
if(invariant_set.implies(simplified_guard).is_true())
i_it->guard=true_exprt();
}
diff --git a/src/analyses/invariant_propagation.h b/src/analyses/invariant_propagation.h
index 0e89339ee12..5df6f6925d7 100644
--- a/src/analyses/invariant_propagation.h
+++ b/src/analyses/invariant_propagation.h
@@ -27,7 +27,7 @@ class invariant_propagationt:public
object_store(_ns)
{
}
-
+
const invariant_sett &lookup(locationt l) const
{
return (*this)[l].invariant_set;
@@ -38,16 +38,16 @@ class invariant_propagationt:public
void make_all_true();
void make_all_false();
-
+
void simplify(goto_programt &goto_program);
void simplify(goto_functionst &goto_functions);
-
+
typedef ait baset;
-
+
protected:
const namespacet &ns;
value_setst &value_sets;
-
+
inv_object_storet object_store;
typedef std::list object_listt;
@@ -62,9 +62,9 @@ class invariant_propagationt:public
void get_objects_rec(
const exprt &src,
std::list &dest);
-
+
void get_globals(object_listt &globals);
-
+
bool check_type(const typet &type) const;
};
diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp
index 5ad5404a863..c5cfac661a5 100644
--- a/src/analyses/invariant_set.cpp
+++ b/src/analyses/invariant_set.cpp
@@ -56,25 +56,25 @@ bool inv_object_storet::get(const exprt &expr, unsigned &n)
{
std::string s=build_string(expr);
if(s=="") return true;
-
+
// if it's a constant, we add it in any case
if(is_constant(expr))
{
n=map.number(s);
-
+
if(n>=entries.size())
{
entries.resize(n+1);
entries[n].expr=expr;
entries[n].is_constant=true;
}
-
+
return false;
}
return map.get_number(s, n);
}
-
+
/*******************************************************************\
Function: inv_object_storet::add
@@ -90,21 +90,21 @@ Function: inv_object_storet::add
unsigned inv_object_storet::add(const exprt &expr)
{
std::string s=build_string(expr);
-
+
assert(s!="");
unsigned n=map.number(s);
-
+
if(n>=entries.size())
{
entries.resize(n+1);
entries[n].expr=expr;
entries[n].is_constant=is_constant(expr);
}
-
+
return n;
}
-
+
/*******************************************************************\
Function: inv_object_storet::is_constant
@@ -121,7 +121,7 @@ bool inv_object_storet::is_constant(unsigned n) const
{
assert(n &p)
// check if there is a contradiction with two constants
unsigned r=eq_set.find(p.first);
-
+
bool constant_seen=false;
mp_integer c;
-
+
for(unsigned i=0; iis_constant(i))
@@ -343,12 +343,12 @@ void invariant_sett::add_eq(const std::pair &p)
make_false();
return;
}
- else
+ else
constant_seen=true;
}
// replicate <= and != constraints
-
+
for(ineq_sett::const_iterator it=le_set.begin();
it!=le_set.end();
it++)
@@ -384,24 +384,24 @@ void invariant_sett::add_eq(
if(eq.first==ineq.first)
{
n=ineq;
- n.first=eq.second;
+ n.first=eq.second;
dest.insert(n);
}
-
+
if(eq.first==ineq.second)
{
n=ineq;
n.second=eq.second;
dest.insert(n);
}
-
+
if(eq.second==ineq.first)
{
n=ineq;
- n.first=eq.first;
+ n.first=eq.first;
dest.insert(n);
}
-
+
if(eq.second==ineq.second)
{
n=ineq;
@@ -426,16 +426,16 @@ tvt invariant_sett::is_eq(std::pair p) const
{
std::pair s=p;
std::swap(s.first, s.second);
-
+
if(has_eq(p))
return tvt(true);
-
+
if(has_ne(p) || has_ne(s))
return tvt(false);
return tvt::unknown();
}
-
+
/*******************************************************************\
Function: invariant_sett::is_le
@@ -452,17 +452,17 @@ tvt invariant_sett::is_le(std::pair p) const
{
std::pair s=p;
std::swap(s.first, s.second);
-
+
if(has_eq(p))
return tvt(true);
-
+
if(has_le(p))
return tvt(true);
-
+
if(has_le(s))
if(has_ne(s) || has_ne(p))
return tvt(false);
-
+
return tvt::unknown();
}
@@ -505,7 +505,7 @@ void invariant_sett::output(
out << to_string(j, identifier);
}
-
+
out << std::endl;
}
@@ -561,7 +561,7 @@ void invariant_sett::add_type_bounds(const exprt &expr, const typet &type)
{
unsigned a;
if(get_object(expr, a)) return;
-
+
add_bounds(a, boundst(0, power(2, op_width)-1));
}
}
@@ -606,13 +606,13 @@ void invariant_sett::strengthen_rec(const exprt &expr)
#if 0
std::cout << "S: " << from_expr(*ns, "", expr) << std::endl;
#endif
-
+
if(is_false)
{
// we can't get any stronger
return;
}
-
+
if(expr.is_true())
{
// do nothing, it's useless
@@ -635,26 +635,26 @@ void invariant_sett::strengthen_rec(const exprt &expr)
expr.id()==ID_lt)
{
assert(expr.operands().size()==2);
-
+
// special rule: x <= (a & b)
// implies: x<=a && x<=b
if(expr.op1().id()==ID_bitand)
{
const exprt &bitand_op=expr.op1();
-
+
forall_operands(it, bitand_op)
{
exprt tmp(expr);
tmp.op1()=*it;
strengthen_rec(tmp);
}
-
+
return;
}
std::pair p;
-
+
if(get_object(expr.op0(), p.first) ||
get_object(expr.op1(), p.second))
return;
@@ -662,7 +662,7 @@ void invariant_sett::strengthen_rec(const exprt &expr)
mp_integer i0, i1;
bool have_i0=!to_integer(expr.op0(), i0);
bool have_i1=!to_integer(expr.op1(), i1);
-
+
if(expr.id()==ID_le)
{
if(have_i0)
@@ -690,20 +690,20 @@ void invariant_sett::strengthen_rec(const exprt &expr)
else if(expr.id()==ID_equal)
{
assert(expr.operands().size()==2);
-
+
const typet &op_type=ns->follow(expr.op0().type());
-
+
if(op_type.id()==ID_struct)
{
const struct_typet &struct_type=to_struct_type(op_type);
-
+
const struct_typet::componentst &c=struct_type.components();
-
+
exprt lhs_member_expr(ID_member);
exprt rhs_member_expr(ID_member);
lhs_member_expr.copy_to_operands(expr.op0());
rhs_member_expr.copy_to_operands(expr.op1());
-
+
for(struct_typet::componentst::const_iterator
it=c.begin();
it!=c.end();
@@ -719,21 +719,21 @@ void invariant_sett::strengthen_rec(const exprt &expr)
equal_exprt equality;
equality.lhs()=lhs_member_expr;
equality.rhs()=rhs_member_expr;
-
+
// recursive call
strengthen_rec(equality);
}
-
+
return;
}
-
+
// special rule: x = (a & b)
// implies: x<=a && x<=b
if(expr.op1().id()==ID_bitand)
{
const exprt &bitand_op=expr.op1();
-
+
forall_operands(it, bitand_op)
{
exprt tmp(expr);
@@ -741,7 +741,7 @@ void invariant_sett::strengthen_rec(const exprt &expr)
tmp.id(ID_le);
strengthen_rec(tmp);
}
-
+
return;
}
else if(expr.op0().id()==ID_bitand)
@@ -751,7 +751,7 @@ void invariant_sett::strengthen_rec(const exprt &expr)
strengthen_rec(tmp);
return;
}
-
+
// special rule: x = (type) y
if(expr.op1().id()==ID_typecast)
{
@@ -763,9 +763,9 @@ void invariant_sett::strengthen_rec(const exprt &expr)
assert(expr.op0().operands().size()==1);
add_type_bounds(expr.op1(), expr.op0().op0().type());
}
-
+
std::pair p, s;
-
+
if(get_object(expr.op0(), p.first) ||
get_object(expr.op1(), p.second))
return;
@@ -789,13 +789,13 @@ void invariant_sett::strengthen_rec(const exprt &expr)
else if(expr.id()==ID_notequal)
{
assert(expr.operands().size()==2);
-
+
std::pair p;
-
+
if(get_object(expr.op0(), p.first) ||
get_object(expr.op1(), p.second))
return;
-
+
// check if this is a contradiction
if(has_eq(p))
make_false();
@@ -822,7 +822,7 @@ tvt invariant_sett::implies(const exprt &expr) const
nnf(tmp);
return implies_rec(tmp);
}
-
+
/*******************************************************************\
Function: invariant_sett::implies
@@ -839,11 +839,11 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
{
if(expr.type().id()!=ID_bool)
throw "implies: non-Boolean expression";
-
+
#if 0
std::cout << "I: " << from_expr(*ns, "", expr) << std::endl;
#endif
-
+
if(is_false) // can't get any stronger
return tvt(true);
@@ -858,7 +858,7 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
forall_operands(it, expr)
if(implies_rec(*it)!=tvt(true))
return tvt::unknown();
-
+
return tvt(true);
}
else if(expr.id()==ID_or)
@@ -875,23 +875,23 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
assert(expr.operands().size()==2);
std::pair p;
-
+
bool ob0=get_object(expr.op0(), p.first);
bool ob1=get_object(expr.op1(), p.second);
-
+
if(ob0 || ob1) return tvt::unknown();
-
+
tvt r;
-
+
if(expr.id()==ID_le)
{
r=is_le(p);
if(!r.is_unknown()) return r;
-
+
boundst b0, b1;
get_bounds(p.first, b0);
get_bounds(p.second, b1);
-
+
return b0<=b1;
}
else if(expr.id()==ID_lt)
@@ -902,7 +902,7 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
boundst b0, b1;
get_bounds(p.first, b0);
get_bounds(p.second, b1);
-
+
return b0second;
}
@@ -987,14 +987,14 @@ void invariant_sett::nnf(exprt &expr, bool negate)
else if(expr.id()==ID_and)
{
if(negate) expr.id(ID_or);
-
+
Forall_operands(it, expr)
nnf(*it, negate);
}
else if(expr.id()==ID_or)
{
if(negate) expr.id(ID_and);
-
+
Forall_operands(it, expr)
nnf(*it, negate);
}
@@ -1116,10 +1116,10 @@ exprt invariant_sett::get_constant(const exprt &expr) const
unsigned a;
if(!get_object(expr, a))
- {
+ {
// bounds?
bounds_mapt::const_iterator it=bounds_map.find(a);
-
+
if(it!=bounds_map.end())
{
if(it->second.singleton())
@@ -1133,12 +1133,12 @@ exprt invariant_sett::get_constant(const exprt &expr) const
if(eq_set.find(i)==r)
{
const exprt &e=object_store->get_expr(i);
-
+
if(e.is_constant())
{
mp_integer value;
assert(!to_integer(e, value));
-
+
if(expr.type().id()==ID_pointer)
{
if(value==0)
@@ -1155,14 +1155,14 @@ exprt invariant_sett::get_constant(const exprt &expr) const
{
if(e.type()==expr.type())
return e;
-
+
exprt tmp(ID_typecast, expr.type());
tmp.copy_to_operands(e);
return tmp;
}
}
}
-
+
return static_cast(get_nil_irep());
}
@@ -1226,13 +1226,13 @@ bool invariant_sett::make_union(const invariant_sett &other)
make_threaded();
return true; // change
}
-
+
if(threaded)
return false; // no change
if(other.is_false)
return false; // no change
-
+
if(is_false)
{
// copy
@@ -1241,22 +1241,22 @@ bool invariant_sett::make_union(const invariant_sett &other)
le_set=other.le_set;
ne_set=other.ne_set;
bounds_map=other.bounds_map;
-
+
return true; // change
}
-
+
// equalities first
unsigned old_eq_roots=eq_set.count_roots();
-
+
eq_set.intersection(other.eq_set);
// inequalities
unsigned old_ne_set=ne_set.size();
unsigned old_le_set=le_set.size();
-
+
intersection(ne_set, other.ne_set);
intersection(le_set, other.le_set);
-
+
// bounds
if(make_union_bounds_map(other.bounds_map))
return true;
@@ -1264,7 +1264,7 @@ bool invariant_sett::make_union(const invariant_sett &other)
if(old_eq_roots!=eq_set.count_roots()) return true;
if(old_ne_set!=ne_set.size()) return true;
if(old_le_set!=le_set.size()) return true;
-
+
return false; // no change
}
@@ -1283,7 +1283,7 @@ Function: invariant_sett::make_union_bounds_map
bool invariant_sett::make_union_bounds_map(const bounds_mapt &other)
{
bool changed=false;
-
+
for(bounds_mapt::iterator
it=bounds_map.begin();
it!=bounds_map.end();
@@ -1307,7 +1307,7 @@ bool invariant_sett::make_union_bounds_map(const bounds_mapt &other)
it++;
}
}
-
+
return changed;
}
@@ -1421,14 +1421,14 @@ void invariant_sett::assignment(
equal_exprt equality;
equality.lhs()=lhs;
equality.rhs()=rhs;
-
+
// first evaluate RHS
simplify(equality.rhs());
::simplify(equality.rhs(), *ns);
-
+
// now kill LHS
modifies(lhs);
-
+
// and put it back
strengthen(equality);
}
@@ -1491,7 +1491,7 @@ void invariant_sett::apply_code(const codet &code)
{
// does nothing
}
- else if(statement=="lock" ||
+ else if(statement=="lock" ||
statement=="unlock" ||
statement==ID_asm)
{
diff --git a/src/analyses/invariant_set.h b/src/analyses/invariant_set.h
index b15c70c856b..3420b67c21f 100644
--- a/src/analyses/invariant_set.h
+++ b/src/analyses/invariant_set.h
@@ -26,14 +26,14 @@ class inv_object_storet
}
bool get(const exprt &expr, unsigned &n);
-
+
unsigned add(const exprt &expr);
-
+
bool is_constant(unsigned n) const;
bool is_constant(const exprt &expr) const;
static bool is_constant_address(const exprt &expr);
-
+
const irep_idt &operator[](unsigned n) const
{
return map[n];
@@ -44,9 +44,9 @@ class inv_object_storet
assert(n mapt;
mapt map;
-
+
struct entryt
{
bool is_constant;
exprt expr;
};
-
+
std::vector entries;
-
+
std::string build_string(const exprt &expr) const;
static bool is_constant_address_rec(const exprt &expr);
@@ -75,22 +75,22 @@ class invariant_sett
public:
// equalities ==
unsigned_union_find eq_set;
-
+
// <=
typedef std::set > ineq_sett;
ineq_sett le_set;
-
+
// !=
ineq_sett ne_set;
-
+
// bounds
typedef interval_template boundst;
typedef std::map bounds_mapt;
bounds_mapt bounds_map;
-
+
bool threaded;
bool is_false;
-
+
invariant_sett():
threaded(false),
is_false(false),
@@ -99,16 +99,16 @@ class invariant_sett
ns(NULL)
{
}
-
+
void output(
const irep_idt &identifier,
std::ostream &out) const;
// true = added s.th.
bool make_union(const invariant_sett &other_invariants);
-
+
void strengthen(const exprt &expr);
-
+
void make_true()
{
eq_set.clear();
@@ -140,7 +140,7 @@ class invariant_sett
void assignment(
const exprt &lhs,
const exprt &rhs);
-
+
void set_value_sets(value_setst &_value_sets)
{
value_sets=&_value_sets;
@@ -150,16 +150,16 @@ class invariant_sett
{
object_store=&_object_store;
}
-
+
void set_namespace(const namespacet &_ns)
{
ns=&_ns;
}
-
+
static void intersection(ineq_sett &dest, const ineq_sett &other)
{
ineq_sett::iterator it_d=dest.begin();
-
+
while(it_d!=dest.end())
{
ineq_sett::iterator next_d(it_d);
@@ -167,11 +167,11 @@ class invariant_sett
if(other.find(*it_d)==other.end())
dest.erase(it_d);
-
+
it_d=next_d;
- }
+ }
}
-
+
static void remove(ineq_sett &dest, unsigned a)
{
for(ineq_sett::iterator it=dest.begin();
@@ -187,34 +187,34 @@ class invariant_sett
it=next;
}
}
-
+
tvt implies(const exprt &expr) const;
-
+
void simplify(exprt &expr) const;
-
+
protected:
value_setst *value_sets;
inv_object_storet *object_store;
const namespacet *ns;
-
+
tvt implies_rec(const exprt &expr) const;
static void nnf(exprt &expr, bool negate=false);
void strengthen_rec(const exprt &expr);
-
+
void add_type_bounds(const exprt &expr, const typet &type);
void add_bounds(unsigned a, const boundst &bound)
{
bounds_map[a].intersect_with(bound);
}
-
+
void get_bounds(unsigned a, boundst &dest) const;
// true = added s.th.
bool make_union_bounds_map(const bounds_mapt &other);
void modifies(unsigned a);
-
+
std::string to_string(
unsigned a,
const irep_idt &identifier) const;
@@ -222,7 +222,7 @@ class invariant_sett
bool get_object(
const exprt &expr,
unsigned &n) const;
-
+
exprt get_constant(const exprt &expr) const;
// queries
@@ -230,31 +230,31 @@ class invariant_sett
{
return eq_set.same_set(p.first, p.second);
}
-
+
bool has_le(const std::pair &p) const
{
return le_set.find(p)!=le_set.end();
}
-
+
bool has_ne(const std::pair &p) const
{
return ne_set.find(p)!=ne_set.end();
}
-
+
tvt is_eq(std::pair p) const;
tvt is_le(std::pair p) const;
-
+
tvt is_lt(std::pair p) const
{
return is_le(p) && !is_eq(p);
}
-
+
tvt is_ge(std::pair p) const
{
std::swap(p.first, p.second);
return is_eq(p) || is_lt(p);
}
-
+
tvt is_gt(std::pair p) const
{
return !is_le(p);
@@ -271,7 +271,7 @@ class invariant_sett
{
add(p, le_set);
}
-
+
void add_ne(const std::pair &p)
{
add(p, ne_set);
diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp
index 0302c336e36..6ee0be8e6e0 100644
--- a/src/analyses/invariant_set_domain.cpp
+++ b/src/analyses/invariant_set_domain.cpp
@@ -42,7 +42,7 @@ void invariant_set_domaint::transform(
invariant_set.strengthen(tmp);
}
break;
-
+
case ASSERT:
case ASSUME:
{
@@ -51,7 +51,7 @@ void invariant_set_domaint::transform(
invariant_set.strengthen(tmp);
}
break;
-
+
case RETURN:
// ignore
break;
@@ -62,24 +62,24 @@ void invariant_set_domaint::transform(
invariant_set.assignment(assignment.lhs(), assignment.rhs());
}
break;
-
+
case OTHER:
if(from_l->code.is_not_nil())
invariant_set.apply_code(from_l->code);
break;
-
+
case DECL:
invariant_set.apply_code(from_l->code);
break;
-
+
case FUNCTION_CALL:
invariant_set.apply_code(from_l->code);
break;
-
+
case START_THREAD:
- invariant_set.make_threaded();
+ invariant_set.make_threaded();
break;
-
+
default:;
// do nothing
}
diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h
index 5ab7f8015f8..528e5b404e2 100644
--- a/src/analyses/invariant_set_domain.h
+++ b/src/analyses/invariant_set_domain.h
@@ -17,7 +17,7 @@ class invariant_set_domaint:public ai_domain_baset
public:
invariant_sett invariant_set;
- // overloading
+ // overloading
inline bool merge(
const invariant_set_domaint &other,
@@ -34,7 +34,7 @@ class invariant_set_domaint:public ai_domain_baset
{
invariant_set.output("", out);
}
-
+
virtual void initialize(
const namespacet &ns,
locationt l)
diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp
index 310b3e4ac06..ba3121717cb 100644
--- a/src/analyses/is_threaded.cpp
+++ b/src/analyses/is_threaded.cpp
@@ -16,7 +16,7 @@ class is_threaded_domaint:public ai_domain_baset
bool has_spawn;
public:
bool is_threaded;
-
+
inline is_threaded_domaint():has_spawn(false), is_threaded(false)
{
}
@@ -40,7 +40,7 @@ class is_threaded_domaint:public ai_domain_baset
return old_i_t!=is_threaded || old_h_s!=has_spawn;
}
-
+
void transform(
locationt from,
locationt to,
@@ -75,9 +75,9 @@ void is_threadedt::compute(const goto_functionst &goto_functions)
const namespacet ns(symbol_table);
ait is_threaded_analysis;
-
+
is_threaded_analysis(goto_functions, ns);
-
+
for(goto_functionst::function_mapt::const_iterator
f_it=goto_functions.function_map.begin();
f_it!=goto_functions.function_map.end();
@@ -92,4 +92,3 @@ void is_threadedt::compute(const goto_functionst &goto_functions)
is_threaded_set.insert(i_it);
}
}
-
diff --git a/src/analyses/is_threaded.h b/src/analyses/is_threaded.h
index 88a785a71b9..7b68e62c6f3 100644
--- a/src/analyses/is_threaded.h
+++ b/src/analyses/is_threaded.h
@@ -28,7 +28,7 @@ class is_threadedt
{
return is_threaded_set.find(t)!=is_threaded_set.end();
}
-
+
protected:
typedef std::set is_threaded_sett;
is_threaded_sett is_threaded_set;
diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
index d2ccb7e785e..9e01e9cb283 100644
--- a/src/analyses/local_bitvector_analysis.cpp
+++ b/src/analyses/local_bitvector_analysis.cpp
@@ -26,7 +26,7 @@ Function: local_bitvector_analysist::flagst::print
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -50,14 +50,14 @@ Function: local_bitvector_analysist::loc_infot::merge
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
bool local_bitvector_analysist::loc_infot::merge(const loc_infot &src)
{
bool result=false;
-
+
std::size_t max_index=
std::max(src.points_to.size(), points_to.size());
@@ -66,7 +66,7 @@ bool local_bitvector_analysist::loc_infot::merge(const loc_infot &src)
if(points_to[i].merge(src.points_to[i]))
result=true;
}
-
+
return result;
}
@@ -100,7 +100,7 @@ Function: local_bitvector_analysist::assign_lhs
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -142,7 +142,7 @@ void local_bitvector_analysist::assign_lhs(
assign_lhs(to_if_expr(lhs).false_case(), rhs, loc_info_src, loc_info_dest);
}
}
-
+
/*******************************************************************\
Function: local_bitvector_analysist::get
@@ -151,7 +151,7 @@ Function: local_bitvector_analysist::get
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -160,9 +160,9 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get(
const exprt &rhs)
{
local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t);
-
+
assert(loc_it!=cfg.loc_map.end());
-
+
const loc_infot &loc_info_src=loc_infos[loc_it->second];
return get_rec(rhs, loc_info_src);
@@ -176,7 +176,7 @@ Function: local_bitvector_analysist::get_rec
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -205,7 +205,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
else if(rhs.id()==ID_address_of)
{
const exprt &object=to_address_of_expr(rhs).object();
-
+
if(object.id()==ID_symbol)
{
if(locals.is_local(to_symbol_expr(object).get_identifier()))
@@ -298,7 +298,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
else
return flagst::mk_unknown();
}
-
+
/*******************************************************************\
Function: local_bitvector_analysist::build
@@ -307,7 +307,7 @@ Function: local_bitvector_analysist::build
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -316,10 +316,10 @@ void local_bitvector_analysist::build(const goto_functiont &goto_function)
if(cfg.nodes.empty()) return;
work_queuet work_queue;
- work_queue.push(0);
-
+ work_queue.push(0);
+
loc_infos.resize(cfg.nodes.size());
-
+
// Gather the objects we track, and
// feed in sufficiently bad defaults for their value
// in the entry location.
@@ -336,10 +336,10 @@ void local_bitvector_analysist::build(const goto_functiont &goto_function)
const local_cfgt::nodet &node=cfg.nodes[loc_nr];
const goto_programt::instructiont &instruction=*node.t;
work_queue.pop();
-
+
const loc_infot &loc_info_src=loc_infos[loc_nr];
loc_infot loc_info_dest=loc_infos[loc_nr];
-
+
switch(instruction.type)
{
case ASSIGN:
@@ -393,7 +393,7 @@ Function: local_bitvector_analysist::output
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -424,8 +424,7 @@ void local_bitvector_analysist::output(
out << "\n";
goto_function.body.output_instruction(ns, "", out, i_it);
out << "\n";
-
+
l++;
}
}
-
diff --git a/src/analyses/local_bitvector_analysis.h b/src/analyses/local_bitvector_analysis.h
index e36b7470cac..788f7d34c14 100644
--- a/src/analyses/local_bitvector_analysis.h
+++ b/src/analyses/local_bitvector_analysis.h
@@ -20,7 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
/*******************************************************************\
Class: local_bitvector_analysist
-
+
Purpose:
\*******************************************************************/
@@ -29,7 +29,7 @@ class local_bitvector_analysist
{
public:
typedef goto_functionst::goto_functiont goto_functiont;
-
+
explicit local_bitvector_analysist(
const goto_functiont &_goto_function):
dirty(_goto_function),
@@ -43,7 +43,7 @@ class local_bitvector_analysist
std::ostream &out,
const goto_functiont &goto_function,
const namespacet &ns) const;
-
+
dirtyt dirty;
localst locals;
local_cfgt cfg;
@@ -54,7 +54,7 @@ class local_bitvector_analysist
inline flagst():bits(0)
{
}
-
+
void clear()
{
bits=0;
@@ -76,16 +76,16 @@ class local_bitvector_analysist
explicit inline flagst(const bitst _bits):bits(_bits)
{
}
-
+
unsigned bits;
-
+
inline bool merge(const flagst &other)
{
unsigned old=bits;
bits|=other.bits; // bit-wise or
return old!=bits;
}
-
+
inline static flagst mk_unknown()
{
return flagst(B_unknown);
@@ -174,7 +174,7 @@ class local_bitvector_analysist
f.print(out);
return out;
}
-
+
inline friend flagst operator|(const flagst f1, const flagst f2)
{
flagst result=f1;
@@ -185,40 +185,40 @@ class local_bitvector_analysist
flagst get(
const goto_programt::const_targett t,
const exprt &src);
-
+
protected:
void build(const goto_functiont &goto_function);
typedef std::stack work_queuet;
numbering pointers;
-
+
// pointers -> flagst
// This is a vector, so it's fast.
typedef expanding_vector points_tot;
- // the information tracked per program location
+ // the information tracked per program location
class loc_infot
{
public:
points_tot points_to;
-
+
bool merge(const loc_infot &src);
};
typedef std::vector loc_infost;
loc_infost loc_infos;
-
+
void assign_lhs(
const exprt &lhs,
const exprt &rhs,
const loc_infot &loc_info_src,
loc_infot &loc_info_dest);
-
+
flagst get_rec(
const exprt &rhs,
const loc_infot &loc_info_src);
-
+
bool is_tracked(const irep_idt &identifier);
};
diff --git a/src/analyses/local_cfg.cpp b/src/analyses/local_cfg.cpp
index 7ed586278be..0f70def622b 100644
--- a/src/analyses/local_cfg.cpp
+++ b/src/analyses/local_cfg.cpp
@@ -29,7 +29,7 @@ Function: local_cfgt::build
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -37,9 +37,9 @@ void local_cfgt::build(const goto_programt &goto_program)
{
nodes.resize(goto_program.instructions.size());
- {
+ {
node_nrt loc_nr=0;
-
+
for(goto_programt::const_targett it=goto_program.instructions.begin();
it!=goto_program.instructions.end();
it++, loc_nr++)
@@ -53,36 +53,36 @@ void local_cfgt::build(const goto_programt &goto_program)
{
nodet &node=nodes[loc_nr];
const goto_programt::instructiont &instruction=*node.t;
-
+
switch(instruction.type)
{
case GOTO:
if(!instruction.guard.is_true())
node.successors.push_back(loc_nr+1);
-
+
for(goto_programt::targetst::const_iterator
t_it=instruction.targets.begin();
t_it!=instruction.targets.end();
t_it++)
{
node_nrt l=loc_map.find(*t_it)->second;
- node.successors.push_back(l);
+ node.successors.push_back(l);
}
break;
-
+
case START_THREAD:
node.successors.push_back(loc_nr+1);
-
+
for(goto_programt::targetst::const_iterator
t_it=instruction.targets.begin();
t_it!=instruction.targets.end();
t_it++)
{
node_nrt l=loc_map.find(*t_it)->second;
- node.successors.push_back(l);
+ node.successors.push_back(l);
}
break;
-
+
case THROW:
case END_FUNCTION:
case END_THREAD:
@@ -91,6 +91,5 @@ void local_cfgt::build(const goto_programt &goto_program)
default:
node.successors.push_back(loc_nr+1);
}
- }
+ }
}
-
diff --git a/src/analyses/local_cfg.h b/src/analyses/local_cfg.h
index 687fa7fc8f3..92eda353932 100644
--- a/src/analyses/local_cfg.h
+++ b/src/analyses/local_cfg.h
@@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
/*******************************************************************\
Class: local_cfgt
-
+
Purpose:
\*******************************************************************/
@@ -36,16 +36,16 @@ class local_cfgt
typedef std::map loc_mapt;
loc_mapt loc_map;
-
+
typedef std::vector nodest;
nodest nodes;
-
+
inline explicit local_cfgt(const goto_programt &_goto_program)
{
build(_goto_program);
}
-protected:
+protected:
void build(const goto_programt &goto_program);
};
diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
index 787648554c6..c69158aebd7 100644
--- a/src/analyses/local_may_alias.cpp
+++ b/src/analyses/local_may_alias.cpp
@@ -33,7 +33,7 @@ Function: local_may_aliast::loc_infot::merge
bool local_may_aliast::loc_infot::merge(const loc_infot &src)
{
bool changed=false;
-
+
// do union; this should be amortized linear
for(std::size_t i=0; i local_may_aliast::get(
const exprt &rhs) const
{
local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t);
-
+
assert(loc_it!=cfg.loc_map.end());
-
+
const loc_infot &loc_info_src=loc_infos[loc_it->second];
-
+
object_sett result_tmp;
get_rec(result_tmp, rhs, loc_info_src);
@@ -165,7 +165,7 @@ std::set local_may_aliast::get(
{
result.insert(objects[*it]);
}
-
+
return result;
}
@@ -177,7 +177,7 @@ Function: local_may_aliast::aliases
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -186,11 +186,11 @@ bool local_may_aliast::aliases(
const exprt &src1, const exprt &src2) const
{
local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t);
-
+
assert(loc_it!=cfg.loc_map.end());
-
+
const loc_infot &loc_info_src=loc_infos[loc_it->second];
-
+
object_sett tmp1, tmp2;
get_rec(tmp1, src1, loc_info_src);
get_rec(tmp2, src2, loc_info_src);
@@ -200,12 +200,12 @@ bool local_may_aliast::aliases(
return true;
std::list result;
-
+
std::set_intersection(
tmp1.begin(), tmp1.end(),
tmp2.begin(), tmp2.end(),
std::back_inserter(result));
-
+
return !result.empty();
}
@@ -217,7 +217,7 @@ Function: local_may_aliast::get_rec
Outputs:
- Purpose:
+ Purpose:
\*******************************************************************/
@@ -238,9 +238,9 @@ void local_may_aliast::get_rec(
if(rhs.type().id()==ID_pointer)
{
unsigned src_pointer=objects.number(rhs);
-
+
dest.insert(src_pointer);
-
+
for(std::size_t i=0; isource_location << "\n";
const loc_infot &loc_info=loc_infos[l];
-
+
for(std::size_t i=0; i work_queuet;
mutable numbering objects;
-
+
typedef unsigned_union_find alias_sett;
- // the information tracked per program location
+ // the information tracked per program location
class loc_infot
{
public:
alias_sett aliases;
-
+
bool merge(const loc_infot &src);
};
typedef std::vector loc_infost;
loc_infost loc_infos;
-
+
void assign_lhs(
const exprt &lhs,
const exprt &rhs,
const loc_infot &loc_info_src,
loc_infot &loc_info_dest);
-
- typedef std::set object_sett;
-
+
+ typedef std::set object_sett;
+
void get_rec(
object_sett &dest,
const exprt &rhs,
const loc_infot &loc_info_src) const;
-
+
unsigned unknown_object;
};
@@ -102,7 +102,7 @@ class local_may_alias_factoryt
inline local_may_alias_factoryt():goto_functions(NULL)
{
}
-
+
inline void operator()(const goto_functionst &_goto_functions)
{
goto_functions=&_goto_functions;
@@ -111,7 +111,7 @@ class local_may_alias_factoryt
forall_goto_program_instructions(i_it, f_it->second.body)
target_map[i_it]=f_it->first;
}
-
+
local_may_aliast & operator()(const irep_idt &fkt)
{
assert(goto_functions!=NULL);
@@ -123,7 +123,7 @@ class local_may_alias_factoryt
return *(fkt_map[fkt]=std::unique_ptr(
new local_may_aliast(f_it2->second)));
}
-
+
local_may_aliast & operator()(goto_programt::const_targett t)
{
target_mapt::const_iterator t_it=
@@ -131,13 +131,13 @@ class local_may_alias_factoryt
assert(t_it!=target_map.end());
return operator()(t_it->second);
}
-
+
std::set get(
const goto_programt::const_targett t,
const exprt &src) const;
protected:
- const goto_functionst *goto_functions;
+ const goto_functionst *goto_functions;
typedef std::map > fkt_mapt;
fkt_mapt fkt_map;
diff --git a/src/analyses/locals.cpp b/src/analyses/locals.cpp
index 590da4bcd9e..e9a41949e50 100644
--- a/src/analyses/locals.cpp
+++ b/src/analyses/locals.cpp
@@ -33,10 +33,10 @@ void localst::build(const goto_functiont &goto_function)
locals_map[code_decl.get_identifier()]=
to_symbol_expr(code_decl.symbol());
}
-
+
const code_typet::parameterst ¶meters=
goto_function.type.parameters();
-
+
for(code_typet::parameterst::const_iterator
it=parameters.begin();
it!=parameters.end();
diff --git a/src/analyses/locals.h b/src/analyses/locals.h
index 3732d3a58b1..78883ad4699 100644
--- a/src/analyses/locals.h
+++ b/src/analyses/locals.h
@@ -35,7 +35,7 @@ class localst
typedef std::map locals_mapt;
locals_mapt locals_map;
-
+
protected:
void build(const goto_functiont &goto_function);
};
diff --git a/src/analyses/natural_loops.cpp b/src/analyses/natural_loops.cpp
index 5fa585db07a..92a1dc1efce 100644
--- a/src/analyses/natural_loops.cpp
+++ b/src/analyses/natural_loops.cpp
@@ -33,8 +33,7 @@ void show_natural_loops(const goto_functionst &goto_functions)
natural_loopst natural_loops;
natural_loops(it->second.body);
natural_loops.output(std::cout);
-
+
std::cout << std::endl;
}
}
-
diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h
index 204cf3362ae..50f84183370 100644
--- a/src/analyses/natural_loops.h
+++ b/src/analyses/natural_loops.h
@@ -26,7 +26,7 @@ class natural_loops_templatet
// map loop headers to loops
typedef std::map loop_mapt;
-
+
loop_mapt loop_map;
inline void operator()(P &program)
@@ -35,12 +35,12 @@ class natural_loops_templatet
}
void output(std::ostream &) const;
-
+
inline const cfg_dominators_templatet& get_dominator_info() const
{
return cfg_dominators;
}
-
+
inline natural_loops_templatet()
{
}
@@ -55,7 +55,7 @@ class natural_loops_templatet
typedef typename cfg_dominators_templatet
::cfgt::nodet nodet;
void compute(P &program);
- void compute_natural_loop(T, T);
+ void compute_natural_loop(T, T);
};
class natural_loopst:
@@ -109,10 +109,10 @@ void natural_loops_templatet
::compute(P &program)
{
const nodet &node=
cfg_dominators.cfg[cfg_dominators.cfg.entry_map[m_it]];
-
+
#ifdef DEBUG
- std::cout << "Computing loop for "
- << m_it->location_number << " -> "
+ std::cout << "Computing loop for "
+ << m_it->location_number << " -> "
<< (*n_it)->location_number << "\n";
#endif
if(node.dominators.find(*n_it)!=node.dominators.end())
@@ -142,7 +142,7 @@ template
void natural_loops_templatet::compute_natural_loop(T m, T n)
{
assert(n->location_number<=m->location_number);
-
+
std::stack stack;
natural_loopt &loop=loop_map[n];
@@ -194,7 +194,7 @@ void natural_loops_templatet::output(std::ostream &out) const
h_it!=loop_map.end(); ++h_it)
{
unsigned n=h_it->first->location_number;
-
+
out << n << " is head of { ";
for(typename natural_loopt::const_iterator l_it=h_it->second.begin();
l_it!=h_it->second.end(); ++l_it)
diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp
index ea43251fb97..c0cda391b9e 100644
--- a/src/analyses/reaching_definitions.cpp
+++ b/src/analyses/reaching_definitions.cpp
@@ -961,4 +961,3 @@ void reaching_definitions_analysist::initialize(
concurrency_aware_ait::initialize(goto_functions);
}
-
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index 4eb76ffaae0..91225e8fc86 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -249,4 +249,3 @@ class reaching_definitions_analysist :
};
#endif
-
diff --git a/src/analyses/replace_symbol_ext.cpp b/src/analyses/replace_symbol_ext.cpp
index 2a53bca1faf..801ce69e881 100644
--- a/src/analyses/replace_symbol_ext.cpp
+++ b/src/analyses/replace_symbol_ext.cpp
@@ -32,7 +32,7 @@ bool replace_symbol_extt::replace(exprt &dest) const
if(have_to_replace(dest.type()))
if(!replace_symbolt::replace(dest.type()))
result=false;
-
+
// now do expression itself
if(!have_to_replace(dest))
diff --git a/src/analyses/static_analysis.cpp b/src/analyses/static_analysis.cpp
index 656644d42c9..3737e109ab7 100644
--- a/src/analyses/static_analysis.cpp
+++ b/src/analyses/static_analysis.cpp
@@ -46,7 +46,7 @@ exprt static_analysis_baset::get_guard(
tmp.make_not();
return tmp;
}
-
+
return from->guard;
}
@@ -70,13 +70,13 @@ exprt static_analysis_baset::get_return_lhs(locationt to)
if(to->is_end_function())
return static_cast(get_nil_irep());
-
+
// must be the function call
assert(to->is_function_call());
const code_function_callt &code=
to_code_function_call(to->code);
-
+
return code.lhs();
}
@@ -270,11 +270,11 @@ void static_analysis_baset::update(
if(!has_location(i_it))
{
generate_state(i_it);
-
+
if(!first)
merge(get_state(i_it), get_state(previous), i_it);
}
-
+
first=false;
previous=i_it;
}
@@ -296,11 +296,11 @@ static_analysis_baset::locationt static_analysis_baset::get_next(
working_sett &working_set)
{
assert(!working_set.empty());
-
+
working_sett::iterator i=working_set.begin();
locationt l=i->second;
working_set.erase(i);
-
+
return l;
}
@@ -322,19 +322,19 @@ bool static_analysis_baset::fixedpoint(
{
if(goto_program.instructions.empty())
return false;
-
+
working_sett working_set;
put_in_working_set(
working_set,
goto_program.instructions.begin());
-
+
bool new_data=false;
while(!working_set.empty())
{
locationt l=get_next(working_set);
-
+
if(visit(l, working_set, goto_program, goto_functions))
new_data=true;
}
@@ -365,7 +365,7 @@ bool static_analysis_baset::visit(
statet ¤t=get_state(l);
current.seen=true;
-
+
goto_programt::const_targetst successors;
goto_program.get_successors(l, successors);
@@ -382,7 +382,7 @@ bool static_analysis_baset::visit(
std::unique_ptr tmp_state(
make_temporary_state(current));
-
+
statet &new_values=*tmp_state;
if(l->is_function_call())
@@ -400,19 +400,19 @@ bool static_analysis_baset::visit(
}
else
new_values.transform(ns, l, to_l);
-
+
statet &other=get_state(to_l);
bool have_new_values=
merge(other, new_values, to_l);
-
+
if(have_new_values)
new_data=true;
-
+
if(have_new_values || !other.seen)
put_in_working_set(working_set, to_l);
}
-
+
return new_data;
}
@@ -439,17 +439,17 @@ void static_analysis_baset::do_function_call(
if(!goto_function.body_available())
return; // do nothing
-
+
assert(!goto_function.body.instructions.empty());
{
// get the state at the beginning of the function
locationt l_begin=goto_function.body.instructions.begin();
-
+
// do the edge from the call site to the beginning of the function
std::unique_ptr tmp_state(make_temporary_state(new_state));
- tmp_state->transform(ns, l_call, l_begin);
-
+ tmp_state->transform(ns, l_call, l_begin);
+
statet &begin_state=get_state(l_begin);
bool new_data=false;
@@ -497,7 +497,7 @@ void static_analysis_baset::do_function_call(
// effect on current procedure (if any)
new_state.transform(ns, l_call, l_return);
}
-}
+}
/*******************************************************************\
@@ -525,7 +525,7 @@ void static_analysis_baset::do_function_call_rec(
if(function.id()==ID_symbol)
{
const irep_idt &identifier=function.get(ID_identifier);
-
+
if(recursion_set.find(identifier)!=recursion_set.end())
{
// recursion detected!
@@ -533,29 +533,29 @@ void static_analysis_baset::do_function_call_rec(
}
else
recursion_set.insert(identifier);
-
+
goto_functionst::function_mapt::const_iterator it=
goto_functions.function_map.find(identifier);
-
+
if(it==goto_functions.function_map.end())
throw "failed to find function "+id2string(identifier);
-
+
do_function_call(
l_call, l_return,
goto_functions,
it,
arguments,
new_state);
-
+
recursion_set.erase(identifier);
}
else if(function.id()==ID_if)
{
if(function.operands().size()!=3)
throw "if takes three arguments";
-
+
std::unique_ptr n2(make_temporary_state(new_state));
-
+
do_function_call_rec(
l_call, l_return,
function.op1(),
@@ -569,7 +569,7 @@ void static_analysis_baset::do_function_call_rec(
arguments,
*n2,
goto_functions);
-
+
merge(new_state, *n2, l_return);
}
else if(function.id()==ID_dereference)
@@ -588,7 +588,7 @@ void static_analysis_baset::do_function_call_rec(
if(it->id()==ID_object_descriptor)
{
const object_descriptor_exprt &o=to_object_descriptor_expr(*it);
- std::unique_ptr n2(make_temporary_state(new_state));
+ std::unique_ptr n2(make_temporary_state(new_state));
do_function_call_rec(l_call, l_return, o.object(), arguments, *n2, goto_functions);
merge(new_state, *n2, l_return);
}
@@ -718,4 +718,3 @@ void static_analysis_baset::concurrent_fixedpoint(
}
}
}
-
diff --git a/src/analyses/static_analysis.h b/src/analyses/static_analysis.h
index 830918f53e3..4d289296938 100644
--- a/src/analyses/static_analysis.h
+++ b/src/analyses/static_analysis.h
@@ -30,7 +30,7 @@ class domain_baset
virtual ~domain_baset()
{
}
-
+
typedef goto_programt::const_targett locationt;
// will go away,
@@ -59,10 +59,10 @@ class domain_baset
std::ostream &out) const
{
}
-
+
typedef hash_set_cont expr_sett;
- // will go away
+ // will go away
virtual void get_reference_set(
const namespacet &ns,
const exprt &expr,
@@ -71,17 +71,17 @@ class domain_baset
// dummy, overload me!
dest.clear();
}
-
+
// also add
//
// bool merge(const T &b, locationt to);
//
// this computes the join between "this" and "b"
// return true if "this" has changed
-
+
protected:
bool seen;
-
+
friend class static_analysis_baset;
};
@@ -98,7 +98,7 @@ class static_analysis_baset
initialized(false)
{
}
-
+
virtual void initialize(
const goto_programt &goto_program)
{
@@ -108,7 +108,7 @@ class static_analysis_baset
generate_states(goto_program);
}
}
-
+
virtual void initialize(
const goto_functionst &goto_functions)
{
@@ -118,13 +118,13 @@ class static_analysis_baset
generate_states(goto_functions);
}
}
-
+
virtual void update(const goto_programt &goto_program);
virtual void update(const goto_functionst &goto_functions);
-
+
virtual void operator()(
const goto_programt &goto_program);
-
+
virtual void operator()(
const goto_functionst &goto_functions);
@@ -136,7 +136,7 @@ class static_analysis_baset
{
initialized=false;
}
-
+
virtual void output(
const goto_functionst &goto_functions,
std::ostream &out) const;
@@ -149,33 +149,33 @@ class static_analysis_baset
}
virtual bool has_location(locationt l) const=0;
-
+
void insert(locationt l)
{
generate_state(l);
}
- // utilities
-
+ // utilities
+
// get guard of a conditional edge
static exprt get_guard(locationt from, locationt to);
-
+
// get lhs that return value is assigned to
// for an edge that returns from a function
static exprt get_return_lhs(locationt to);
protected:
const namespacet &ns;
-
+
virtual void output(
const goto_programt &goto_program,
const irep_idt &identifier,
std::ostream &out) const;
typedef std::map working_sett;
-
+
locationt get_next(working_sett &working_set);
-
+
void put_in_working_set(
working_sett &working_set,
locationt l)
@@ -188,7 +188,7 @@ class static_analysis_baset
bool fixedpoint(
const goto_programt &goto_program,
const goto_functionst &goto_functions);
-
+
virtual void fixedpoint(
const goto_functionst &goto_functions)=0;
@@ -203,31 +203,31 @@ class static_analysis_baset
working_sett &working_set,
const goto_programt &goto_program,
const goto_functionst &goto_functions);
-
+
static locationt successor(locationt l)
{
l++;
return l;
}
-
+
virtual bool merge(statet &a, const statet &b, locationt to)=0;
// for concurrent fixedpoint
virtual bool merge_shared(statet &a, const statet &b, locationt to)=0;
-
+
typedef std::set functions_donet;
functions_donet functions_done;
typedef std::set recursion_sett;
recursion_sett recursion_set;
-
+
void generate_states(
const goto_functionst &goto_functions);
void generate_states(
const goto_programt &goto_program);
-
+
bool initialized;
-
+
// function calls
void do_function_call_rec(
locationt l_call, locationt l_return,
@@ -244,7 +244,7 @@ class static_analysis_baset
statet &new_state);
// abstract methods
-
+
virtual void generate_state(locationt l)=0;
virtual statet &get_state(locationt l)=0;
virtual const statet &get_state(locationt l) const=0;
@@ -277,14 +277,14 @@ class static_analysist:public static_analysis_baset
if(it==state_map.end()) throw "failed to find state";
return it->second;
}
-
+
inline const T &operator[](locationt l) const
{
typename state_mapt::const_iterator it=state_map.find(l);
if(it==state_map.end()) throw "failed to find state";
return it->second;
}
-
+
virtual void clear()
{
state_map.clear();
@@ -295,7 +295,7 @@ class static_analysist:public static_analysis_baset
{
return state_map.count(l)!=0;
}
-
+
protected:
typedef std::map state_mapt;
state_mapt state_map;
@@ -318,7 +318,7 @@ class static_analysist:public static_analysis_baset
{
return static_cast(a).merge(static_cast(b), to);
}
-
+
virtual statet *make_temporary_state(statet &s)
{
return new T(static_cast(s));
@@ -342,7 +342,7 @@ class static_analysist:public static_analysis_baset
sequential_fixedpoint(goto_functions);
}
-private:
+private:
// to enforce that T is derived from domain_baset
void dummy(const T &s) { const statet &x=dummy1(s); (void)x; }
diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp
index 4967df42c80..cb58c208158 100644
--- a/src/analyses/uninitialized_domain.cpp
+++ b/src/analyses/uninitialized_domain.cpp
@@ -50,7 +50,7 @@ void uninitialized_domaint::transform(
std::list written=expressions_written(*from);
forall_expr_list(it, written) assign(*it);
-
+
// we only care about the *first* uninitalized use
forall_expr_list(it, read) assign(*it);
}
@@ -121,7 +121,7 @@ bool uninitialized_domaint::merge(
locationt to)
{
unsigned old_uninitialized=uninitialized.size();
-
+
uninitialized.insert(
other.uninitialized.begin(),
other.uninitialized.end());
diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h
index 78064e86c37..04066fe4b47 100644
--- a/src/analyses/uninitialized_domain.h
+++ b/src/analyses/uninitialized_domain.h
@@ -27,17 +27,16 @@ class uninitialized_domaint:public ai_domain_baset
std::ostream &out,
const ai_baset &ai,
const namespacet &ns) const;
-
+
// returns true iff there is s.th. new
bool merge(
const uninitialized_domaint &other,
locationt from,
locationt to);
-
+
protected:
void assign(const exprt &lhs);
};
typedef ait
uninitialized_analysist;
-
diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile
index 0764c137f49..5d6381c6b00 100644
--- a/src/ansi-c/Makefile
+++ b/src/ansi-c/Makefile
@@ -79,7 +79,7 @@ library_check: library/*.c
[ $$ec -eq 0 ] || exit $$ec ; \
done
touch $@
-
+
cprover_library.inc: library/converter$(EXEEXT) library/*.c
cat library/*.c | library/converter$(EXEEXT) > $@
@@ -108,6 +108,5 @@ generated_files: cprover_library.inc gcc_builtin_headers_generic.inc \
###############################################################################
-ansi-c$(LIBEXT): $(OBJ)
+ansi-c$(LIBEXT): $(OBJ)
$(LINKLIB)
-
diff --git a/src/ansi-c/anonymous_member.cpp b/src/ansi-c/anonymous_member.cpp
index b4309576fa8..9aa1d2317b9 100644
--- a/src/ansi-c/anonymous_member.cpp
+++ b/src/ansi-c/anonymous_member.cpp
@@ -34,7 +34,7 @@ static exprt make_member_expr(
if(struct_union.get_bool(ID_C_lvalue))
result.set(ID_C_lvalue, true);
- // todo: should to typedef chains properly
+ // todo: should to typedef chains properly
const typet &type=
ns.follow(struct_union.type());
@@ -42,7 +42,7 @@ static exprt make_member_expr(
type.get_bool(ID_C_constant) ||
struct_union.type().get_bool(ID_C_constant))
result.set(ID_C_constant, true);
-
+
return result;
}
@@ -75,7 +75,7 @@ exprt get_component_rec(
it++)
{
const typet &type=ns.follow(it->type());
-
+
if(it->get_name()==component_name)
{
return make_member_expr(struct_union, *it, ns);
@@ -88,7 +88,7 @@ exprt get_component_rec(
if(result.is_not_nil()) return result;
}
}
-
+
return nil_exprt();
}
@@ -130,6 +130,6 @@ bool has_component_rec(
return true;
}
}
-
+
return false;
}
diff --git a/src/ansi-c/anonymous_member.h b/src/ansi-c/anonymous_member.h
index 865066f8e5b..df76e716427 100644
--- a/src/ansi-c/anonymous_member.h
+++ b/src/ansi-c/anonymous_member.h
@@ -18,4 +18,3 @@ bool has_component_rec(
const typet &struct_union_type,
const irep_idt &component_name,
const namespacet &ns);
-
diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
index b445aa5f2d1..8fde8c57c4d 100644
--- a/src/ansi-c/ansi_c_convert_type.cpp
+++ b/src/ansi-c/ansi_c_convert_type.cpp
@@ -119,7 +119,7 @@ void ansi_c_convert_typet::read_rec(const typet &type)
bv_cnt++;
const exprt &size_expr=
static_cast(type.find(ID_size));
-
+
bv_width=size_expr;
}
else if(type.id()==ID_custom_floatbv)
@@ -207,7 +207,7 @@ void ansi_c_convert_typet::read_rec(const typet &type)
{
const exprt &as_expr=
static_cast(static_cast(type));
-
+
forall_operands(it, as_expr)
{
// these are symbols
@@ -254,7 +254,7 @@ Function: ansi_c_convert_typet::write
void ansi_c_convert_typet::write(typet &type)
{
type.clear();
-
+
// first, do "other"
if(!other.empty())
@@ -437,7 +437,7 @@ void ansi_c_convert_typet::write(typet &type)
else
{
// it is integer -- signed or unsigned?
-
+
bool is_signed=true; // default
if(signed_cnt && unsigned_cnt)
@@ -459,7 +459,7 @@ void ansi_c_convert_typet::write(typet &type)
error() << "conflicting type modifiers" << eom;
throw 0;
}
-
+
if(int8_cnt)
type=is_signed?signed_char_type():unsigned_char_type();
else if(int16_cnt)
@@ -535,7 +535,7 @@ void ansi_c_convert_typet::write(typet &type)
new_type.subtype().swap(type);
type=new_type;
}
-
+
if(complex_cnt)
{
// These take more or less arbitrary subtypes.
@@ -551,7 +551,7 @@ void ansi_c_convert_typet::write(typet &type)
new_type.subtype()=type;
type.swap(new_type);
}
-
+
c_qualifiers.write(type);
if(packed)
diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h
index b8060b80dcf..f87e4c86a8f 100644
--- a/src/ansi-c/ansi_c_convert_type.h
+++ b/src/ansi-c/ansi_c_convert_type.h
@@ -22,7 +22,7 @@ class ansi_c_convert_typet:public messaget
int_cnt, short_cnt, long_cnt,
double_cnt, float_cnt, c_bool_cnt,
proper_bool_cnt, complex_cnt;
-
+
// extensions
unsigned int8_cnt, int16_cnt, int32_cnt, int64_cnt,
ptr32_cnt, ptr64_cnt,
@@ -30,7 +30,7 @@ class ansi_c_convert_typet:public messaget
floatbv_cnt, fixedbv_cnt;
typet gcc_attribute_mode;
-
+
bool packed, aligned;
exprt vector_size, alignment, bv_width, fraction_width;
exprt msc_based; // this is Visual Studio
@@ -38,22 +38,22 @@ class ansi_c_convert_typet:public messaget
// storage spec
c_storage_spect c_storage_spec;
-
+
// qualifiers
c_qualifierst c_qualifiers;
void read(const typet &type);
void write(typet &type);
-
+
source_locationt source_location;
-
+
std::list other;
-
+
ansi_c_convert_typet(message_handlert &_message_handler):
messaget(_message_handler)
{
}
-
+
void clear()
{
unsigned_cnt=signed_cnt=char_cnt=int_cnt=short_cnt=
@@ -67,14 +67,14 @@ class ansi_c_convert_typet:public messaget
fraction_width.make_nil();
msc_based.make_nil();
gcc_attribute_mode.make_nil();
-
+
packed=aligned=constructor=destructor=false;
other.clear();
c_storage_spec.clear();
c_qualifiers.clear();
}
-
+
protected:
void read_rec(const typet &type);
};
diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp
index c006c34cd5e..f9dea43c02b 100644
--- a/src/ansi-c/ansi_c_declaration.cpp
+++ b/src/ansi-c/ansi_c_declaration.cpp
@@ -29,7 +29,7 @@ Function: ansi_c_declaratort::build
void ansi_c_declaratort::build(irept &src)
{
typet *p=static_cast(&src);
-
+
// walk down subtype until we hit symbol or "abstract"
while(true)
{
@@ -62,7 +62,7 @@ void ansi_c_declaratort::build(irept &src)
else
p=&t.subtype();
}
-
+
type()=static_cast(src);
value().make_nil();
}
@@ -95,7 +95,7 @@ void ansi_c_declarationt::output(std::ostream &out) const
out << "\n";
out << "Type: " << type().pretty() << "\n";
-
+
for(declaratorst::const_iterator d_it=declarators().begin();
d_it!=declarators().end();
d_it++)
@@ -123,7 +123,7 @@ typet ansi_c_declarationt::full_type(
// this gets types that are still raw parse trees
while(p->is_not_nil())
{
- if(p->id()==ID_pointer || p->id()==ID_array ||
+ if(p->id()==ID_pointer || p->id()==ID_array ||
p->id()==ID_vector || p->id()==ID_c_bit_field ||
p->id()==ID_block_pointer || p->id()==ID_code)
p=&p->subtype();
@@ -138,7 +138,7 @@ typet ansi_c_declarationt::full_type(
}
*p=type();
-
+
return result;
}
@@ -158,7 +158,7 @@ void ansi_c_declarationt::to_symbol(
const ansi_c_declaratort &declarator,
symbolt &symbol) const
{
- symbol.clear();
+ symbol.clear();
symbol.value=declarator.value();
symbol.type=full_type(declarator);
symbol.name=declarator.get_name();
@@ -169,16 +169,16 @@ void ansi_c_declarationt::to_symbol(
symbol.is_macro=get_is_typedef() || get_is_enum_constant();
symbol.is_parameter=get_is_parameter();
symbol.is_weak=get_is_weak();
-
+
// is it a function?
-
+
if(symbol.type.id()==ID_code && !symbol.is_type)
{
symbol.is_static_lifetime=false;
symbol.is_thread_local=false;
symbol.is_file_local=get_is_static();
-
+
if(get_is_inline())
symbol.type.set(ID_C_inlined, true);
@@ -205,13 +205,13 @@ void ansi_c_declarationt::to_symbol(
!symbol.is_macro &&
!symbol.is_type &&
(get_is_global() || get_is_static());
-
+
symbol.is_thread_local=
(!symbol.is_static_lifetime && !get_is_extern()) ||
get_is_thread_local();
-
+
symbol.is_file_local=
- symbol.is_macro ||
+ symbol.is_macro ||
(!get_is_global() && !get_is_extern()) ||
(get_is_global() && get_is_static()) ||
symbol.is_parameter;
diff --git a/src/ansi-c/ansi_c_declaration.h b/src/ansi-c/ansi_c_declaration.h
index 25c00feda6f..87ea59a818a 100644
--- a/src/ansi-c/ansi_c_declaration.h
+++ b/src/ansi-c/ansi_c_declaration.h
@@ -24,27 +24,27 @@ class ansi_c_declaratort:public exprt
{
return static_cast(add(ID_value));
}
-
+
inline const exprt &value() const
{
return static_cast(find(ID_value));
}
-
+
inline void set_name(const irep_idt &name)
{
return set(ID_name, name);
}
-
+
inline irep_idt get_name() const
{
return get(ID_name);
}
-
+
inline irep_idt get_base_name() const
{
return get(ID_base_name);
}
-
+
inline void set_base_name(const irep_idt &base_name)
{
return set(ID_base_name, base_name);
@@ -71,112 +71,112 @@ class ansi_c_declarationt:public exprt
inline ansi_c_declarationt():exprt(ID_declaration)
{
}
-
+
inline bool get_is_typedef() const
{
return get_bool(ID_is_typedef);
}
-
+
inline void set_is_typedef(bool is_typedef)
{
set(ID_is_typedef, is_typedef);
}
-
+
inline bool get_is_enum_constant() const
{
return get_bool(ID_is_enum_constant);
}
-
+
inline void set_is_enum_constant(bool is_enum_constant)
{
set(ID_is_enum_constant, is_enum_constant);
}
-
+
inline bool get_is_static() const
{
return get_bool(ID_is_static);
}
-
+
inline void set_is_static(bool is_static)
{
set(ID_is_static, is_static);
}
-
+
inline bool get_is_parameter() const
{
return get_bool(ID_is_parameter);
}
-
+
inline void set_is_parameter(bool is_parameter)
{
set(ID_is_parameter, is_parameter);
}
-
+
inline bool get_is_member() const
{
return get_bool(ID_is_member);
}
-
+
inline void set_is_member(bool is_member)
{
set(ID_is_member, is_member);
}
-
+
inline bool get_is_global() const
{
return get_bool(ID_is_global);
}
-
+
inline void set_is_global(bool is_global)
{
set(ID_is_global, is_global);
}
-
+
inline bool get_is_register() const
{
return get_bool(ID_is_register);
}
-
+
inline void set_is_register(bool is_register)
{
set(ID_is_register, is_register);
}
-
+
inline bool get_is_thread_local() const
{
return get_bool(ID_is_thread_local);
}
-
+
inline void set_is_thread_local(bool is_thread_local)
{
set(ID_is_thread_local, is_thread_local);
}
-
+
inline bool get_is_inline() const
{
return get_bool(ID_is_inline);
}
-
+
inline void set_is_inline(bool is_inline)
{
set(ID_is_inline, is_inline);
}
-
+
inline bool get_is_extern() const
{
return get_bool(ID_is_extern);
}
-
+
inline void set_is_extern(bool is_extern)
{
set(ID_is_extern, is_extern);
}
-
+
inline bool get_is_static_assert() const
{
return get_bool(ID_is_static_assert);
}
-
+
inline void set_is_static_assert(bool is_static_assert)
{
set(ID_is_static_assert, is_static_assert);
@@ -191,7 +191,7 @@ class ansi_c_declarationt:public exprt
{
set(ID_is_weak, is_weak);
}
-
+
void to_symbol(
const ansi_c_declaratort &,
symbolt &symbol) const;
@@ -210,7 +210,7 @@ class ansi_c_declarationt:public exprt
return (declaratorst &)operands();
}
- // special case of a declaration with exactly one declarator
+ // special case of a declaration with exactly one declarator
inline const ansi_c_declaratort &declarator() const
{
assert(declarators().size()==1);
@@ -222,9 +222,9 @@ class ansi_c_declarationt:public exprt
assert(declarators().size()==1);
return declarators()[0];
}
-
+
void output(std::ostream &) const;
-
+
inline void add_initializer(exprt &value)
{
assert(!declarators().empty());
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index f4db1403fbd..1acfb7d4459 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/src/ansi-c/ansi_c_entry_point.cpp
@@ -46,7 +46,7 @@ exprt::operandst build_function_environment(
{
exprt::operandst result;
result.resize(parameters.size());
-
+
std::size_t i=0;
for(const auto & p : parameters)
@@ -55,25 +55,25 @@ exprt::operandst build_function_environment(
if(base_name.empty()) base_name="argument#"+i2string(i);
irep_idt identifier=id2string(goto_functionst::entry_point())+
"::"+id2string(base_name);
-
- {
+
+ {
auxiliary_symbolt new_symbol;
new_symbol.mode=ID_C;
new_symbol.is_static_lifetime=false;
new_symbol.name=identifier;
new_symbol.base_name=base_name;
new_symbol.type=p.type();
-
+
symbol_table.move(new_symbol);
}
-
+
symbol_exprt symbol_expr(identifier, p.type());
code_declt decl;
decl.symbol()=symbol_expr;
-
+
init_code.add(decl);
-
+
codet input(ID_input);
input.operands().resize(2);
@@ -82,13 +82,13 @@ exprt::operandst build_function_environment(
index_exprt(string_constantt(base_name), gen_zero(index_type())));
input.op1()=symbol_expr;
input.add_source_location()=p.source_location();
-
+
init_code.move_to_operands(input);
-
+
result[i]=symbol_expr;
i++;
}
-
+
return result;
}
@@ -124,7 +124,7 @@ void record_function_outputs(
const symbolt &return_symbol=symbol_table.lookup("return'");
output.op0()=address_of_exprt(
- index_exprt(string_constantt(return_symbol.base_name),
+ index_exprt(string_constantt(return_symbol.base_name),
gen_zero(index_type())));
output.op1()=return_symbol.symbol_expr();
@@ -149,7 +149,7 @@ void record_function_outputs(
output.operands().resize(2);
output.op0()=address_of_exprt(
- index_exprt(string_constantt(symbol.base_name),
+ index_exprt(string_constantt(symbol.base_name),
gen_zero(index_type())));
output.op1()=symbol.symbol_expr();
output.add_source_location()=p.source_location();
@@ -185,35 +185,35 @@ bool ansi_c_entry_point(
return false; // silently ignore
irep_idt main_symbol;
-
+
// find main symbol
if(config.main!="")
{
std::list matches;
-
+
forall_symbol_base_map(it, symbol_table.symbol_base_map, config.main)
{
// look it up
symbol_tablet::symbolst::const_iterator s_it=symbol_table.symbols.find(it->second);
-
+
if(s_it==symbol_table.symbols.end()) continue;
-
+
if(s_it->second.type.id()==ID_code)
matches.push_back(it->second);
}
-
+
if(matches.empty())
{
messaget message(message_handler);
- message.error() << "main symbol `" << config.main
+ message.error() << "main symbol `" << config.main
<< "' not found" << messaget::eom;
return true; // give up
}
-
+
if(matches.size()>=2)
{
messaget message(message_handler);
- message.error() << "main symbol `" << config.main
+ message.error() << "main symbol `" << config.main
<< "' is ambiguous" << messaget::eom;
return true;
}
@@ -222,16 +222,16 @@ bool ansi_c_entry_point(
}
else
main_symbol=standard_main;
-
+
// look it up
symbol_tablet::symbolst::const_iterator s_it=
symbol_table.symbols.find(main_symbol);
-
+
if(s_it==symbol_table.symbols.end())
return false; // give up silently
-
+
const symbolt &symbol=s_it->second;
-
+
// check if it has a body
if(symbol.value.is_nil())
{
@@ -243,9 +243,9 @@ bool ansi_c_entry_point(
if(static_lifetime_init(symbol_table, symbol.location, message_handler))
return true;
-
+
code_blockt init_code;
-
+
// build call to initialization function
{
@@ -259,7 +259,7 @@ bool ansi_c_entry_point(
<< messaget::eom;
return true;
}
-
+
code_function_callt call_init;
call_init.lhs().make_nil();
call_init.add_source_location()=symbol.location;
@@ -269,7 +269,7 @@ bool ansi_c_entry_point(
}
// build call to main function
-
+
code_function_callt call_main;
call_main.add_source_location()=symbol.location;
call_main.function()=symbol.symbol_expr();
@@ -303,36 +303,36 @@ bool ansi_c_entry_point(
const symbolt &argc_symbol=ns.lookup("argc'");
const symbolt &argv_symbol=ns.lookup("argv'");
-
+
{
// assume argc is at least one
exprt one=from_integer(1, argc_symbol.type);
-
+
exprt ge(ID_ge, typet(ID_bool));
ge.copy_to_operands(argc_symbol.symbol_expr(), one);
-
+
codet assumption;
assumption.set_statement(ID_assume);
assumption.move_to_operands(ge);
init_code.move_to_operands(assumption);
}
-
+
{
// assume argc is at most MAX/8-1
mp_integer upper_bound=
power(2, config.ansi_c.int_width-4);
-
+
exprt bound_expr=from_integer(upper_bound, argc_symbol.type);
-
+
exprt le(ID_le, typet(ID_bool));
le.copy_to_operands(argc_symbol.symbol_expr(), bound_expr);
-
+
codet assumption;
assumption.set_statement(ID_assume);
assumption.move_to_operands(le);
init_code.move_to_operands(assumption);
}
-
+
{
// record argc as an input
codet input(ID_input);
@@ -342,14 +342,14 @@ bool ansi_c_entry_point(
input.op1()=argc_symbol.symbol_expr();
init_code.move_to_operands(input);
}
-
+
if(parameters.size()==3)
- {
+ {
const symbolt &envp_size_symbol=ns.lookup("envp_size'");
// assume envp_size is INTMAX-1
mp_integer max;
-
+
if(envp_size_symbol.type.id()==ID_signedbv)
{
max=to_signedbv_type(envp_size_symbol.type).largest();
@@ -360,21 +360,21 @@ bool ansi_c_entry_point(
}
else
assert(false);
-
+
exprt max_minus_one=from_integer(max-1, envp_size_symbol.type);
-
+
exprt le(ID_le, bool_typet());
le.copy_to_operands(envp_size_symbol.symbol_expr(), max_minus_one);
-
+
codet assumption;
assumption.set_statement(ID_assume);
assumption.move_to_operands(le);
init_code.move_to_operands(assumption);
}
-
+
{
/* zero_string doesn't work yet */
-
+
/*
exprt zero_string(ID_zero_string, array_typet());
zero_string.type().subtype()=char_type();
@@ -387,11 +387,11 @@ bool ansi_c_entry_point(
if(argv_symbol.type.subtype()!=address_of.type())
address_of.make_typecast(argv_symbol.type.subtype());
-
+
// assign argv[*] to the address of a string-object
exprt array_of("array_of", argv_symbol.type);
array_of.copy_to_operands(address_of);
-
+
init_code.copy_to_operands(
code_assignt(argv_symbol.symbol_expr(), array_of));
*/
@@ -401,12 +401,12 @@ bool ansi_c_entry_point(
// assign argv[argc] to NULL
exprt null(ID_constant, argv_symbol.type.subtype());
null.set(ID_value, ID_NULL);
-
+
exprt index_expr(ID_index, argv_symbol.type.subtype());
index_expr.copy_to_operands(
argv_symbol.symbol_expr(),
argc_symbol.symbol_expr());
-
+
// disable bounds check on that one
index_expr.set("bounds_check", false);
@@ -414,44 +414,44 @@ bool ansi_c_entry_point(
}
if(parameters.size()==3)
- {
+ {
const symbolt &envp_symbol=ns.lookup("envp'");
const symbolt &envp_size_symbol=ns.lookup("envp_size'");
-
+
// assume envp[envp_size] is NULL
exprt null(ID_constant, envp_symbol.type.subtype());
null.set(ID_value, ID_NULL);
-
+
exprt index_expr(ID_index, envp_symbol.type.subtype());
index_expr.copy_to_operands(
envp_symbol.symbol_expr(),
envp_size_symbol.symbol_expr());
-
+
// disable bounds check on that one
index_expr.set("bounds_check", false);
-
+
exprt is_null(ID_equal, typet(ID_bool));
is_null.copy_to_operands(index_expr, null);
-
+
codet assumption2;
assumption2.set_statement(ID_assume);
assumption2.move_to_operands(is_null);
init_code.move_to_operands(assumption2);
}
-
+
{
exprt::operandst &operands=call_main.arguments();
if(parameters.size()==3)
operands.resize(3);
- else
+ else
operands.resize(2);
-
+
exprt &op0=operands[0];
exprt &op1=operands[1];
-
+
op0=argc_symbol.symbol_expr();
-
+
{
const exprt &arg1=parameters[1];
@@ -460,7 +460,7 @@ bool ansi_c_entry_point(
// disable bounds check on that one
index_expr.set("bounds_check", false);
-
+
op1=exprt(ID_address_of, arg1.type());
op1.move_to_operands(index_expr);
}
@@ -472,11 +472,11 @@ bool ansi_c_entry_point(
exprt &op2=operands[2];
const exprt &arg2=parameters[2];
-
+
exprt index_expr(ID_index, arg2.type().subtype());
index_expr.copy_to_operands(
envp_symbol.symbol_expr(), gen_zero(index_type()));
-
+
op2=exprt(ID_address_of, arg2.type());
op2.move_to_operands(index_expr);
}
@@ -503,12 +503,12 @@ bool ansi_c_entry_point(
code_typet main_type;
main_type.return_type()=empty_typet();
-
+
new_symbol.name=goto_functionst::entry_point();
new_symbol.type.swap(main_type);
new_symbol.value.swap(init_code);
new_symbol.mode=symbol.mode;
-
+
if(symbol_table.move(new_symbol))
{
messaget message;
@@ -516,6 +516,6 @@ bool ansi_c_entry_point(
message.error() << "failed to move main symbol" << messaget::eom;
return true;
}
-
+
return false;
}
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index dc424d6cd57..ca4cf92f637 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -140,7 +140,7 @@ void ansi_c_internal_additions(std::string &code)
"void __CPROVER_input(const char *id, ...);\n"
"void __CPROVER_output(const char *id, ...);\n"
"void __CPROVER_cover(__CPROVER_bool condition);\n"
-
+
// concurrency-related
"void __CPROVER_atomic_begin();\n"
"void __CPROVER_atomic_end();\n"
@@ -151,13 +151,13 @@ void ansi_c_internal_additions(std::string &code)
// traces
"void CBMC_trace(int lvl, const char *event, ...);\n"
-
+
// pointers
"unsigned __CPROVER_POINTER_OBJECT(const void *p);\n"
"signed __CPROVER_POINTER_OFFSET(const void *p);\n"
"__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);\n"
"extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];\n"
-
+
// malloc
"void *__CPROVER_malloc(__CPROVER_size_t size);\n"
"const void *__CPROVER_deallocated=0;\n"
@@ -169,7 +169,7 @@ void ansi_c_internal_additions(std::string &code)
// this is ANSI-C
"extern __CPROVER_thread_local const char __func__[__CPROVER_constant_infinity_uint];\n"
-
+
// this is GCC
"extern __CPROVER_thread_local const char __FUNCTION__[__CPROVER_constant_infinity_uint];\n"
"extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];\n"
@@ -202,7 +202,7 @@ void ansi_c_internal_additions(std::string &code)
"double __CPROVER_fabs(double x);\n"
"long double __CPROVER_fabsl(long double x);\n"
"float __CPROVER_fabsf(float x);\n"
-
+
// arrays
"__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);\n"
"void __CPROVER_array_copy(const void *dest, const void *src);\n"
@@ -211,10 +211,10 @@ void ansi_c_internal_additions(std::string &code)
// k-induction
"void __CPROVER_k_induction_hint(unsigned min, unsigned max, "
"unsigned step, unsigned loop_free);\n"
-
+
// format string-related
"int __CPROVER_scanf(const char *, ...);\n"
-
+
// pipes, write, read, close
"struct __CPROVER_pipet {\n"
" _Bool widowed;\n"
@@ -228,7 +228,7 @@ void ansi_c_internal_additions(std::string &code)
"unsigned __CPROVER_pipe_count=0;\n"
"\n";
-
+
// GCC junk stuff, also for CLANG and ARM
if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC ||
config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE ||
@@ -246,7 +246,7 @@ void ansi_c_internal_additions(std::string &code)
{
if(config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE)
code+="typedef double __float128;\n"; // clang doesn't do __float128
-
+
code+=gcc_builtin_headers_ia32;
code+=gcc_builtin_headers_ia32_2;
}
@@ -290,15 +290,15 @@ void ansi_c_internal_additions(std::string &code)
if(config.ansi_c.os==configt::ansi_ct::ost::OS_WIN)
code+="int __noop();\n"
"int __assume(int);\n";
-
+
// ARM stuff
if(config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
code+=arm_builtin_headers;
-
+
// CW stuff
if(config.ansi_c.mode==configt::ansi_ct::flavourt::CODEWARRIOR)
code+=cw_builtin_headers;
-
+
// Architecture strings
ansi_c_architecture_strings(code);
}
diff --git a/src/ansi-c/ansi_c_internal_additions.h b/src/ansi-c/ansi_c_internal_additions.h
index 366af5f85a4..9ac0dc3a269 100644
--- a/src/ansi-c/ansi_c_internal_additions.h
+++ b/src/ansi-c/ansi_c_internal_additions.h
@@ -14,4 +14,3 @@ void ansi_c_architecture_strings(std::string &code);
extern const char gcc_builtin_headers_generic[];
extern const char gcc_builtin_headers_ia32[];
extern const char arm_builtin_headers[];
-
diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
index 5c80e6905a6..6e3b587d248 100644
--- a/src/ansi-c/ansi_c_language.cpp
+++ b/src/ansi-c/ansi_c_language.cpp
@@ -86,7 +86,7 @@ bool ansi_c_languaget::preprocess(
return c_preprocess(path, outstream, get_message_handler());
}
-
+
/*******************************************************************\
Function: ansi_c_languaget::parse
@@ -150,7 +150,7 @@ bool ansi_c_languaget::parse(
return result;
}
-
+
/*******************************************************************\
Function: ansi_c_languaget::typecheck
@@ -173,10 +173,10 @@ bool ansi_c_languaget::typecheck(
return true;
remove_internal_symbols(new_symbol_table);
-
+
if(linking(symbol_table, new_symbol_table, get_message_handler()))
return true;
-
+
return false;
}
@@ -196,7 +196,7 @@ bool ansi_c_languaget::final(symbol_tablet &symbol_table)
{
if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
return true;
-
+
return false;
}
@@ -211,7 +211,7 @@ Function: ansi_c_languaget::show_parse
Purpose:
\*******************************************************************/
-
+
void ansi_c_languaget::show_parse(std::ostream &out)
{
parse_tree.output(out);
@@ -308,7 +308,7 @@ Function: ansi_c_languaget::to_expr
Purpose:
\*******************************************************************/
-
+
bool ansi_c_languaget::to_expr(
const std::string &code,
const std::string &module,
@@ -321,7 +321,7 @@ bool ansi_c_languaget::to_expr(
std::istringstream i_preprocessed(
"void __my_expression = (void) (\n"+code+"\n);");
-
+
// parsing
ansi_c_parser.clear();
@@ -338,14 +338,14 @@ bool ansi_c_languaget::to_expr(
else
{
expr=ansi_c_parser.parse_tree.items.front().declarator().value();
-
+
// typecheck it
result=ansi_c_typecheck(expr, get_message_handler(), ns);
}
// save some memory
ansi_c_parser.clear();
-
+
// now remove that (void) cast
if(expr.id()==ID_typecast &&
expr.type().id()==ID_empty &&
diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h
index 901df70df7c..5344bce5ebb 100644
--- a/src/ansi-c/ansi_c_language.h
+++ b/src/ansi-c/ansi_c_language.h
@@ -29,7 +29,7 @@ class ansi_c_languaget:public languaget
virtual bool parse(
std::istream &instream,
const std::string &path);
-
+
virtual bool typecheck(
symbol_tablet &symbol_table,
const std::string &module);
@@ -38,10 +38,10 @@ class ansi_c_languaget:public languaget
symbol_tablet &symbol_table);
virtual void show_parse(std::ostream &out);
-
+
virtual ~ansi_c_languaget();
ansi_c_languaget() { }
-
+
virtual bool from_expr(
const exprt &expr,
std::string &code,
@@ -62,21 +62,21 @@ class ansi_c_languaget:public languaget
const std::string &module,
exprt &expr,
const namespacet &ns);
-
+
virtual languaget *new_language()
{ return new ansi_c_languaget; }
-
+
virtual std::string id() const { return "C"; }
virtual std::string description() const { return "ANSI-C 99"; }
virtual std::set extensions() const;
- virtual void modules_provided(std::set &modules);
-
+ virtual void modules_provided(std::set &modules);
+
protected:
ansi_c_parse_treet parse_tree;
std::string parse_path;
};
-
+
languaget *new_ansi_c_language();
-
+
#endif
diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp
index 5454b26f5f8..88787d4b519 100644
--- a/src/ansi-c/ansi_c_parser.cpp
+++ b/src/ansi-c/ansi_c_parser.cpp
@@ -36,7 +36,7 @@ ansi_c_id_classt ansi_c_parsert::lookup(
tag?"tag-"+id2string(base_name):
label?"label-"+id2string(base_name):
base_name;
-
+
for(scopest::const_reverse_iterator it=scopes.rbegin();
it!=scopes.rend();
it++)
@@ -51,7 +51,7 @@ ansi_c_id_classt ansi_c_parsert::lookup(
return n_it->second.id_class;
}
}
-
+
// Not found.
// If it's a tag, we will add to current scope.
if(tag)
@@ -87,7 +87,7 @@ void ansi_c_parsert::add_tag_with_body(irept &tag)
"tag-"+tag.get_string(ID_C_base_name);
irep_idt prefixed_name=current_scope().prefix+scope_name;
-
+
if(prefixed_name!=tag.get(ID_identifier))
{
// re-defined in a deeper scope
@@ -138,15 +138,15 @@ void ansi_c_parsert::add_declarator(
assert(declarator.is_not_nil());
ansi_c_declarationt &ansi_c_declaration=
to_ansi_c_declaration(declaration);
-
+
ansi_c_declaratort new_declarator;
new_declarator.build(declarator);
irep_idt base_name=new_declarator.get_base_name();
-
+
bool is_member=ansi_c_declaration.get_is_member();
bool is_parameter=ansi_c_declaration.get_is_parameter();
-
+
if(is_member)
{
// we don't put them into a struct scope (unlike C++)
@@ -154,7 +154,7 @@ void ansi_c_parsert::add_declarator(
ansi_c_declaration.declarators().push_back(new_declarator);
return; // done
}
-
+
// global?
if(current_scope().prefix=="")
ansi_c_declaration.set_is_global(true);
@@ -167,14 +167,14 @@ void ansi_c_parsert::add_declarator(
bool is_extern=c_storage_spec.is_extern;
bool force_root_scope=false;
-
+
// Functions always go into global scope, unless
// declared as a parameter or are typedefs.
if(new_declarator.type().id()==ID_code &&
!is_parameter &&
!is_typedef)
force_root_scope=true;
-
+
// variables marked as 'extern' always go into global scope
if(is_extern)
force_root_scope=true;
@@ -185,18 +185,18 @@ void ansi_c_parsert::add_declarator(
scopet &scope=
force_root_scope?root_scope():current_scope();
- // set the final name
+ // set the final name
irep_idt prefixed_name=force_root_scope?
base_name:
current_scope().prefix+id2string(base_name);
new_declarator.set_name(prefixed_name);
- // add to scope
+ // add to scope
ansi_c_identifiert &identifier=scope.name_map[base_name];
identifier.id_class=id_class;
identifier.prefixed_name=prefixed_name;
}
-
+
ansi_c_declaration.declarators().push_back(new_declarator);
}
@@ -211,7 +211,7 @@ Function: ansi_c_parsert::get_class
Purpose:
\*******************************************************************/
-
+
ansi_c_id_classt ansi_c_parsert::get_class(const typet &type)
{
if(type.id()==ID_typedef)
diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h
index b6440e815f5..0ca7f4f5b89 100644
--- a/src/ansi-c/ansi_c_parser.h
+++ b/src/ansi-c/ansi_c_parser.h
@@ -28,30 +28,30 @@ class ansi_c_parsert:public parsert
{
public:
ansi_c_parse_treet parse_tree;
-
+
ansi_c_parsert():
cpp98(false), cpp11(false),
for_has_scope(false)
{
}
-
+
virtual bool parse() override
{
return yyansi_cparse()!=0;
}
- virtual void clear() override
+ virtual void clear() override
{
parsert::clear();
parse_tree.clear();
-
+
// scanner state
tag_following=false;
asm_block_following=false;
parenthesis_counter=0;
string_literal.clear();
pragma_pack.clear();
-
+
// setup global scope
scopes.clear();
scopes.push_back(scopet());
@@ -67,33 +67,33 @@ class ansi_c_parsert:public parsert
typedef configt::ansi_ct::flavourt modet;
modet mode;
- // recognize C++98 and C++11 keywords
+ // recognize C++98 and C++11 keywords
bool cpp98, cpp11;
-
+
// in C99 and upwards, for(;;) has a scope
bool for_has_scope;
- typedef ansi_c_identifiert identifiert;
+ typedef ansi_c_identifiert identifiert;
typedef ansi_c_scopet scopet;
typedef std::list scopest;
scopest scopes;
-
+
scopet &root_scope()
{
return scopes.front();
}
-
+
const scopet &root_scope() const
{
return scopes.front();
}
-
+
void pop_scope()
{
scopes.pop_back();
}
-
+
scopet ¤t_scope()
{
assert(!scopes.empty());
@@ -113,7 +113,7 @@ class ansi_c_parsert:public parsert
assert(declaration.id()==ID_declaration);
parse_tree.items.push_back(declaration);
}
-
+
void new_scope(const std::string &prefix)
{
const scopet ¤t=current_scope();
@@ -128,7 +128,7 @@ class ansi_c_parsert:public parsert
bool label);
static ansi_c_id_classt get_class(const typet &type);
-
+
irep_idt lookup_label(const irep_idt base_name)
{
irep_idt identifier;
diff --git a/src/ansi-c/ansi_c_scope.cpp b/src/ansi-c/ansi_c_scope.cpp
index 4807916f4a6..8c2bcc4e589 100644
--- a/src/ansi-c/ansi_c_scope.cpp
+++ b/src/ansi-c/ansi_c_scope.cpp
@@ -36,4 +36,3 @@ void ansi_c_scopet::print(std::ostream &out) const
<< "\n";
}
}
-
diff --git a/src/ansi-c/ansi_c_scope.h b/src/ansi-c/ansi_c_scope.h
index 7bd953dca9e..b95cdcb06f7 100644
--- a/src/ansi-c/ansi_c_scope.h
+++ b/src/ansi-c/ansi_c_scope.h
@@ -20,12 +20,12 @@ class ansi_c_identifiert
public:
ansi_c_id_classt id_class;
irep_idt base_name, prefixed_name;
-
+
ansi_c_identifiert():id_class(ANSI_C_UNKNOWN)
{
}
};
-
+
class ansi_c_scopet
{
public:
@@ -33,19 +33,19 @@ class ansi_c_scopet
// ansi_c_identifiert.
typedef hash_map_cont name_mapt;
name_mapt name_map;
-
+
std::string prefix;
-
+
// We remember the last declarator for the benefit
// of function argument scoping.
irep_idt last_declarator;
-
+
// for(;;) and { } scopes are numbered
unsigned compound_counter;
unsigned anon_counter;
-
+
ansi_c_scopet():compound_counter(0), anon_counter(0) { }
-
+
void swap(ansi_c_scopet &scope)
{
name_map.swap(scope.name_map);
@@ -53,7 +53,7 @@ class ansi_c_scopet
last_declarator.swap(scope.last_declarator);
std::swap(compound_counter, scope.compound_counter);
}
-
+
void print(std::ostream &out) const;
};
diff --git a/src/ansi-c/ansi_c_typecheck.cpp b/src/ansi-c/ansi_c_typecheck.cpp
index 5abe39acef5..53daf912dc2 100644
--- a/src/ansi-c/ansi_c_typecheck.cpp
+++ b/src/ansi-c/ansi_c_typecheck.cpp
@@ -97,6 +97,6 @@ bool ansi_c_typecheck(
{
ansi_c_typecheck.error() << e << messaget::eom;
}
-
+
return ansi_c_typecheck.get_error_found();
}
diff --git a/src/ansi-c/c_preprocess.cpp b/src/ansi-c/c_preprocess.cpp
index 28523fff96c..0177d5950eb 100644
--- a/src/ansi-c/c_preprocess.cpp
+++ b/src/ansi-c/c_preprocess.cpp
@@ -46,7 +46,7 @@ Author: Daniel Kroening, kroening@kroening.com
" -D__INTMAX_TYPE__=\"long long int\""\
" -D__UINTMAX_TYPE__=\"long long unsigned int\""\
" -D__INTPTR_TYPE__=\"int\""\
- " -D__UINTPTR_TYPE__=\"unsigned int\""
+ " -D__UINTPTR_TYPE__=\"unsigned int\""
#define GCC_DEFINES_32 \
" -D__INT_MAX__=2147483647"\
@@ -61,8 +61,8 @@ Author: Daniel Kroening, kroening@kroening.com
" -D__INTMAX_TYPE__=\"long long int\""\
" -D__UINTMAX_TYPE__=\"long long unsigned int\""\
" -D__INTPTR_TYPE__=\"long int\""\
- " -D__UINTPTR_TYPE__=\"long unsigned int\""
-
+ " -D__UINTPTR_TYPE__=\"long unsigned int\""
+
#define GCC_DEFINES_LP64 \
" -D__INT_MAX__=2147483647"\
" -D__CHAR_BIT__=8"\
@@ -76,7 +76,7 @@ Author: Daniel Kroening, kroening@kroening.com
" -D__INTMAX_TYPE__=\"long int\""\
" -D__UINTMAX_TYPE__=\"long unsigned int\""\
" -D__INTPTR_TYPE__=\"long int\""\
- " -D__UINTPTR_TYPE__=\"long unsigned int\""
+ " -D__UINTPTR_TYPE__=\"long unsigned int\""
#define GCC_DEFINES_LLP64 \
" -D__INT_MAX__=2147483647"\
@@ -91,7 +91,7 @@ Author: Daniel Kroening, kroening@kroening.com
" -D__INTMAX_TYPE__=\"long long int\""\
" -D__UINTMAX_TYPE__=\"long long unsigned int\""\
" -D__INTPTR_TYPE__=\"long long int\""\
- " -D__UINTPTR_TYPE__=\"long long unsigned int\""
+ " -D__UINTPTR_TYPE__=\"long long unsigned int\""
/*******************************************************************\
@@ -133,7 +133,7 @@ static std::string shell_quote(const std::string &src)
{
#ifdef _WIN32
// first check if quoting is needed at all
-
+
if(src.find(' ')==std::string::npos &&
src.find('"')==std::string::npos &&
src.find('&')==std::string::npos &&
@@ -147,9 +147,9 @@ static std::string shell_quote(const std::string &src)
// seems fine -- return as is
return src;
}
-
+
std::string result;
-
+
result+='"';
for(unsigned i=0; i::const_iterator
it=config.ansi_c.defines.begin();
it!=config.ansi_c.defines.end();
@@ -542,9 +542,9 @@ bool c_preprocess_visual_studio(
// (this is already in UTF-8).
command_file << shell_quote(file) << "\n";
}
-
+
std::string tmpi=get_temporary_file("tmp.cl", "");
-
+
std::string command="CL @\""+command_file_name+"\"";
command+=" > \""+tmpi+"\"";
command+=" 2> \""+stderr_file+"\"";
@@ -615,13 +615,13 @@ void postprocess_codewarrior(
// /* #line 1 "__ppc_eabi_init.cpp" /* stack depth 0 */
//
// We remove the initial '/* ' prefix
-
+
std::string line;
-
+
while(instream)
{
std::getline(instream, line);
-
+
if(line.size()>=2 &&
line[0]=='#' && (line[1]=='#' || line[1]==' ' || line[1]=='\t'))
{
@@ -664,7 +664,7 @@ bool c_preprocess_codewarrior(
std::string stderr_file=get_temporary_file("tmp.stderr", "");
std::string command;
-
+
command="mwcceppc -E -P -D__CPROVER__ -ppopt line -ppopt full";
for(std::list::const_iterator
@@ -690,7 +690,7 @@ bool c_preprocess_codewarrior(
it!=config.ansi_c.preprocessor_options.end();
it++)
command+=" "+*it;
-
+
int result;
std::string tmpi=get_temporary_file("tmp.cl", "");
@@ -761,16 +761,16 @@ bool c_preprocess_gcc_clang(
std::string stderr_file=get_temporary_file("tmp.stderr", "");
std::string command;
-
+
if(preprocessor==configt::ansi_ct::preprocessort::CLANG)
command="clang";
else
command="gcc";
-
+
command +=" -E -undef -D__CPROVER__";
command+=" -D__WORDSIZE="+i2string(config.ansi_c.pointer_width);
-
+
command+=" -D__DBL_MIN_EXP__=\"(-1021)\"";
command+=" -D__FLT_MIN__=1.17549435e-38F";
command+=" -D__DEC64_SUBNORMAL_MIN__=0.000000000000001E-383DD";
@@ -876,13 +876,13 @@ bool c_preprocess_gcc_clang(
else
command+=GCC_DEFINES_32;
}
-
+
// The width of wchar_t depends on the OS!
{
command+=" -D__WCHAR_MAX__="+type_max(wchar_t_type());
-
+
std::string sig=config.ansi_c.wchar_t_is_unsigned?"unsigned":"signed";
-
+
if(config.ansi_c.wchar_t_width==config.ansi_c.short_int_width)
command+=" -D__WCHAR_TYPE__=\""+sig+" short int\"";
else if(config.ansi_c.wchar_t_width==config.ansi_c.int_width)
@@ -928,11 +928,11 @@ bool c_preprocess_gcc_clang(
case configt::ansi_ct::ost::NO_OS:
command+=" -nostdinc"; // make sure we don't mess with the system library
break;
-
+
default:
assert(false);
}
-
+
// Standard Defines, ANSI9899 6.10.8
switch(config.ansi_c.c_standard)
{
@@ -951,7 +951,7 @@ bool c_preprocess_gcc_clang(
command += " -D __STDC_IEC_559__=1";
command += " -D __STDC_IEC_559_COMPLEX__=1";
command += " -D __STDC_ISO_10646__=1";
-
+
for(std::list::const_iterator
it=config.ansi_c.defines.begin();
it!=config.ansi_c.defines.end();
@@ -975,10 +975,10 @@ bool c_preprocess_gcc_clang(
it!=config.ansi_c.preprocessor_options.end();
it++)
command+=" "+*it;
-
+
int result;
- #if 0
+ #if 0
// the following forces the mode
switch(config.ansi_c.mode)
{
@@ -1087,9 +1087,9 @@ bool c_preprocess_arm(
std::string stderr_file=get_temporary_file("tmp.stderr", "");
std::string command;
-
+
command="armcc -E -D__CPROVER__";
-
+
// command+=" -D__sizeof_int="+i2string(config.ansi_c.int_width/8);
// command+=" -D__sizeof_long="+i2string(config.ansi_c.long_int_width/8);
// command+=" -D__sizeof_ptr="+i2string(config.ansi_c.pointer_width/8);
@@ -1104,7 +1104,7 @@ bool c_preprocess_arm(
// if(config.ansi_c.char_is_unsigned)
// command+=" -D__CHAR_UNSIGNED__";
-
+
if(config.ansi_c.os!=configt::ansi_ct::ost::OS_WIN)
{
command+=" -D__WORDSIZE="+i2string(config.ansi_c.pointer_width);
@@ -1116,7 +1116,7 @@ bool c_preprocess_arm(
else if(config.ansi_c.int_width==64)
command+=GCC_DEFINES_LP64;
}
-
+
// Standard Defines, ANSI9899 6.10.8
command+=" -D__STDC__";
//command+=" -D__STDC_VERSION__=199901L";
@@ -1224,14 +1224,14 @@ bool c_preprocess_none(
#else
std::ifstream infile(file);
#endif
-
+
if(!infile)
{
messaget message(message_handler);
message.error() << "failed to open `" << file << "'" << messaget::eom;
return true;
}
-
+
if(config.ansi_c.mode==configt::ansi_ct::flavourt::CODEWARRIOR)
{
// special treatment for "/* #line"
@@ -1269,6 +1269,6 @@ bool test_c_preprocessor(message_handlert &message_handler)
{
std::ostringstream out;
std::istringstream in(c_test_program);
-
+
return c_preprocess(in, out, message_handler);
}
diff --git a/src/ansi-c/c_preprocess.h b/src/ansi-c/c_preprocess.h
index a9f4cb2d83e..37b6bfa83c1 100644
--- a/src/ansi-c/c_preprocess.h
+++ b/src/ansi-c/c_preprocess.h
@@ -18,7 +18,7 @@ bool c_preprocess(
const std::string &path,
std::ostream &outstream,
message_handlert &message_handler);
-
+
bool c_preprocess(
std::istream &instream,
std::ostream &outstream,
@@ -26,5 +26,5 @@ bool c_preprocess(
// returns 'true' in case of error
bool test_c_preprocessor(message_handlert &message_handler);
-
+
#endif
diff --git a/src/ansi-c/c_qualifiers.cpp b/src/ansi-c/c_qualifiers.cpp
index 2602565810c..75ca8bf9c05 100644
--- a/src/ansi-c/c_qualifiers.cpp
+++ b/src/ansi-c/c_qualifiers.cpp
@@ -25,7 +25,7 @@ Function: c_qualifierst::as_string
std::string c_qualifierst::as_string() const
{
std::string qualifiers;
-
+
if(is_constant)
qualifiers+="const ";
@@ -34,19 +34,19 @@ std::string c_qualifierst::as_string() const
if(is_restricted)
qualifiers+="restrict ";
-
+
if(is_atomic)
qualifiers+="_Atomic ";
-
+
if(is_ptr32)
qualifiers+="__ptr32 ";
-
+
if(is_ptr64)
qualifiers+="__ptr64 ";
if(is_noreturn)
qualifiers+="_Noreturn ";
-
+
return qualifiers;
}
@@ -185,4 +185,3 @@ std::ostream &operator << (
{
return out << c_qualifiers.as_string();
}
-
diff --git a/src/ansi-c/c_qualifiers.h b/src/ansi-c/c_qualifiers.h
index 006b3f481df..f676d12b2b7 100644
--- a/src/ansi-c/c_qualifiers.h
+++ b/src/ansi-c/c_qualifiers.h
@@ -20,13 +20,13 @@ class c_qualifierst
{
clear();
}
-
+
explicit c_qualifierst(const typet &src)
{
clear();
read(src);
}
-
+
void clear()
{
is_constant=false;
@@ -40,21 +40,21 @@ class c_qualifierst
// standard ones
bool is_constant, is_volatile, is_restricted, is_atomic, is_noreturn;
-
+
// MS Visual Studio extension
bool is_ptr32, is_ptr64;
-
+
// gcc extension
bool is_transparent_union;
-
+
// will likely add alignment here as well
-
+
std::string as_string() const;
void read(const typet &src);
void write(typet &src) const;
-
+
static void clear(typet &dest);
-
+
bool is_subset_of(const c_qualifierst &q) const
{
return (!is_constant || q.is_constant) &&
@@ -67,7 +67,7 @@ class c_qualifierst
// is_transparent_union isn't checked
}
-
+
friend bool operator == (
const c_qualifierst &a,
const c_qualifierst &b)
@@ -88,7 +88,7 @@ class c_qualifierst
{
return !(a==b);
}
-
+
c_qualifierst &operator += (
const c_qualifierst &b)
{
@@ -102,7 +102,7 @@ class c_qualifierst
is_noreturn|=b.is_noreturn;
return *this;
}
-
+
friend unsigned count(const c_qualifierst &q)
{
return q.is_constant+q.is_volatile+q.is_restricted+q.is_atomic+
diff --git a/src/ansi-c/c_sizeof.cpp b/src/ansi-c/c_sizeof.cpp
index c39c7e2080e..4de0d9dd22b 100644
--- a/src/ansi-c/c_sizeof.cpp
+++ b/src/ansi-c/c_sizeof.cpp
@@ -32,7 +32,7 @@ exprt c_sizeoft::sizeof_rec(const typet &type)
// this implementation will eventually be replaced
// by size_of_expr in util/pointer_offset_size.h
exprt dest;
-
+
if(type.id()==ID_signedbv ||
type.id()==ID_unsignedbv ||
type.id()==ID_floatbv ||
@@ -66,7 +66,7 @@ exprt c_sizeoft::sizeof_rec(const typet &type)
// the following is an MS extension
if(type.get_bool(ID_C_ptr32))
return from_integer(4, size_type());
-
+
std::size_t bits=config.ansi_c.pointer_width;
std::size_t bytes=bits/8;
if((bits%8)!=0) bytes++;
@@ -82,7 +82,7 @@ exprt c_sizeoft::sizeof_rec(const typet &type)
{
const exprt &size_expr=
to_array_type(type).size();
-
+
if(size_expr.is_nil())
{
// treated like an empty array
@@ -119,7 +119,7 @@ exprt c_sizeoft::sizeof_rec(const typet &type)
to_struct_type(type).components();
dest=from_integer(0, size_type());
-
+
mp_integer bit_field_width=0;
for(struct_typet::componentst::const_iterator
@@ -151,7 +151,7 @@ exprt c_sizeoft::sizeof_rec(const typet &type)
dest=plus_exprt(dest, tmp);
}
}
-
+
if(bit_field_width!=0)
dest=plus_exprt(dest, from_integer(bit_field_width/8, size_type()));
}
@@ -159,7 +159,7 @@ exprt c_sizeoft::sizeof_rec(const typet &type)
{
// the empty union will have size 0
exprt max_size=from_integer(0, size_type());
-
+
const union_typet::componentst &components=
to_union_type(type).components();
@@ -172,7 +172,7 @@ exprt c_sizeoft::sizeof_rec(const typet &type)
continue;
const typet &sub_type=it->type();
-
+
exprt tmp;
if(sub_type.id()==ID_c_bit_field)
@@ -212,7 +212,7 @@ exprt c_sizeoft::sizeof_rec(const typet &type)
// simply multiply
const exprt &size_expr=
to_vector_type(type).size();
-
+
exprt tmp_dest=sizeof_rec(type.subtype());
if(tmp_dest.is_nil())
@@ -258,7 +258,7 @@ exprt c_sizeoft::sizeof_rec(const typet &type)
// meaningful size.
dest.make_nil();
}
-
+
return dest;
}
@@ -282,7 +282,7 @@ exprt c_sizeoft::c_offsetof(
type.components();
exprt dest=from_integer(0, size_type());
-
+
mp_integer bit_field_width=0;
for(struct_typet::componentst::const_iterator
@@ -297,10 +297,10 @@ exprt c_sizeoft::c_offsetof(
dest=plus_exprt(dest, from_integer(bit_field_width/8, size_type()));
return dest;
}
-
+
if(it->get_bool(ID_is_type))
continue;
-
+
const typet &sub_type=ns.follow(it->type());
if(sub_type.id()==ID_code)
@@ -369,4 +369,3 @@ exprt c_offsetof(
simplify(tmp, ns);
return tmp;
}
-
diff --git a/src/ansi-c/c_sizeof.h b/src/ansi-c/c_sizeof.h
index b4ebc041951..2ec8508f928 100644
--- a/src/ansi-c/c_sizeof.h
+++ b/src/ansi-c/c_sizeof.h
@@ -15,7 +15,7 @@ class c_sizeoft
c_sizeoft(const namespacet &_ns):ns(_ns)
{
}
-
+
virtual ~c_sizeoft()
{
}
diff --git a/src/ansi-c/c_storage_spec.h b/src/ansi-c/c_storage_spec.h
index 05a4941b0af..b4a28c117c9 100644
--- a/src/ansi-c/c_storage_spec.h
+++ b/src/ansi-c/c_storage_spec.h
@@ -18,13 +18,13 @@ class c_storage_spect
{
clear();
}
-
+
explicit c_storage_spect(const typet &type)
{
clear();
read(type);
}
-
+
void clear()
{
is_typedef=false;
@@ -38,7 +38,7 @@ class c_storage_spect
asm_label.clear();
section.clear();
}
-
+
bool is_typedef, is_extern, is_static, is_register,
is_inline, is_thread_local, is_weak;
@@ -48,7 +48,7 @@ class c_storage_spect
// GCC asm labels __asm__("foo") - these change the symbol name
irep_idt asm_label;
irep_idt section;
-
+
friend bool operator == (
const c_storage_spect &a,
const c_storage_spect &b)
@@ -83,10 +83,10 @@ class c_storage_spect
a.is_inline |=b.is_inline;
a.is_thread_local |=b.is_thread_local;
// attributes belong to the declarator, don't replace them
-
+
return a;
}
-
+
void read(const typet &type);
};
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index 6e8f432711e..43bbbc7c7bb 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/src/ansi-c/c_typecast.cpp
@@ -106,7 +106,7 @@ bool is_void_pointer(const typet &type)
{
if(type.subtype().id()==ID_empty)
return true;
-
+
return is_void_pointer(type.subtype());
}
else
@@ -129,7 +129,7 @@ bool check_c_implicit_typecast(
const typet &src_type,
const typet &dest_type)
{
- // check qualifiers
+ // check qualifiers
if(src_type.id()==ID_pointer && dest_type.id()==ID_pointer &&
src_type.subtype().get_bool(ID_C_constant) &&
@@ -137,7 +137,7 @@ bool check_c_implicit_typecast(
return true;
if(src_type==dest_type) return false;
-
+
const irep_idt &src_type_id=src_type.id();
if(src_type_id==ID_c_bit_field)
@@ -251,7 +251,7 @@ bool check_c_implicit_typecast(
// imaginary part of the complex value is discarded and the value of the
// real part is converted according to the conversion rules for the
// corresponding real type.
-
+
return check_c_implicit_typecast(src_type.subtype(), dest_type);
}
}
@@ -269,7 +269,7 @@ bool check_c_implicit_typecast(
is_void_pointer(dest_type)) // to void from anything
return false;
}
-
+
if(dest_type.id()==ID_array &&
src_type.subtype()==dest_type.subtype()) return false;
@@ -312,12 +312,12 @@ Function: c_typecastt::follow_with_qualifiers
typet c_typecastt::follow_with_qualifiers(const typet &src_type)
{
if(src_type.id()!=ID_symbol) return src_type;
-
+
typet result_type=src_type;
-
+
// collect qualifiers
c_qualifierst qualifiers(src_type);
-
+
while(result_type.id()==ID_symbol)
{
const symbolt &followed_type_symbol=
@@ -422,8 +422,8 @@ c_typecastt::c_typet c_typecastt::get_c_type(
return COMPLEX;
else if(type.id()==ID_c_bit_field)
return get_c_type(to_c_bit_field_type(type).subtype());
-
- return OTHER;
+
+ return OTHER;
}
/*******************************************************************\
@@ -443,9 +443,9 @@ void c_typecastt::implicit_typecast_arithmetic(
c_typet c_type)
{
typet new_type;
-
+
const typet &expr_type=ns.follow(expr.type());
-
+
switch(c_type)
{
case PTR:
@@ -561,10 +561,10 @@ Function: c_typecastt::implicit_typecast
void c_typecastt::implicit_typecast(
exprt &expr,
const typet &type)
-{
+{
typet src_type=follow_with_qualifiers(expr.type()),
dest_type=follow_with_qualifiers(type);
-
+
typet type_qual=type;
c_qualifierst qualifiers(dest_type);
qualifiers.write(type_qual);
@@ -607,7 +607,7 @@ void c_typecastt::implicit_typecast_followed(
if(src_type.id()==ID_pointer &&
src_type.subtype().get_bool(ID_C_constant))
src_type_no_const.subtype().remove(ID_C_constant);
-
+
// Check union members.
const union_typet &dest_union_type=to_union_type(dest_type);
@@ -644,12 +644,12 @@ void c_typecastt::implicit_typecast_followed(
expr.set(ID_value, ID_NULL);
return; // ok
}
-
+
if(src_type.id()==ID_pointer ||
src_type.id()==ID_array)
{
// we are quite generous about pointers
-
+
const typet &src_sub=ns.follow(src_type.subtype());
const typet &dest_sub=ns.follow(dest_type.subtype());
@@ -699,7 +699,7 @@ void c_typecastt::implicit_typecast_followed(
return; // ok
}
}
-
+
if(check_c_implicit_typecast(src_type, dest_type))
errors.push_back("implicit conversion not permitted");
else if(src_type!=dest_type)
@@ -735,7 +735,7 @@ void c_typecastt::implicit_typecast_arithmetic(
// get the biggest width of both
unsigned width1=type1.get_int(ID_width);
unsigned width2=type2.get_int(ID_width);
-
+
// produce type
typet result_type;
@@ -753,7 +753,7 @@ void c_typecastt::implicit_typecast_arithmetic(
do_typecast(expr1, result_type);
do_typecast(expr2, result_type);
-
+
return;
}
else if(max_type==COMPLEX)
@@ -801,7 +801,7 @@ void c_typecastt::implicit_typecast_arithmetic(
{
if(c_type1==VOIDPTR)
do_typecast(expr1, expr2.type());
-
+
if(c_type2==VOIDPTR)
do_typecast(expr2, expr1.type());
}
@@ -824,7 +824,7 @@ void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
{
// special case: array -> pointer is actually
// something like address_of
-
+
const typet &src_type=ns.follow(expr.type());
if(src_type.id()==ID_array)
@@ -845,7 +845,7 @@ void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
// explicit comparision with zero.
// Note that this requires ieee_float_notequal
// in case of floating-point numbers.
-
+
if(dest_type.get(ID_C_c_type)==ID_bool)
{
expr=is_not_zero(expr, ns);
@@ -856,7 +856,7 @@ void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
expr=is_not_zero(expr, ns);
}
else
- {
+ {
expr.make_typecast(dest_type);
}
}
diff --git a/src/ansi-c/c_typecast.h b/src/ansi-c/c_typecast.h
index 203d00477c9..d2039237000 100644
--- a/src/ansi-c/c_typecast.h
+++ b/src/ansi-c/c_typecast.h
@@ -56,13 +56,13 @@ class c_typecastt
virtual void implicit_typecast_arithmetic(
exprt &expr1,
exprt &expr2);
-
+
std::list errors;
std::list warnings;
protected:
const namespacet &ns;
-
+
// these are in promotion order
enum c_typet { BOOL,
@@ -83,7 +83,7 @@ class c_typecastt
void implicit_typecast_arithmetic(
exprt &expr,
c_typet c_type);
-
+
typet follow_with_qualifiers(const typet &src);
// after follow_with_qualifiers
diff --git a/src/ansi-c/c_typecheck_argc_argv.cpp b/src/ansi-c/c_typecheck_argc_argv.cpp
index 5e77cbf0600..71ac609d4b3 100644
--- a/src/ansi-c/c_typecheck_argc_argv.cpp
+++ b/src/ansi-c/c_typecheck_argc_argv.cpp
@@ -40,7 +40,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
}
symbolt *argc_new_symbol;
-
+
const exprt &op0=static_cast(parameters[0]);
const exprt &op1=static_cast(parameters[1]);
@@ -83,7 +83,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
// need to add one to the size -- the array is terminated
// with NULL
exprt one_expr=from_integer(1, argc_new_symbol->type);
-
+
exprt size_expr(ID_plus, argc_new_symbol->type);
size_expr.copy_to_operands(argc_new_symbol->symbol_expr(), one_expr);
argv_type.add(ID_size).swap(size_expr);
@@ -99,21 +99,21 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
symbolt *argv_new_symbol;
move_symbol(argv_symbol, argv_new_symbol);
}
-
+
if(parameters.size()==3)
- {
- symbolt envp_symbol;
+ {
+ symbolt envp_symbol;
envp_symbol.base_name="envp'";
envp_symbol.name="envp'";
envp_symbol.type=(static_cast(parameters[2])).type();
envp_symbol.is_static_lifetime=true;
-
+
symbolt envp_size_symbol, *envp_new_size_symbol;
envp_size_symbol.base_name="envp_size";
envp_size_symbol.name="envp_size'";
envp_size_symbol.type=op0.type(); // same type as argc!
- envp_size_symbol.is_static_lifetime=true;
- move_symbol(envp_size_symbol, envp_new_size_symbol);
+ envp_size_symbol.is_static_lifetime=true;
+ move_symbol(envp_size_symbol, envp_new_size_symbol);
if(envp_symbol.type.id()!=ID_pointer)
{
@@ -122,12 +122,12 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
<< to_string(envp_symbol.type) << '\'' << eom;
throw 0;
}
-
+
exprt size_expr = envp_new_size_symbol->symbol_expr();
envp_symbol.type.id(ID_array);
envp_symbol.type.add(ID_size).swap(size_expr);
-
+
symbolt *envp_new_symbol;
move_symbol(envp_symbol, envp_new_symbol);
}
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index e055236d12f..be7c58cc197 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -30,7 +30,7 @@ Function: c_typecheck_baset::to_string
\*******************************************************************/
std::string c_typecheck_baset::to_string(const exprt &expr)
-{
+{
return expr2c(expr, *this);
}
@@ -47,7 +47,7 @@ Function: c_typecheck_baset::to_string
\*******************************************************************/
std::string c_typecheck_baset::to_string(const typet &type)
-{
+{
return type2c(type, *this);
}
@@ -96,10 +96,10 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
bool is_function=symbol.type.id()==ID_code;
const typet &final_type=follow(symbol.type);
-
+
// set a few flags
symbol.is_lvalue=!symbol.is_type && !symbol.is_macro;
-
+
irep_idt root_name=symbol.base_name;
irep_idt new_name=symbol.name;
@@ -121,7 +121,7 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
error() << "only functions can have a function body" << eom;
throw 0;
}
-
+
// set the pretty name
if(symbol.is_type &&
(final_type.id()==ID_struct ||
@@ -145,18 +145,18 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
{
symbol.pretty_name=new_name;
}
-
+
// see if we have it already
symbol_tablet::symbolst::iterator old_it=symbol_table.symbols.find(symbol.name);
-
+
if(old_it==symbol_table.symbols.end())
{
// just put into symbol_table
symbolt *new_symbol;
move_symbol(symbol, new_symbol);
-
+
typecheck_new_symbol(*new_symbol);
- }
+ }
else
{
if(old_it->second.is_type!=symbol.is_type)
@@ -221,13 +221,13 @@ void c_typecheck_baset::typecheck_new_symbol(symbolt &symbol)
type_symbolt new_symbol(symbol.type);
new_symbol.name=id2string(symbol.name)+"$type";
- new_symbol.base_name=id2string(symbol.base_name)+"$type";
+ new_symbol.base_name=id2string(symbol.base_name)+"$type";
new_symbol.location=symbol.location;
new_symbol.mode=symbol.mode;
new_symbol.module=symbol.module;
-
+
symbol.type=symbol_typet(new_symbol.name);
-
+
symbolt *new_sp;
symbol_table.move(new_symbol, new_sp);
}
@@ -266,7 +266,7 @@ void c_typecheck_baset::typecheck_redefinition_type(
{
// overwrite location
old_symbol.location=new_symbol.location;
-
+
// move body
old_symbol.type.swap(new_symbol.type);
}
@@ -290,7 +290,7 @@ void c_typecheck_baset::typecheck_redefinition_type(
{
if("incomplete_"+final_old.id_string()==final_new.id_string())
{
- // just ignore silently
+ // just ignore silently
}
else
{
@@ -303,8 +303,8 @@ void c_typecheck_baset::typecheck_redefinition_type(
}
}
else if(config.ansi_c.os==configt::ansi_ct::ost::OS_WIN &&
- final_new.id()==ID_c_enum && final_old.id()==ID_c_enum)
- {
+ final_new.id()==ID_c_enum && final_old.id()==ID_c_enum)
+ {
// under Windows, ignore this silently;
// MSC doesn't think this is a problem, but GCC complains.
}
@@ -365,9 +365,9 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
if(follow(new_symbol.type).id()!=ID_code &&
!new_symbol.is_macro)
do_initializer(new_symbol);
-
+
const typet &final_new=follow(new_symbol.type);
-
+
// K&R stuff?
if(old_symbol.type.id()==ID_KnR)
{
@@ -379,18 +379,18 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
<< eom;
throw 0;
}
-
+
// fix up old symbol -- we now got the type
old_symbol.type=new_symbol.type;
return;
}
-
+
if(final_new.id()==ID_code)
{
bool inlined=
(new_symbol.type.get_bool(ID_C_inlined) ||
old_symbol.type.get_bool(ID_C_inlined));
-
+
if(final_old.id()!=ID_code)
{
error().source_location=new_symbol.location;
@@ -404,7 +404,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
code_typet &old_ct=to_code_type(old_symbol.type);
code_typet &new_ct=to_code_type(new_symbol.type);
-
+
if(old_ct.has_ellipsis() && !new_ct.has_ellipsis())
old_ct=new_ct;
else if(!old_ct.has_ellipsis() && new_ct.has_ellipsis())
@@ -417,14 +417,14 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
}
// do body
-
+
if(new_symbol.value.is_not_nil())
- {
+ {
if(old_symbol.value.is_not_nil())
{
// gcc allows re-definition if the first
// definition is marked as "extern inline"
-
+
if(old_symbol.type.get_bool(ID_C_inlined) &&
(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC ||
config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE ||
@@ -473,10 +473,10 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
old_symbol.is_macro=true;
else
typecheck_function_body(new_symbol);
-
+
// overwrite location
old_symbol.location=new_symbol.location;
-
+
// move body
old_symbol.value.swap(new_symbol.value);
@@ -503,7 +503,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
to_symbol_type(old_symbol.type).get_identifier();
symbol_tablet::symbolst::iterator s_it=symbol_table.symbols.find(identifier);
-
+
if(s_it==symbol_table.symbols.end())
{
error().source_location=old_symbol.location;
@@ -512,10 +512,10 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
<< eom;
throw 0;
}
-
+
symbolt &symbol=s_it->second;
-
- symbol.type=final_new;
+
+ symbol.type=final_new;
}
else
old_symbol.type=new_symbol.type;
@@ -533,7 +533,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
final_new.id()==ID_pointer &&
follow(final_new).subtype().id()==ID_code)
{
- // to allow
+ // to allow
// int (*f) ();
// int (*f) (int)=0;
old_symbol.type=new_symbol.type;
@@ -544,7 +544,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
follow(final_new).subtype().id()==ID_code &&
to_code_type(follow(final_new).subtype()).has_ellipsis())
{
- // to allow
+ // to allow
// int (*f) (int)=0;
// int (*f) ();
}
@@ -603,13 +603,13 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
old_symbol.is_macro=new_symbol.is_macro;
}
}
-
+
// take care of some flags
if(old_symbol.is_extern && !new_symbol.is_extern)
old_symbol.location=new_symbol.location;
old_symbol.is_extern=old_symbol.is_extern && new_symbol.is_extern;
-
+
// We should likely check is_volatile and
// is_thread_local for consistency. GCC complains if these
// mismatch.
@@ -630,21 +630,21 @@ Function: c_typecheck_baset::typecheck_function_body
void c_typecheck_baset::typecheck_function_body(symbolt &symbol)
{
code_typet &code_type=to_code_type(symbol.type);
-
+
assert(symbol.value.is_not_nil());
-
+
// reset labels
labels_used.clear();
labels_defined.clear();
// fix type
symbol.value.type()=code_type;
-
+
// set return type
return_type=code_type.return_type();
-
+
unsigned anon_counter=0;
-
+
// Add the parameter declarations into the symbol table.
code_typet::parameterst ¶meters=code_type.parameters();
for(code_typet::parameterst::iterator
@@ -658,7 +658,7 @@ void c_typecheck_baset::typecheck_function_body(symbolt &symbol)
irep_idt base_name="#anon"+i2string(anon_counter++);
p_it->set_base_name(base_name);
}
-
+
// produce identifier
irep_idt base_name=p_it->get_base_name();
irep_idt identifier=id2string(symbol.name)+"::"+id2string(base_name);
@@ -666,7 +666,7 @@ void c_typecheck_baset::typecheck_function_body(symbolt &symbol)
p_it->set_identifier(identifier);
parameter_symbolt p_symbol;
-
+
p_symbol.type=p_it->type();
p_symbol.name=identifier;
p_symbol.base_name=base_name;
@@ -676,10 +676,10 @@ void c_typecheck_baset::typecheck_function_body(symbolt &symbol)
move_symbol(p_symbol, new_p_symbol);
}
- // typecheck the body code
+ // typecheck the body code
typecheck_code(to_code(symbol.value));
- // special case for main()
+ // special case for main()
if(symbol.name==ID_main)
add_argc_argv(symbol);
@@ -805,7 +805,7 @@ void c_typecheck_baset::typecheck_declaration(
// first typecheck the type of the declaration
typecheck_type(declaration.type());
-
+
// mark as 'already typechecked'
make_already_typechecked(declaration.type());
@@ -906,4 +906,3 @@ void c_typecheck_baset::typecheck_declaration(
}
}
}
-
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
index 32bb18633ca..eb2d6e66c3a 100644
--- a/src/ansi-c/c_typecheck_base.h
+++ b/src/ansi-c/c_typecheck_base.h
@@ -62,11 +62,11 @@ class c_typecheck_baset:
typedef hash_map_cont id_type_mapt;
id_type_mapt parameter_map;
-
+
// overload to use language specific syntax
virtual std::string to_string(const exprt &expr);
virtual std::string to_string(const typet &type);
-
+
//
// service functions
//
@@ -91,13 +91,13 @@ class c_typecheck_baset:
designatort &designator,
const exprt &value,
bool force_constant);
-
+
designatort make_designator(const typet &type, const exprt &src);
void designator_enter(const typet &type, designatort &designator); // go down
void increment_designator(designatort &designator);
// typecasts
-
+
bool gcc_vector_types_compatible(const vector_typet &, const vector_typet &);
virtual void implicit_typecast(exprt &expr, const typet &type);
@@ -108,7 +108,7 @@ class c_typecheck_baset:
{
implicit_typecast(expr, bool_typet());
}
-
+
// code
virtual void start_typecheck_code();
virtual void typecheck_code(codet &code);
@@ -134,16 +134,16 @@ class c_typecheck_baset:
virtual void typecheck_dowhile(code_dowhilet &code);
virtual void typecheck_start_thread(codet &code);
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec);
-
+
bool break_is_allowed;
bool continue_is_allowed;
bool case_is_allowed;
typet switch_op_type;
typet return_type;
-
+
// to check that all labels used are also defined
std::map labels_defined, labels_used;
-
+
// expressions
virtual void typecheck_expr_builtin_va_arg(exprt &expr);
virtual void typecheck_expr_builtin_offsetof(exprt &expr);
@@ -186,9 +186,9 @@ class c_typecheck_baset:
virtual void make_constant(exprt &expr);
virtual void make_constant_index(exprt &expr);
virtual void make_constant_rec(exprt &expr);
-
+
virtual bool gcc_types_compatible_p(const typet &, const typet &);
-
+
// types
virtual void typecheck_type(typet &type);
virtual void typecheck_compound_type(struct_union_typet &type);
@@ -204,14 +204,14 @@ class c_typecheck_baset:
virtual void typecheck_custom_type(typet &type);
virtual void adjust_function_parameter(typet &type) const;
virtual bool is_complete_type(const typet &type) const;
-
+
typet enum_constant_type(
const mp_integer &min, const mp_integer &max) const;
-
+
typet enum_underlying_type(
const mp_integer &min, const mp_integer &max,
bool is_packed) const;
-
+
void make_already_typechecked(typet &dest)
{
typet result(ID_already_typechecked);
@@ -229,7 +229,7 @@ class c_typecheck_baset:
void move_symbol(symbolt &symbol, symbolt *&new_symbol);
void move_symbol(symbolt &symbol)
{ symbolt *new_symbol; move_symbol(symbol, new_symbol); }
-
+
// top-level stuff
void typecheck_declaration(ansi_c_declarationt &);
void typecheck_symbol(symbolt &symbol);
@@ -239,14 +239,14 @@ class c_typecheck_baset:
void typecheck_function_body(symbolt &symbol);
virtual void do_initializer(symbolt &symbol);
-
+
inline static bool is_numeric_type(const typet &src)
{
return src.id()==ID_complex ||
src.id()==ID_unsignedbv ||
src.id()==ID_signedbv ||
- src.id()==ID_floatbv ||
- src.id()==ID_fixedbv ||
+ src.id()==ID_floatbv ||
+ src.id()==ID_fixedbv ||
src.id()==ID_c_bool ||
src.id()==ID_bool ||
src.id()==ID_c_enum_tag ||
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index 5b8fd61d325..77f3bf3ba50 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -167,22 +167,22 @@ Function: c_typecheck_baset::typecheck_asm
void c_typecheck_baset::typecheck_asm(codet &code)
{
const irep_idt flavor=to_code_asm(code).get_flavor();
-
+
if(flavor==ID_gcc)
{
// These have 5 operands.
// The first parameter is a string.
// Parameters 1, 2, 3, 4 are lists of expressions.
-
+
// Parameter 1: OutputOperands
// Parameter 2: InputOperands
// Parameter 3: Clobbers
// Parameter 4: GotoLabels
assert(code.operands().size()==5);
-
+
typecheck_expr(code.op0());
-
+
for(unsigned i=1; iis_nil()) continue;
codet &code_op=to_code(*it1);
-
+
if(code_op.get_statement()==ID_label)
{
// these may be nested
codet *code_ptr=&code_op;
-
+
while(code_ptr->get_statement()==ID_label)
{
assert(code_ptr->operands().size()==1);
code_ptr=&to_code(code_ptr->op0());
}
-
+
//codet &label_op=*code_ptr;
new_ops.move_to_operands(code_op);
@@ -352,7 +352,7 @@ void c_typecheck_baset::typecheck_decl(codet &code)
ansi_c_declarationt declaration;
declaration.swap(code.op0());
-
+
if(declaration.get_is_static_assert())
{
assert(declaration.operands().size()==2);
@@ -363,13 +363,13 @@ void c_typecheck_baset::typecheck_decl(codet &code)
typecheck_code(code);
return; // done
}
-
+
typecheck_declaration(declaration);
-
+
std::list new_code;
-
+
// iterate over declarators
-
+
for(ansi_c_declarationt::declaratorst::const_iterator
d_it=declaration.declarators().begin();
d_it!=declaration.declarators().end();
@@ -390,8 +390,8 @@ void c_typecheck_baset::typecheck_decl(codet &code)
}
symbolt &symbol=s_it->second;
-
- // This must not be an incomplete type, unless it's 'extern'
+
+ // This must not be an incomplete type, unless it's 'extern'
// or a typedef.
if(!symbol.is_type &&
!symbol.is_extern &&
@@ -401,7 +401,7 @@ void c_typecheck_baset::typecheck_decl(codet &code)
error() << "incomplete type not permitted here" << eom;
throw 0;
}
-
+
// see if it's a typedef
// or a function
// or static
@@ -417,21 +417,21 @@ void c_typecheck_baset::typecheck_decl(codet &code)
code.add_source_location()=symbol.location;
code.symbol()=symbol.symbol_expr();
code.symbol().add_source_location()=symbol.location;
-
+
// add initializer, if any
if(symbol.value.is_not_nil())
{
code.operands().resize(2);
- code.op1()=symbol.value;
+ code.op1()=symbol.value;
}
-
+
new_code.push_back(code);
}
}
-
+
// stash away any side-effects in the declaration
new_code.splice(new_code.begin(), clean_code);
-
+
if(new_code.empty())
{
source_locationt source_location=code.source_location();
@@ -488,7 +488,7 @@ bool c_typecheck_baset::is_complete_type(const typet &type) const
return is_complete_type(type.subtype());
else if(type.id()==ID_symbol)
return is_complete_type(follow(type));
-
+
return true;
}
@@ -538,7 +538,7 @@ void c_typecheck_baset::typecheck_for(codet &code)
error() << "for expected to have four operands" << eom;
throw 0;
}
-
+
// the "for" statement has an implicit block around it,
// since code.op0() may contain declarations
//
@@ -677,7 +677,7 @@ void c_typecheck_baset::typecheck_switch_case(code_switch_caset &code)
error() << "did not expect `case' here" << eom;
throw 0;
}
-
+
exprt &case_expr=code.case_op();
typecheck_expr(case_expr);
implicit_typecast(case_expr, switch_op_type);
@@ -779,7 +779,7 @@ void c_typecheck_baset::typecheck_gcc_computed_goto(codet &code)
}
exprt &dest=code.op0();
-
+
if(dest.id()!=ID_dereference)
{
err_location(dest);
@@ -787,7 +787,7 @@ void c_typecheck_baset::typecheck_gcc_computed_goto(codet &code)
<< eom;
throw 0;
}
-
+
assert(dest.operands().size()==1);
typecheck_expr(dest.op0());
@@ -837,7 +837,7 @@ void c_typecheck_baset::typecheck_ifthenelse(code_ifthenelset &code)
code_block.move_to_operands(code.then_case());
code.then_case().swap(code_block);
}
-
+
typecheck_code(to_code(code.then_case()));
if(!code.else_case().is_nil())
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 884cf94d94d..94a861e7a7d 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -133,7 +133,7 @@ bool c_typecheck_baset::gcc_types_compatible_p(
// check qualifiers first
if(c_qualifierst(type1)!=c_qualifierst(type2))
return false;
-
+
if(type1.id()==ID_c_enum_tag)
return gcc_types_compatible_p(follow_tag(to_c_enum_tag_type(type1)), type2);
else if(type2.id()==ID_c_enum_tag)
@@ -190,12 +190,12 @@ bool c_typecheck_baset::gcc_types_compatible_p(
// Need to distinguish e.g. long int from int or
// long long int from long int.
// The rules appear to match those of C++.
-
+
if(type1.get(ID_C_c_type)==type2.get(ID_C_c_type))
return true;
}
}
-
+
return false;
}
@@ -283,7 +283,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
typecheck_type(subtypes[0]);
typecheck_type(subtypes[1]);
source_locationt source_location=expr.source_location();
-
+
// ignores top-level qualifiers
subtypes[0].remove(ID_C_constant);
subtypes[0].remove(ID_C_volatile);
@@ -291,7 +291,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
subtypes[1].remove(ID_C_constant);
subtypes[1].remove(ID_C_volatile);
subtypes[1].remove(ID_C_restricted);
-
+
expr.make_bool(gcc_types_compatible_p(subtypes[0], subtypes[1]));
expr.add_source_location()=source_location;
}
@@ -331,7 +331,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
// op1 the bound expression
assert(expr.operands().size()==2);
expr.type()=bool_typet();
-
+
if(expr.op0().get(ID_statement)!=ID_decl)
{
err_location(expr);
@@ -372,18 +372,18 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
throw 0;
}
- // we could compile away, I suppose
+ // we could compile away, I suppose
expr.type()=op_type;
expr.op0().make_typecast(complex_typet(op_type));
}
else
{
expr.type()=op_type.subtype();
-
+
// these are lvalues if the operand is one
if(expr.op0().get_bool(ID_C_lvalue))
expr.set(ID_C_lvalue, true);
-
+
if(expr.op0().get_bool(ID_C_constant))
expr.set(ID_C_constant, true);
}
@@ -393,7 +393,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
// This is C11.
// The operand is already typechecked. Depending
// on it's type, we return one of the generic associatios.
-
+
if(expr.operands().size()!=1)
{
err_location(expr);
@@ -409,7 +409,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
irept::subt &generic_associations=
expr.add(ID_generic_associations).get_sub();
-
+
// first typecheck all types
Forall_irep(it, generic_associations)
if(it->get(ID_type_arg)!=ID_default)
@@ -421,9 +421,9 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
// first try non-default match
exprt default_match=nil_exprt();
exprt assoc_match=nil_exprt();
-
+
const typet &op_type=follow(expr.op0().type());
-
+
forall_irep(it, generic_associations)
{
if(it->get(ID_type_arg)==ID_default)
@@ -431,7 +431,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
else if(op_type==follow(static_cast(it->find(ID_type_arg))))
assoc_match=static_cast(it->find(ID_value));
}
-
+
if(assoc_match.is_nil())
{
if(default_match.is_not_nil())
@@ -511,13 +511,13 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
typet arg_type=expr.type();
typecheck_type(arg_type);
-
+
code_typet new_type;
new_type.return_type().swap(arg_type);
new_type.parameters().resize(1);
new_type.parameters()[0].type()=pointer_type(void_type());
- assert(expr.operands().size()==1);
+ assert(expr.operands().size()==1);
exprt arg=expr.op0();
implicit_typecast(arg, pointer_type(void_type()));
@@ -530,21 +530,21 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
result.function().type()=new_type;
result.arguments().push_back(arg);
result.type()=new_type.return_type();
-
+
expr.swap(result);
-
+
// Make sure symbol exists, but we have it return void
// to avoid collisions of the same symbol with different
// types.
-
+
code_typet symbol_type=new_type;
symbol_type.return_type()=void_type();
-
+
symbolt symbol;
symbol.base_name=ID_gcc_builtin_va_arg;
symbol.name=ID_gcc_builtin_va_arg;
symbol.type=symbol_type;
-
+
symbol_table.move(symbol);
}
@@ -602,7 +602,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr)
typet &type=static_cast(expr.add(ID_type_arg));
typecheck_type(type);
-
+
exprt &member=static_cast