Skip to content

Commit

Permalink
Various bits of cleanup, to be broken up into sensible commits
Browse files Browse the repository at this point in the history
  • Loading branch information
tautschnig committed Jun 20, 2018
1 parent 3e14fe5 commit fb8ccf7
Show file tree
Hide file tree
Showing 57 changed files with 299 additions and 269 deletions.
5 changes: 2 additions & 3 deletions src/ansi-c/expr2c.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2218,9 +2218,8 @@ std::string expr2ct::convert_array(
break;

assert(it->is_constant());
mp_integer i;
to_integer(*it, i);
unsigned int ch=integer2unsigned(i);
const auto i = numeric_cast<mp_integer>(*it);
const unsigned int ch = numeric_cast_v<unsigned>(*i);

if(last_was_hex)
{
Expand Down
26 changes: 14 additions & 12 deletions src/ansi-c/padding.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -35,12 +35,15 @@ mp_integer alignment(const typet &type, const namespacet &ns)
const exprt &given_alignment=
static_cast<const exprt &>(type.find(ID_C_alignment));

mp_integer a_int;
mp_integer a_int = 0;

// we trust it blindly, no matter how nonsensical
if(given_alignment.is_nil() ||
to_integer(given_alignment, a_int))
a_int=0;
if(given_alignment.is_not_nil())
{
const auto a = numeric_cast<mp_integer>(given_alignment);
if(a.has_value())
a_int = *a;
}

// alignment but no packing
if(a_int>0 && !type.get_bool(ID_C_packed))
Expand Down Expand Up @@ -386,17 +389,16 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
}

// any explicit alignment for the struct?
if(type.find(ID_C_alignment).is_not_nil())
const exprt &alignment =
static_cast<const exprt &>(type.find(ID_C_alignment));
if(alignment.is_not_nil())
{
const exprt &alignment=
static_cast<const exprt &>(type.find(ID_C_alignment));
if(alignment.id()!=ID_default)
{
exprt tmp=alignment;
simplify(tmp, ns);
mp_integer tmp_i;
if(!to_integer(tmp, tmp_i) && tmp_i>max_alignment)
max_alignment=tmp_i;
const auto tmp_i = numeric_cast<mp_integer>(simplify_expr(alignment, ns));

if(tmp_i.has_value() && *tmp_i > max_alignment)
max_alignment = *tmp_i;
}
}
// Is the struct packed, without any alignment specification?
Expand Down
19 changes: 12 additions & 7 deletions src/ansi-c/type2name.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -178,14 +178,19 @@ static std::string type2name(
}
else if(type.id()==ID_array)
{
const array_typet &t=to_array_type(type);
mp_integer size;
if(t.size().id()==ID_symbol)
result += "ARR" + id2string(to_symbol_expr(t.size()).get_identifier());
else if(to_integer(t.size(), size))
result+="ARR?";
const exprt &size = to_array_type(type).size();

if(size.id()==ID_symbol)
result += "ARR" + id2string(to_symbol_expr(size).get_identifier());
else
result+="ARR"+integer2string(size);
{
const auto size_int = numeric_cast<mp_integer>(size);

if(!size_int.has_value())
result += "ARR?";
else
result += "ARR" + integer2string(*size_int);
}
}
else if(type.id()==ID_symbol ||
type.id()==ID_c_enum_tag ||
Expand Down
4 changes: 2 additions & 2 deletions src/cpp/cpp_token_buffer.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
#include <ansi-c/ansi_c_y.tab.h>
#include <ansi-c/ansi_c_parser.h>

int cpp_token_buffert::LookAhead(unsigned offset)
int cpp_token_buffert::LookAhead(std::size_t offset)
{
assert(current_pos<=token_vector.size());

Expand Down Expand Up @@ -56,7 +56,7 @@ int cpp_token_buffert::get_token()
return kind;
}

int cpp_token_buffert::LookAhead(unsigned offset, cpp_tokent &token)
int cpp_token_buffert::LookAhead(std::size_t offset, cpp_tokent &token)
{
assert(current_pos<=token_vector.size());

Expand Down
6 changes: 3 additions & 3 deletions src/cpp/cpp_token_buffer.h
Original file line number Diff line number Diff line change
Expand Up @@ -25,12 +25,12 @@ class cpp_token_buffert
{
}

typedef unsigned int post;
typedef std::size_t post;

int LookAhead(unsigned offset);
int LookAhead(std::size_t offset);
int get_token(cpp_tokent &token);
int get_token();
int LookAhead(unsigned offset, cpp_tokent &token);
int LookAhead(std::size_t offset, cpp_tokent &token);

post Save();
void Restore(post pos);
Expand Down
4 changes: 2 additions & 2 deletions src/cpp/cpp_typecheck_code.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -25,12 +25,12 @@ void cpp_typecheckt::typecheck_code(codet &code)

if(statement==ID_try_catch)
{
code.type()=code_typet();
code.type() = code_typet({}, empty_typet());
typecheck_try_catch(code);
}
else if(statement==ID_member_initializer)
{
code.type()=code_typet();
code.type() = code_typet({}, empty_typet());
typecheck_member_initializer(code);
}
else if(statement==ID_msc_if_exists ||
Expand Down
14 changes: 6 additions & 8 deletions src/cpp/cpp_typecheck_constructor.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -435,7 +435,7 @@ void cpp_typecheckt::default_assignop_value(
declarator.value().add_source_location()=source_location;
declarator.value().id(ID_code);
declarator.value().set(ID_statement, ID_block);
declarator.value().type()=code_typet();
declarator.value().type() = code_typet({}, empty_typet());

exprt &block=declarator.value();

Expand Down Expand Up @@ -482,13 +482,11 @@ void cpp_typecheckt::default_assignop_value(
continue;
}

mp_integer size;
bool to_int=to_integer(size_expr, size);
CHECK_RETURN(!to_int);
CHECK_RETURN(size>=0);
const auto size = numeric_cast<mp_integer>(size_expr);
CHECK_RETURN(!size.has_value());
CHECK_RETURN(*size >= 0);

exprt::operandst empty_operands;
for(mp_integer i=0; i < size; ++i)
for(mp_integer i = 0; i < *size; ++i)
copy_array(source_location, mem_name, i, arg_name, block);
}
else
Expand All @@ -501,7 +499,7 @@ void cpp_typecheckt::default_assignop_value(
ret_code.operands().push_back(exprt(ID_dereference));
ret_code.op0().operands().push_back(exprt("cpp-this"));
ret_code.set(ID_statement, ID_return);
ret_code.type()=code_typet();
ret_code.type() = code_typet({}, empty_typet());
}

/// Check a constructor initialization-list. An initializer has to be a data
Expand Down
8 changes: 4 additions & 4 deletions src/cpp/parse.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -5514,9 +5514,8 @@ bool Parser::rTypeNameOrFunctionType(typet &tname)
<< "Parser::rTypeNameOrFunctionType 2\n";
#endif

code_typet type;

if(!rCastOperatorName(type.return_type()))
typet return_type;
if(!rCastOperatorName(return_type))
return false;

#ifdef DEBUG
Expand All @@ -5526,7 +5525,7 @@ bool Parser::rTypeNameOrFunctionType(typet &tname)

if(lex.LookAhead(0)!='(')
{
tname.swap(type.return_type());
tname.swap(return_type);

if(!optPtrOperator(tname))
return false;
Expand All @@ -5539,6 +5538,7 @@ bool Parser::rTypeNameOrFunctionType(typet &tname)
<< "Parser::rTypeNameOrFunctionType 4\n";
#endif

code_typet type({}, return_type);
cpp_tokent op;
lex.get_token(op);

Expand Down
4 changes: 2 additions & 2 deletions src/goto-cc/linker_script_merge.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -415,7 +415,7 @@ int linker_script_merget::ls_data2instructions(


// Array symbol_exprt
std::size_t array_size=integer2size_t(string2integer(d["size"].value));
mp_integer array_size = string2integer(d["size"].value);
if(array_size > MAX_FLATTENED_ARRAY_SIZE)
{
warning() << "Object section '" << d["section"].value << "' of size "
Expand All @@ -434,7 +434,7 @@ int linker_script_merget::ls_data2instructions(
array_loc.set_file(linker_script);
std::ostringstream array_comment;
array_comment << "Object section '" << d["section"].value << "' of size "
<< integer2unsigned(array_size) << " bytes";
<< array_size << " bytes";
array_loc.set_comment(array_comment.str());
array_expr.add_source_location()=array_loc;

Expand Down
4 changes: 2 additions & 2 deletions src/goto-instrument/cover_basic_blocks.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
// update lines belonging to block
const irep_idt &line = it->source_location.get_line();
if(!line.empty())
block_info.lines.insert(unsafe_string2unsigned(id2string(line)));
block_info.lines.insert(unsafe_string2size_t(id2string(line)));

// set representative program location to instrument
if(
Expand Down Expand Up @@ -155,7 +155,7 @@ void cover_basic_blockst::update_covered_lines(block_infot &block_info)

const auto &cover_set = block_info.lines;
INVARIANT(!cover_set.empty(), "covered lines set must not be empty");
std::vector<unsigned> line_list(cover_set.begin(), cover_set.end());
std::vector<std::size_t> line_list(cover_set.begin(), cover_set.end());

std::string covered_lines = format_number_range(line_list);
block_info.source_location.set_basic_block_covered_lines(covered_lines);
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/cover_instrument_mcdc.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -361,7 +361,7 @@ void remove_repetition(std::set<exprt> &exprs)
{
std::set<signed> signs1 = sign_of_expr(c, x);
std::set<signed> signs2 = sign_of_expr(c, y);
int s1 = signs1.size(), s2 = signs2.size();
std::size_t s1 = signs1.size(), s2 = signs2.size();
// it is easy to check non-equivalence;
if(s1 != s2)
{
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/document_properties.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ class document_propertiest

void document_propertiest::strip_space(std::list<linet> &lines)
{
unsigned strip=50;
std::size_t strip=50;

for(std::list<linet>::const_iterator it=lines.begin();
it!=lines.end(); it++)
Expand Down
5 changes: 1 addition & 4 deletions src/goto-instrument/function.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -34,10 +34,7 @@ code_function_callt function_to_call(
typet p=pointer_type(char_type());
p.subtype().set(ID_C_constant, true);

code_typet function_type;
function_type.return_type()=empty_typet();
function_type.parameters().push_back(
code_typet::parametert(p));
const code_typet function_type({code_typet::parametert(p)}, empty_typet());

symbolt new_symbol;
new_symbol.name=id;
Expand Down
8 changes: 3 additions & 5 deletions src/goto-instrument/goto_program2code.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -775,15 +775,15 @@ bool goto_program2codet::set_block_end_points(
cases_listt &cases,
std::set<unsigned> &processed_locations)
{
std::map<goto_programt::const_targett, std::size_t> targets_done;
std::set<goto_programt::const_targett> targets_done;

for(cases_listt::iterator it=cases.begin();
it!=cases.end();
++it)
{
// some branch targets may be shared by multiple branch instructions,
// as in case 1: case 2: code; we build a nested code_switch_caset
if(targets_done.find(it->case_start)!=targets_done.end())
if(!targets_done.insert(it->case_start).second)
continue;

// compute the block that belongs to this case
Expand Down Expand Up @@ -819,8 +819,6 @@ bool goto_program2codet::set_block_end_points(

it->case_last=case_end;
}

targets_done[it->case_start]=1;
}

return false;
Expand Down Expand Up @@ -971,7 +969,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch(
it->case_last->location_number > max_target->location_number)
max_target=it->case_last;

std::map<goto_programt::const_targett, unsigned> targets_done;
std::map<goto_programt::const_targett, std::size_t> targets_done;
loop_last_stack.push_back(std::make_pair(max_target, false));

// iterate over all <branch conditions, branch instruction, branch target>
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/wmm/data_dp.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,7 @@ void data_dpt::dp_merge()
if(data.size()<2)
return;

unsigned initial_size=data.size();
std::size_t initial_size=data.size();

unsigned from=0;
unsigned to=0;
Expand Down
4 changes: 2 additions & 2 deletions src/goto-instrument/wmm/goto2graph.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -115,8 +115,8 @@ unsigned instrumentert::goto2graph_cfg(
<< visitor.max_thread << messaget::eom;

/* SCCs which could host critical cycles */
unsigned interesting_sccs=0;
for(unsigned i=0; i<num_sccs; i++)
std::size_t interesting_sccs=0;
for(std::size_t i=0; i<num_sccs; i++)
if(egraph_SCCs[i].size()>3)
interesting_sccs++;

Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/wmm/goto2graph.h
Original file line number Diff line number Diff line change
Expand Up @@ -289,7 +289,7 @@ class instrumentert

/* critical cycles per SCC */
std::vector<std::set<event_grapht::critical_cyclet> > set_of_cycles_per_SCC;
unsigned num_sccs;
std::size_t num_sccs;

/* map from function to begin and end of the corresponding part of the
graph */
Expand Down
6 changes: 3 additions & 3 deletions src/goto-instrument/wmm/weak_memory.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -161,9 +161,9 @@ void weak_memory(
{
instrumenter.collect_cycles_by_SCCs(model);
message.status()<<"cycles collected: "<<messaget::eom;
unsigned interesting_scc = 0;
unsigned total_cycles = 0;
for(unsigned i=0; i<instrumenter.num_sccs; i++)
std::size_t interesting_scc = 0;
std::size_t total_cycles = 0;
for(std::size_t i=0; i<instrumenter.num_sccs; i++)
if(instrumenter.egraph_SCCs[i].size()>=4)
{
message.status()<<"SCC #"<<i<<": "
Expand Down
11 changes: 7 additions & 4 deletions src/goto-programs/goto_convert.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -149,12 +149,15 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
bool stack_is_prefix=true;
if(label_stack.size()>goto_stack.size())
stack_is_prefix=false;
for(std::size_t i=0, ilim=label_stack.size();
i!=ilim && stack_is_prefix;
++i)
auto label_stack_it = label_stack.begin();
for(const auto &g : goto_stack)
{
if(goto_stack[i]!=label_stack[i])
if(!stack_is_prefix || label_stack_it == label_stack.end())
break;
else if(g != *label_stack_it)
stack_is_prefix=false;

++label_stack_it;
}

if(!stack_is_prefix)
Expand Down
6 changes: 3 additions & 3 deletions src/goto-programs/goto_trace.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -214,11 +214,11 @@ void trace_value(
<< "\n";
}

void show_state_header(
static void show_state_header(
std::ostream &out,
const goto_trace_stept &state,
const source_locationt &source_location,
unsigned step_nr)
std::size_t step_nr)
{
out << "\n";

Expand Down Expand Up @@ -249,7 +249,7 @@ void show_goto_trace(
const namespacet &ns,
const goto_tracet &goto_trace)
{
unsigned prev_step_nr=0;
std::size_t prev_step_nr=0;
bool first_step=true;

for(const auto &step : goto_trace.steps)
Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/remove_function_pointers.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ remove_function_pointerst::remove_function_pointerst(

// build type map
forall_goto_functions(f_it, goto_functions)
type_map[f_it->first]=f_it->second.type;
type_map.emplace(f_it->first, f_it->second.type);
}

bool remove_function_pointerst::arg_is_type_compatible(
Expand Down
Loading

0 comments on commit fb8ccf7

Please sign in to comment.