Skip to content

Commit f6ae635

Browse files
author
Daniel Kroening
committed
use std::size_t in interpreter
1 parent 5191170 commit f6ae635

File tree

2 files changed

+29
-25
lines changed

2 files changed

+29
-25
lines changed

src/goto-programs/interpreter.cpp

+24-23
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ Author: Daniel Kroening, [email protected]
3030
#include "interpreter_class.h"
3131
#include "remove_returns.h"
3232

33-
const size_t interpretert::npos=std::numeric_limits<size_t>::max();
33+
const std::size_t interpretert::npos=std::numeric_limits<size_t>::max();
3434

3535
void interpretert::operator()()
3636
{
@@ -392,7 +392,7 @@ void interpretert::execute_other()
392392
mp_vectort tmp, rhs;
393393
evaluate(pc->code.op1(), tmp);
394394
mp_integer address=evaluate_address(pc->code.op0());
395-
size_t size=get_size(pc->code.op0().type());
395+
std::size_t size=get_size(pc->code.op0().type());
396396
while(rhs.size()<size) rhs.insert(rhs.end(), tmp.begin(), tmp.end());
397397
if(size!=rhs.size())
398398
error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
@@ -419,7 +419,7 @@ void interpretert::execute_decl()
419419
/// \par parameters: an object and a memory offset
420420
struct_typet::componentt interpretert::get_component(
421421
const irep_idt &object,
422-
unsigned offset)
422+
std::size_t offset)
423423
{
424424
const symbolt &symbol=ns.lookup(object);
425425
const typet real_type=ns.follow(symbol.type);
@@ -468,7 +468,7 @@ exprt interpretert::get_value(
468468
for(struct_typet::componentst::const_iterator it=components.begin();
469469
it!=components.end(); it++)
470470
{
471-
size_t size=get_size(it->type());
471+
std::size_t size=get_size(it->type());
472472
const exprt operand=get_value(it->type(), offset);
473473
offset+=size;
474474
result.copy_to_operands(operand);
@@ -480,7 +480,7 @@ exprt interpretert::get_value(
480480
// Get size of array
481481
exprt result=array_exprt(to_array_type(real_type));
482482
const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
483-
size_t subtype_size=get_size(type.subtype());
483+
std::size_t subtype_size=get_size(type.subtype());
484484
std::size_t count;
485485
if(size_expr.id()!=ID_constant)
486486
{
@@ -495,7 +495,7 @@ exprt interpretert::get_value(
495495

496496
// Retrieve the value for each member in the array
497497
result.reserve_operands(count);
498-
for(unsigned i=0; i<count; i++)
498+
for(std::size_t i=0; i<count; i++)
499499
{
500500
const exprt operand=get_value(
501501
type.subtype(),
@@ -533,7 +533,7 @@ exprt interpretert::get_value(
533533
result.reserve_operands(components.size());
534534
for(const struct_union_typet::componentt &expr : components)
535535
{
536-
size_t size=get_size(expr.type());
536+
std::size_t size=get_size(expr.type());
537537
const exprt operand=get_value(expr.type(), rhs, offset);
538538
offset+=size;
539539
result.copy_to_operands(operand);
@@ -546,8 +546,9 @@ exprt interpretert::get_value(
546546
const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
547547

548548
// Get size of array
549-
size_t subtype_size=get_size(type.subtype());
550-
unsigned count;
549+
std::size_t subtype_size=get_size(type.subtype());
550+
551+
std::size_t count;
551552
if(unbounded_size(type))
552553
{
553554
count=base_address_to_actual_size(offset)/subtype_size;
@@ -556,12 +557,12 @@ exprt interpretert::get_value(
556557
{
557558
mp_integer mp_count;
558559
to_integer(size_expr, mp_count);
559-
count=integer2unsigned(mp_count);
560+
count=integer2size_t(mp_count);
560561
}
561562

562563
// Retrieve the value for each member in the array
563564
result.reserve_operands(count);
564-
for(unsigned i=0; i<count; i++)
565+
for(std::size_t i=0; i<count; i++)
565566
{
566567
const exprt operand=get_value(type.subtype(), rhs,
567568
offset+i*subtype_size);
@@ -607,7 +608,7 @@ exprt interpretert::get_value(
607608
// We want the symbol pointed to
608609
std::size_t address=integer2size_t(rhs[offset]);
609610
irep_idt identifier=address_to_identifier(address);
610-
size_t offset=address_to_offset(address);
611+
std::size_t offset=address_to_offset(address);
611612
const typet type=get_type(identifier);
612613
exprt symbol_expr(ID_symbol, type);
613614
symbol_expr.set(ID_identifier, identifier);
@@ -656,7 +657,7 @@ void interpretert::execute_assign()
656657
if(!rhs.empty())
657658
{
658659
mp_integer address=evaluate_address(code_assign.lhs());
659-
size_t size=get_size(code_assign.lhs().type());
660+
std::size_t size=get_size(code_assign.lhs().type());
660661

661662
if(size!=rhs.size())
662663
error() << "!! failed to obtain rhs ("
@@ -684,9 +685,9 @@ void interpretert::execute_assign()
684685
side_effect_exprt side_effect=to_side_effect_expr(code_assign.rhs());
685686
if(side_effect.get_statement()==ID_nondet)
686687
{
687-
unsigned address=integer2unsigned(evaluate_address(code_assign.lhs()));
688-
size_t size=get_size(code_assign.lhs().type());
689-
for(size_t i=0; i<size; i++)
688+
std::size_t address=integer2size_t(evaluate_address(code_assign.lhs()));
689+
std::size_t size=get_size(code_assign.lhs().type());
690+
for(std::size_t i=0; i<size; i++)
690691
{
691692
memory[address+i].initialized=
692693
memory_cellt::initializedt::READ_BEFORE_WRITTEN;
@@ -803,7 +804,7 @@ void interpretert::execute_function_call()
803804
for(const auto &id : locals)
804805
{
805806
const symbolt &symbol=ns.lookup(id);
806-
frame.local_map[id]=integer2unsigned(build_memory_map(id, symbol.type));
807+
frame.local_map[id]=integer2size_t(build_memory_map(id, symbol.type));
807808
}
808809

809810
// assign the arguments
@@ -867,7 +868,7 @@ void interpretert::build_memory_map()
867868

868869
void interpretert::build_memory_map(const symbolt &symbol)
869870
{
870-
size_t size=0;
871+
std::size_t size=0;
871872

872873
if(symbol.type.id()==ID_code)
873874
{
@@ -920,7 +921,7 @@ mp_integer interpretert::build_memory_map(
920921
const typet &type)
921922
{
922923
typet alloc_type=concretize_type(type);
923-
size_t size=get_size(alloc_type);
924+
std::size_t size=get_size(alloc_type);
924925
auto it=dynamic_types.find(id);
925926

926927
if(it!=dynamic_types.end())
@@ -970,7 +971,7 @@ bool interpretert::unbounded_size(const typet &type)
970971
/// get allocated 2^32 address space each (of a 2^64 sized space).
971972
/// \param type: a structured type
972973
/// \return Size of the given type
973-
size_t interpretert::get_size(const typet &type)
974+
std::size_t interpretert::get_size(const typet &type)
974975
{
975976
if(unbounded_size(type))
976977
return 2ULL << 32ULL;
@@ -980,7 +981,7 @@ size_t interpretert::get_size(const typet &type)
980981
const struct_typet::componentst &components=
981982
to_struct_type(type).components();
982983

983-
unsigned sum=0;
984+
std::size_t sum=0;
984985

985986
for(const auto &comp : components)
986987
{
@@ -997,7 +998,7 @@ size_t interpretert::get_size(const typet &type)
997998
const union_typet::componentst &components=
998999
to_union_type(type).components();
9991000

1000-
size_t max_size=0;
1001+
std::size_t max_size=0;
10011002

10021003
for(const auto &comp : components)
10031004
{
@@ -1025,7 +1026,7 @@ size_t interpretert::get_size(const typet &type)
10251026
mp_integer size_mp;
10261027
bool ret=to_integer(size_const, size_mp);
10271028
CHECK_RETURN(!ret);
1028-
return subtype_size*integer2unsigned(size_mp);
1029+
return subtype_size*integer2size_t(size_mp);
10291030
}
10301031
return subtype_size;
10311032
}

src/goto-programs/interpreter_class.h

+5-2
Original file line numberDiff line numberDiff line change
@@ -198,14 +198,17 @@ class interpretert:public messaget
198198

199199
struct_typet::componentt get_component(
200200
const irep_idt &object,
201-
unsigned offset);
201+
std::size_t offset);
202202

203203
typet get_type(const irep_idt &id) const;
204+
204205
exprt get_value(
205206
const typet &type,
206207
std::size_t offset=0,
207208
bool use_non_det=false);
209+
208210
exprt get_value(const typet &type, mp_vectort &rhs, std::size_t offset=0);
211+
209212
exprt get_value(const irep_idt &id);
210213

211214
void step();
@@ -244,7 +247,7 @@ class interpretert:public messaget
244247
goto_functionst::function_mapt::const_iterator return_function;
245248
mp_integer return_value_address;
246249
memory_mapt local_map;
247-
unsigned old_stack_pointer;
250+
std::size_t old_stack_pointer;
248251
};
249252

250253
typedef std::stack<stack_framet> call_stackt;

0 commit comments

Comments
 (0)