replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #1154 from diffblue/pointer-cleanup 

Pointer cleanup
This commit is contained in:
Michael Tautschnig 2017-07-20 19:24:26 +01:00 committed by GitHub
parent 424ef50cb7 db71221c95
commit f8b8f9e621
42 changed files with 255 additions and 277 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
src/ansi-c/ansi_c_entry_point.cpp
View File

@ -327,16 +327,13 @@ bool ansi_c_entry_point(
zero_string.type().set(ID_size, "infinity");
exprt index(ID_index, char_type());
index.copy_to_operands(zero_string, from_integer(0, uint_type()));
exprt address_of("address_of", pointer_typet());
address_of.type().subtype()=char_type();
address_of.copy_to_operands(index);
exprt address_of=address_of_exprt(index, pointer_type(char_type()));
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);
array_of_exprt array_of(address_of, argv_symbol.type);
init_code.copy_to_operands(
code_assignt(argv_symbol.symbol_expr(), array_of));
@ -400,17 +397,18 @@ bool ansi_c_entry_point(
{
const exprt &arg1=parameters[1];
const pointer_typet &pointer_type=
to_pointer_type(arg1.type());
exprt index_expr(ID_index, arg1.type().subtype());
index_expr.copy_to_operands(
index_exprt index_expr(
argv_symbol.symbol_expr(),
from_integer(0, index_type()));
from_integer(0, index_type()),
pointer_type.subtype());
// 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);
op1=address_of_exprt(index_expr, pointer_type);
}
// do we need envp?
@ -420,13 +418,15 @@ bool ansi_c_entry_point(
exprt &op2=operands[2];
const exprt &arg2=parameters[2];
const pointer_typet &pointer_type=
to_pointer_type(arg2.type());
exprt index_expr(ID_index, arg2.type().subtype());
index_expr.copy_to_operands(
envp_symbol.symbol_expr(), from_integer(0, index_type()));
index_exprt index_expr(
envp_symbol.symbol_expr(),
from_integer(0, index_type()),
pointer_type.subtype());
op2=exprt(ID_address_of, arg2.type());
op2.move_to_operands(index_expr);
op2=address_of_exprt(index_expr, pointer_type);
}
}
}

10
src/ansi-c/c_typecheck_expr.cpp
View File

@ -834,11 +834,10 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr)
if(expr.type().id()==ID_code) // function designator
{ // special case: this is sugar for &f
exprt tmp(ID_address_of, pointer_type(expr.type()));
address_of_exprt tmp(expr, pointer_type(expr.type()));
tmp.set("#implicit", true);
tmp.add_source_location()=expr.source_location();
tmp.move_to_operands(expr);
expr.swap(tmp);
expr=tmp;
}
}
}
@ -1778,11 +1777,10 @@ void c_typecheck_baset::typecheck_expr_function_identifier(exprt &expr)
{
if(expr.type().id()==ID_code)
{
exprt tmp(ID_address_of, pointer_type(expr.type()));
address_of_exprt tmp(expr, pointer_type(expr.type()));
tmp.set(ID_C_implicit, true);
tmp.add_source_location()=expr.source_location();
tmp.move_to_operands(expr);
expr.swap(tmp);
expr=tmp;
}
}

4
src/ansi-c/c_typecheck_type.cpp
View File

@ -1498,9 +1498,7 @@ void c_typecheck_baset::adjust_function_parameter(typet &type) const
{
// see ISO/IEC 9899:1999 page 199 clause 8,
// may be hidden in typedef
pointer_typet tmp;
tmp.subtype()=type;
type.swap(tmp);
type=pointer_type(type);
}
else if(type.id()==ID_KnR)
{

5
src/cpp/cpp_constructor.cpp
View File

@ -289,10 +289,7 @@ codet cpp_typecheckt::cpp_constructor(
assert(tmp_this.id()==ID_address_of
&& tmp_this.op0().id()=="new_object");
exprt address_of(ID_address_of, typet(ID_pointer));
address_of.type().subtype()=object_tc.type();
address_of.copy_to_operands(object_tc);
tmp_this.swap(address_of);
tmp_this=address_of_exprt(object_tc);
if(block.operands().empty())
return to_code(initializer);

4
src/cpp/cpp_convert_type.cpp
View File

@ -251,8 +251,8 @@ void cpp_convert_typet::read_function_type(const typet &type)
// see if it's an array type
if(final_type.id()==ID_array)
{
final_type.id(ID_pointer);
final_type.remove(ID_size);
// turn into pointer type
final_type=pointer_type(final_type.subtype());
}
code_typet::parametert new_parameter(final_type);

5
src/cpp/cpp_destructor.cpp
View File

@ -142,10 +142,7 @@ codet cpp_typecheckt::cpp_destructor(
assert(tmp_this.id()==ID_address_of
&& tmp_this.op0().id()=="new_object");
exprt address_of(ID_address_of, typet(ID_pointer));
address_of.type().subtype()=object.type();
address_of.copy_to_operands(object);
tmp_this.swap(address_of);
tmp_this=address_of_exprt(object, pointer_type(object.type()));
new_code.swap(initializer);
}

7
src/cpp/cpp_typecheck_compound_type.cpp
View File

@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
#include <util/arith_tools.h>
#include <util/simplify_expr.h>
#include <util/std_types.h>
#include <util/c_types.h>
#include <ansi-c/c_qualifiers.h>
@ -545,7 +546,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
// add a virtual-table pointer
struct_typet::componentt compo;
compo.type()=pointer_typet(symbol_typet(vt_name));
compo.type()=pointer_type(symbol_typet(vt_name));
compo.set_name(id2string(symbol.name) +"::@vtable_pointer");
compo.set(ID_base_name, "@vtable_pointer");
compo.set(
@ -567,7 +568,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
// add an entry to the virtual table
struct_typet::componentt vt_entry;
vt_entry.type()=pointer_typet(component.type());
vt_entry.type()=pointer_type(component.type());
vt_entry.set_name(id2string(vtit->first)+"::"+virtual_name);
vt_entry.set(ID_base_name, virtual_name);
vt_entry.set(ID_pretty_name, virtual_name);
@ -1353,7 +1354,7 @@ void cpp_typecheckt::add_this_to_method_type(
if(has_volatile(method_qualifier))
subtype.set(ID_C_volatile, true);
parameter.type()=pointer_typet(subtype);
parameter.type()=pointer_type(subtype);
}
void cpp_typecheckt::add_anonymous_members_to_scope(

154
src/cpp/cpp_typecheck_conversions.cpp
View File

@ -73,15 +73,13 @@ bool cpp_typecheckt::standard_conversion_array_to_pointer(
{
assert(expr.type().id()==ID_array);
exprt index(ID_index, expr.type().subtype());
index.copy_to_operands(expr, from_integer(0, index_type()));
index_exprt index(
expr,
from_integer(0, index_type()));
index.set(ID_C_lvalue, true);
pointer_typet pointer;
pointer.subtype()=expr.type().subtype();
new_expr=exprt(ID_address_of, pointer);
new_expr.move_to_operands(index);
new_expr=address_of_exprt(index);
return true;
}
@ -96,17 +94,10 @@ bool cpp_typecheckt::standard_conversion_array_to_pointer(
bool cpp_typecheckt::standard_conversion_function_to_pointer(
const exprt &expr, exprt &new_expr) const
{
const code_typet &func_type=to_code_type(expr.type());
if(!expr.get_bool(ID_C_lvalue))
return false;
pointer_typet pointer;
pointer.subtype()=func_type;
new_expr=exprt(ID_address_of);
new_expr.copy_to_operands(expr);
new_expr.type()=pointer;
new_expr=address_of_exprt(expr);
return true;
}
@ -887,16 +878,13 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
if(subtype_typecast(from_struct, to_struct))
{
exprt address(ID_address_of, pointer_typet());
address.copy_to_operands(expr);
address.type().subtype()=expr.type();
exprt address=address_of_exprt(expr);
// simplify address
if(expr.id()==ID_dereference)
address=expr.op0();
pointer_typet ptr_sub;
ptr_sub.subtype()=type;
pointer_typet ptr_sub=pointer_type(type);
c_qualifierst qual_from;
qual_from.read(expr.type());
qual_from.write(ptr_sub.subtype());
@ -1019,62 +1007,60 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
}
else if(from_struct.is_not_nil() && arg1_struct.is_not_nil())
{
// try derived-to-base conversion
exprt expr_pfrom(ID_address_of, pointer_typet());
expr_pfrom.type().subtype()=expr.type();
expr_pfrom.copy_to_operands(expr);
// try derived-to-base conversion
address_of_exprt expr_pfrom(expr, pointer_type(expr.type()));
pointer_typet pto=pointer_type(arg1_type);
pointer_typet pto;
pto.subtype()=arg1_type;
exprt expr_ptmp;
tmp_rank=0;
if(standard_conversion_sequence(
expr_pfrom, pto, expr_ptmp, tmp_rank))
{
// check if it's ambiguous
if(found)
return false;
found=true;
exprt expr_ptmp;
tmp_rank=0;
if(standard_conversion_sequence(
expr_pfrom, pto, expr_ptmp, tmp_rank))
rank+=tmp_rank;
// create temporary object
exprt expr_deref=
exprt(ID_dereference, expr_ptmp.type().subtype());
expr_deref.set(ID_C_lvalue, true);
expr_deref.copy_to_operands(expr_ptmp);
expr_deref.add_source_location()=expr.source_location();
exprt new_object("new_object", type);
new_object.set(ID_C_lvalue, true);
new_object.type().set(ID_C_constant, false);
exprt func_symb=cpp_symbol_expr(lookup(component.get(ID_name)));
func_symb.type()=comp_type;
{
// check if it's ambiguous
if(found)
return false;
found=true;
rank+=tmp_rank;
// create temporary object
exprt expr_deref=
exprt(ID_dereference, expr_ptmp.type().subtype());
expr_deref.set(ID_C_lvalue, true);
expr_deref.copy_to_operands(expr_ptmp);
expr_deref.add_source_location()=expr.source_location();
exprt new_object("new_object", type);
new_object.set(ID_C_lvalue, true);
new_object.type().set(ID_C_constant, false);
exprt func_symb=cpp_symbol_expr(lookup(component.get(ID_name)));
func_symb.type()=comp_type;
{
exprt tmp("already_typechecked");
tmp.copy_to_operands(func_symb);
func_symb.swap(func_symb);
}
side_effect_expr_function_callt ctor_expr;
ctor_expr.add_source_location()=expr.source_location();
ctor_expr.function().swap(func_symb);
ctor_expr.arguments().push_back(expr_deref);
typecheck_side_effect_function_call(ctor_expr);
new_expr.swap(ctor_expr);
assert(new_expr.get(ID_statement)==ID_temporary_object);
if(to.get_bool(ID_C_constant))
new_expr.type().set(ID_C_constant, true);
exprt tmp("already_typechecked");
tmp.copy_to_operands(func_symb);
func_symb.swap(func_symb);
}
side_effect_expr_function_callt ctor_expr;
ctor_expr.add_source_location()=expr.source_location();
ctor_expr.function().swap(func_symb);
ctor_expr.arguments().push_back(expr_deref);
typecheck_side_effect_function_call(ctor_expr);
new_expr.swap(ctor_expr);
INVARIANT(
new_expr.get(ID_statement)==ID_temporary_object,
"statement ID");
if(to.get_bool(ID_C_constant))
new_expr.type().set(ID_C_constant, true);
}
}
if(found)
return true;
}
if(found)
return true;
}
}
@ -1297,9 +1283,8 @@ bool cpp_typecheckt::reference_binding(
address_of_exprt tmp;
tmp.add_source_location()=expr.source_location();
tmp.object()=expr;
tmp.type()=pointer_typet();
tmp.type()=pointer_type(tmp.op0().type());
tmp.type().set(ID_C_reference, true);
tmp.type().subtype()=tmp.op0().type();
new_expr.swap(tmp);
}
@ -1427,10 +1412,9 @@ bool cpp_typecheckt::reference_binding(
if(user_defined_conversion_sequence(arg_expr, type.subtype(), new_expr, rank))
{
address_of_exprt tmp;
tmp.type()=pointer_typet();
tmp.type()=pointer_type(new_expr.type());
tmp.object()=new_expr;
tmp.type().set(ID_C_reference, true);
tmp.type().subtype()= new_expr.type();
tmp.add_source_location()=new_expr.source_location();
new_expr.swap(tmp);
return true;
@ -1449,12 +1433,11 @@ bool cpp_typecheckt::reference_binding(
new_expr.swap(tmp);
}
exprt tmp(ID_address_of, pointer_typet());
tmp.copy_to_operands(new_expr);
address_of_exprt tmp(new_expr, pointer_type(new_expr.type()));
tmp.type().set(ID_C_reference, true);
tmp.type().subtype()= new_expr.type();
tmp.add_source_location()=new_expr.source_location();
new_expr.swap(tmp);
new_expr=tmp;
return true;
}
@ -1715,10 +1698,9 @@ bool cpp_typecheckt::const_typecast(
if(new_expr.type()!=type.subtype())
return false;
exprt address_of(ID_address_of, type);
address_of.copy_to_operands(expr);
exprt address_of=address_of_exprt(expr, to_pointer_type(type));
add_implicit_dereference(address_of);
new_expr.swap(address_of);
new_expr=address_of;
return true;
}
else if(type.id()==ID_pointer)
@ -1880,9 +1862,7 @@ bool cpp_typecheckt::reinterpret_typecast(
if(is_reference(type) && e.get_bool(ID_C_lvalue))
{
exprt tmp(ID_address_of, pointer_typet());
tmp.type().subtype()=e.type();
tmp.copy_to_operands(e);
exprt tmp=address_of_exprt(e);
tmp.make_typecast(type);
new_expr.swap(tmp);
return true;
@ -1946,10 +1926,8 @@ bool cpp_typecheckt::static_typecast(
return true;
}
exprt address_of(ID_address_of, pointer_typet());
address_of.type().subtype()=e.type();
address_of.copy_to_operands(e);
make_ptr_typecast(address_of , type);
exprt address_of=address_of_exprt(e);
make_ptr_typecast(address_of, type);
new_expr.swap(address_of);
return true;
}

24
src/cpp/cpp_typecheck_expr.cpp
View File

@ -722,9 +722,7 @@ void cpp_typecheckt::typecheck_expr_address_of(exprt &expr)
// we take the address of the method.
assert(expr.op0().id()==ID_member);
exprt symb=cpp_symbol_expr(lookup(expr.op0().get(ID_component_name)));
exprt address(ID_address_of, typet(ID_pointer));
address.copy_to_operands(symb);
address.type().subtype()=symb.type();
address_of_exprt address(symb, pointer_type(symb.type()));
address.set(ID_C_implicit, true);
expr.op0().swap(address);
}
@ -757,7 +755,7 @@ void cpp_typecheckt::typecheck_expr_address_of(exprt &expr)
const bool is_ref=is_reference(expr.type());
c_typecheck_baset::typecheck_expr_address_of(expr);
if(is_ref)
expr.type()=reference_typet(expr.type().subtype());
expr.type()=reference_type(expr.type().subtype());
}
void cpp_typecheckt::typecheck_expr_throw(exprt &expr)
@ -810,8 +808,8 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr)
expr.set(ID_size, to_array_type(expr.type()).size());
// new actually returns a pointer, not an array
pointer_typet ptr_type;
ptr_type.subtype()=expr.type().subtype();
pointer_typet ptr_type=
pointer_type(expr.type().subtype());
expr.type().swap(ptr_type);
}
else
@ -821,8 +819,7 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr)
expr.set(ID_statement, ID_cpp_new);
pointer_typet ptr_type;
ptr_type.subtype().swap(expr.type());
pointer_typet ptr_type=pointer_type(expr.type());
expr.type().swap(ptr_type);
}
@ -2255,11 +2252,9 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
if(operand.type().id()!=ID_pointer &&
operand.type()==argument.type().subtype())
{
exprt tmp(ID_address_of, typet(ID_pointer));
tmp.type().subtype()=operand.type();
address_of_exprt tmp(operand, pointer_type(operand.type()));
tmp.add_source_location()=operand.source_location();
tmp.move_to_operands(operand);
operand.swap(tmp);
operand=tmp;
}
}
}
@ -2671,10 +2666,7 @@ void cpp_typecheckt::convert_pmop(exprt &expr)
else
{
assert(expr.op0().get_bool(ID_C_lvalue));
exprt address_of(ID_address_of, typet(ID_pointer));
address_of.copy_to_operands(expr.op0());
address_of.type().subtype()=address_of.op0().type();
expr.op0().swap(address_of);
expr.op0()=address_of_exprt(expr.op0());
}
}

4
src/cpp/cpp_typecheck_type.cpp
View File

@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
#include <util/source_location.h>
#include <util/simplify_expr.h>
#include <util/c_types.h>
#include <ansi-c/c_qualifiers.h>
@ -107,8 +108,7 @@ void cpp_typecheckt::typecheck_type(typet &type)
// Add 'this' to the parameters
exprt a0(ID_parameter);
a0.set(ID_C_base_name, ID_this);
a0.type().id(ID_pointer);
a0.type().subtype() = class_object;
a0.type()=pointer_type(class_object);
parameters.insert(parameters.begin(), a0);
}
}

13
src/cpp/cpp_typecheck_virtual_table.cpp
View File

@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
#include "cpp_typecheck.h"
#include <util/std_types.h>
#include <util/c_types.h>
#include <util/std_expr.h>
void cpp_typecheckt::do_virtual_table(const symbolt &symbol)
@ -32,21 +32,20 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol)
const code_typet &code_type=to_code_type(compo.type());
assert(code_type.parameters().size() > 0);
const pointer_typet &pointer_type =
static_cast<const pointer_typet&>(code_type.parameters()[0].type());
const pointer_typet &parameter_pointer_type=
to_pointer_type(code_type.parameters()[0].type());
irep_idt class_id=pointer_type.subtype().get("identifier");
irep_idt class_id=parameter_pointer_type.subtype().get("identifier");
std::map<irep_idt, exprt> &value_map =
vt_value_maps[class_id];
exprt e=symbol_exprt(compo.get_name(), code_type);
if(compo.get_bool("is_pure_virtual"))
{
pointer_typet pointer_type(code_type);
e=null_pointer_exprt(pointer_type);
pointer_typet code_pointer_type=pointer_type(code_type);
e=null_pointer_exprt(code_pointer_type);
value_map[compo.get("virtual_name")]=e;
}
else

2
src/cpp/parse.cpp
View File

@ -6476,7 +6476,7 @@ bool Parser::rPrimaryExpr(exprt &exp)
case TOK_NULLPTR:
lex.get_token(tk);
exp=constant_exprt(ID_NULL, pointer_typet(typet(ID_nullptr)));
exp=constant_exprt(ID_NULL, typet(ID_pointer, typet(ID_nullptr)));
set_location(exp, tk);
#ifdef DEBUG
std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 6\n";

2
src/goto-instrument/function.cpp
View File

@ -32,7 +32,7 @@ code_function_callt function_to_call(
if(s_it==symbol_table.symbols.end())
{
// not there
pointer_typet p(char_type());
typet p=pointer_type(char_type());
p.subtype().set(ID_C_constant, true);
code_typet function_type;

4
src/goto-instrument/goto_program2code.cpp
View File

@ -384,7 +384,7 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
static_cast<typet const&>(r.find(ID_C_va_arg_type));
dereference_exprt deref(
null_pointer_exprt(pointer_typet(va_arg_type)),
null_pointer_exprt(pointer_type(va_arg_type)),
va_arg_type);
type_of.arguments().push_back(deref);
@ -1378,7 +1378,7 @@ goto_programt::const_targett goto_program2codet::convert_start_thread(
// we don't bother setting the type
f.lhs()=cf.lhs();
f.function()=symbol_exprt("pthread_create", code_typet());
exprt n=null_pointer_exprt(pointer_typet(empty_typet()));
exprt n=null_pointer_exprt(pointer_type(empty_typet()));
f.arguments().push_back(n);
f.arguments().push_back(n);
f.arguments().push_back(cf.function());

2
src/goto-instrument/thread_instrumentation.cpp
View File

@ -43,7 +43,7 @@ void thread_exit_instrumentation(goto_programt &goto_program)
binary_exprt get_may("get_may");
// NULL is any
get_may.op0()=null_pointer_exprt(to_pointer_type(pointer_type(empty_typet())));
get_may.op0()=null_pointer_exprt(pointer_type(empty_typet()));
get_may.op1()=address_of_exprt(mutex_locked_string);
end->make_assertion(not_exprt(get_may));

11
src/goto-instrument/wmm/shared_buffers.cpp
View File

@ -6,13 +6,12 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
#include "shared_buffers.h"
#include "fence.h"
#include "../rw_set.h"
#include <util/c_types.h>
/// returns a unique id (for fresh variables)
std::string shared_bufferst::unique(void)
{
@ -54,7 +53,7 @@ const shared_bufferst::varst &shared_bufferst::operator()(
object,
symbol.base_name,
"$read_delayed_var",
pointer_typet(symbol.type));
pointer_type(symbol.type));
for(unsigned cnt=0; cnt<nb_threads; cnt++)
{
@ -121,7 +120,7 @@ void shared_bufferst::add_initialization(goto_programt &goto_program)
assignment(goto_program, t, source_location, vars.second.read_delayed,
false_exprt());
assignment(goto_program, t, source_location, vars.second.read_delayed_var,
null_pointer_exprt(pointer_typet(vars.second.type)));
null_pointer_exprt(pointer_type(vars.second.type)));
for(const auto &id : vars.second.r_buff0_thds)
assignment(goto_program, t, source_location, id, false_exprt());
@ -1173,7 +1172,7 @@ void shared_bufferst::cfg_visitort::weak_memory(
r_it->second.object, vars.type);
symbol_exprt new_read_expr=symbol_exprt(
vars.read_delayed_var,
pointer_typet(vars.type));
pointer_type(vars.type));
symbol_exprt read_delayed_expr=symbol_exprt(
vars.read_delayed, bool_typet());

7
src/goto-programs/builtin_functions.cpp
View File

@ -602,7 +602,7 @@ void goto_convertt::do_java_new(
// we produce a malloc side-effect, which stays
side_effect_exprt malloc_expr(ID_malloc);
malloc_expr.copy_to_operands(object_size);
malloc_expr.type()=pointer_typet(object_type);
malloc_expr.type()=rhs.type();
goto_programt::targett t_n=dest.add_instruction(ASSIGN);
t_n->code=code_assignt(lhs, malloc_expr);
@ -658,7 +658,7 @@ void goto_convertt::do_java_new_array(
// we produce a malloc side-effect, which stays
side_effect_exprt malloc_expr(ID_malloc);
malloc_expr.copy_to_operands(object_size);
malloc_expr.type()=pointer_typet(object_type);
malloc_expr.type()=rhs.type();
goto_programt::targett t_n=dest.add_instruction(ASSIGN);
t_n->code=code_assignt(lhs, malloc_expr);
@ -1384,8 +1384,7 @@ void goto_convertt::do_function_call_symbol(
if(lhs.is_not_nil())
{
typet t=pointer_typet();
t.subtype()=lhs.type();
typet t=pointer_type(lhs.type());
dereference_exprt rhs(lhs.type());
rhs.op0()=typecast_exprt(list_arg, t);
rhs.add_source_location()=function.source_location();

3
src/goto-programs/class_identifier.cpp
View File

@ -12,6 +12,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com
#include "class_identifier.h"
#include <util/std_expr.h>
#include <util/c_types.h>
#include <util/namespace.h>
/// \par parameters: Struct expression
@ -66,7 +67,7 @@ exprt get_class_identifier_field(
"Non-pointer this-arg in remove-virtuals?");
const auto &points_to=this_expr.type().subtype();
if(points_to==empty_typet())
this_expr=typecast_exprt(this_expr, pointer_typet(suggested_type));
this_expr=typecast_exprt(this_expr, pointer_type(suggested_type));
exprt deref=dereference_exprt(this_expr, this_expr.type().subtype());
return build_class_identifier(deref, ns);
}

4
src/goto-programs/goto_convert.cpp
View File

@ -712,9 +712,7 @@ void goto_convertt::convert_decl(
if(destructor.is_not_nil())
{
// add "this"
exprt this_expr(ID_address_of, pointer_typet());
this_expr.type().subtype()=symbol.type;
this_expr.copy_to_operands(symbol_expr);
address_of_exprt this_expr(symbol_expr, pointer_type(symbol.type));
destructor.arguments().push_back(this_expr);
targets.destructor_stack.push_back(destructor);

4
src/goto-programs/goto_convert_new_switch_case.cpp
View File

@ -555,9 +555,7 @@ void goto_convertt::convert_decl(
if(destructor.is_not_nil())
{
// add "this"
exprt this_expr(ID_address_of, pointer_typet());
this_expr.type().subtype()=symbol.type;
this_expr.copy_to_operands(symbol_expr);
address_of_exprt this_expr(symbol_expr, pointer_type(symbol.type));
destructor.arguments().push_back(this_expr);
targets.destructor_stack.push_back(destructor);

4
src/goto-programs/remove_asm.cpp
View File

@ -16,6 +16,7 @@ Date: December 2014
#include <sstream>
#include <util/c_types.h>
#include <util/std_expr.h>
#include <ansi-c/string_constant.h>
@ -61,7 +62,8 @@ void remove_asmt::gcc_asm_function_call(
code_function_callt function_call;
function_call.lhs().make_nil();
const pointer_typet void_pointer=pointer_typet(void_typet());
const typet void_pointer=
pointer_type(void_typet());
// outputs
forall_operands(it, code.op1())

9
src/goto-programs/remove_exceptions.cpp
View File

@ -20,6 +20,7 @@ Date: December 2016
#include <stack>
#include <algorithm>
#include <util/c_types.h>
#include <util/std_expr.h>
#include <util/symbol_table.h>
@ -108,12 +109,12 @@ void remove_exceptionst::add_exceptional_returns(
new_symbol.base_name=id2string(function_symbol.base_name)+EXC_SUFFIX;
new_symbol.name=id2string(function_symbol.name)+EXC_SUFFIX;
new_symbol.mode=function_symbol.mode;
new_symbol.type=typet(ID_pointer, empty_typet());
new_symbol.type=pointer_type(empty_typet());
symbol_table.add(new_symbol);
// initialize the exceptional return with NULL
symbol_exprt lhs_expr_null=new_symbol.symbol_expr();
null_pointer_exprt rhs_expr_null((pointer_typet(empty_typet())));
null_pointer_exprt rhs_expr_null(pointer_type(empty_typet()));
goto_programt::targett t_null=
goto_program.insert_before(goto_program.instructions.begin());
t_null->make_assignment();
@ -146,7 +147,7 @@ void remove_exceptionst::instrument_exception_handler(
symbol_table.lookup(id2string(function_id)+EXC_SUFFIX);
// next we reset the exceptional return to NULL
symbol_exprt lhs_expr_null=function_symbol.symbol_expr();
null_pointer_exprt rhs_expr_null((pointer_typet(empty_typet())));
null_pointer_exprt rhs_expr_null(pointer_type(empty_typet()));
// add the assignment
goto_programt::targett t_null=goto_program.insert_after(instr_it);
@ -326,7 +327,7 @@ void remove_exceptionst::instrument_function_call(
// add a null check (so that instanceof can be applied)
equal_exprt eq_null(
callee_exc,
null_pointer_exprt(pointer_typet(empty_typet())));
null_pointer_exprt(pointer_type(empty_typet())));
goto_programt::targett t_null=goto_program.insert_after(instr_it);
t_null->make_goto(next_it);
t_null->source_location=instr_it->source_location;

5
src/goto-programs/remove_function_pointers.cpp
View File

@ -375,10 +375,7 @@ void remove_function_pointerst::remove_function_pointer(
t3->make_goto(t_final, true_exprt());
// goto to call
address_of_exprt address_of;
address_of.object()=fun;
address_of.type()=pointer_typet();
address_of.type().subtype()=fun.type();
address_of_exprt address_of(fun, pointer_type(fun.type()));
if(address_of.type()!=pointer.type())
address_of.make_typecast(pointer.type());

11
src/goto-programs/remove_virtual_functions.cpp
View File

@ -10,13 +10,13 @@ Author: Daniel Kroening, kroening@kroening.com
/// Remove Virtual Function (Method) Calls
#include "remove_virtual_functions.h"
#include <util/prefix.h>
#include <util/type_eq.h>
#include "class_hierarchy.h"
#include "class_identifier.h"
#include <util/c_types.h>
#include <util/prefix.h>
#include <util/type_eq.h>
class remove_virtual_functionst
{
public:
@ -147,7 +147,8 @@ void remove_virtual_functionst::remove_virtual_function(
t1->make_function_call(code);
auto &newcall=to_code_function_call(t1->code);
newcall.function()=fun.symbol_expr;
pointer_typet need_type(symbol_typet(fun.symbol_expr.get(ID_C_class)));
typet need_type=
pointer_type(symbol_typet(fun.symbol_expr.get(ID_C_class)));
if(!type_eq(newcall.arguments()[0].type(), need_type, ns))
newcall.arguments()[0].make_typecast(need_type);
}

7
src/goto-programs/string_abstraction.cpp
View File

@ -207,7 +207,7 @@ void string_abstractiont::add_argument(
const irep_idt &identifier)
{
typet final_type=is_ptr_argument(type)?
type:pointer_typet(type);
type:pointer_type(type);
str_args.push_back(code_typet::parametert(final_type));
str_args.back().add_source_location()=fct_symbol.location;
@ -689,7 +689,7 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type,
// char* or void* or char[]
if(is_char_type(eff_type.subtype()) ||
eff_type.subtype().id()==ID_empty)
map_entry.first->second=pointer_typet(string_struct);
map_entry.first->second=pointer_type(string_struct);
else
{
const typet &subt=build_abstraction_type_rec(eff_type.subtype(), known);
@ -699,8 +699,7 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type,
map_entry.first->second=
array_typet(subt, to_array_type(eff_type).size());
else
map_entry.first->second=
pointer_typet(subt);
map_entry.first->second=pointer_type(subt);
}
}
}

10
src/goto-programs/string_instrumentation.cpp
View File

@ -825,14 +825,12 @@ void string_instrumentationt::do_strerror(
}
// return a pointer to some magic buffer
exprt index=exprt(ID_index, char_type());
index.copy_to_operands(
index_exprt index(
symbol_buf.symbol_expr(),
from_integer(0, index_type()));
from_integer(0, index_type()),
char_type());
exprt ptr=exprt(ID_address_of, pointer_typet());
ptr.type().subtype()=char_type();
ptr.copy_to_operands(index);
address_of_exprt ptr(index);
// make that zero-terminated
{

5
src/goto-symex/auto_objects.cpp
View File

@ -66,8 +66,9 @@ void goto_symext::initialize_auto_object(
{
// could be NULL nondeterministically
address_of_exprt address_of_expr=
address_of_exprt(make_auto_object(type.subtype()));
address_of_exprt address_of_expr(
make_auto_object(type.subtype()),
pointer_type);
if_exprt rhs(
side_effect_expr_nondett(bool_typet()),

6
src/goto-symex/symex_builtin_functions.cpp
View File

@ -169,7 +169,7 @@ void goto_symext::symex_malloc(
if(object_type.id()==ID_array)
{
rhs.type()=pointer_typet(value_symbol.type.subtype());
rhs.type()=pointer_type(value_symbol.type.subtype());
index_exprt index_expr(value_symbol.type.subtype());
index_expr.array()=value_symbol.symbol_expr();
index_expr.index()=from_integer(0, index_type());
@ -178,7 +178,7 @@ void goto_symext::symex_malloc(
else
{
rhs.op0()=value_symbol.symbol_expr();
rhs.type()=pointer_typet(value_symbol.type);
rhs.type()=pointer_type(value_symbol.type);
}
if(rhs.type()!=lhs.type())
@ -404,7 +404,7 @@ void goto_symext::symex_cpp_new(
// make symbol expression
exprt rhs(ID_address_of, pointer_typet());
exprt rhs(ID_address_of, code.type());
rhs.type().subtype()=code.type().subtype();
if(do_array)

16
src/goto-symex/symex_dereference.cpp
View File

@ -122,7 +122,7 @@ exprt goto_symext::address_arithmetic(
}
// do (expr.type() *)(((char *)op)+offset)
result=typecast_exprt(result, pointer_typet(char_type()));
result=typecast_exprt(result, pointer_type(char_type()));
// there could be further dereferencing in the offset
exprt offset=be.offset();
@ -132,14 +132,14 @@ exprt goto_symext::address_arithmetic(
// treat &array as &array[0]
const typet &expr_type=ns.follow(expr.type());
pointer_typet dest_type;
typet dest_type_subtype;
if(expr_type.id()==ID_array && !keep_array)
dest_type.subtype()=expr_type.subtype();
dest_type_subtype=expr_type.subtype();
else
dest_type.subtype()=expr_type;
dest_type_subtype=expr_type;
result=typecast_exprt(result, dest_type);
result=typecast_exprt(result, pointer_type(dest_type_subtype));
}
else if(expr.id()==ID_index ||
expr.id()==ID_member)
@ -222,7 +222,7 @@ exprt goto_symext::address_arithmetic(
const typet &expr_type=ns.follow(expr.type());
assert((expr_type.id()==ID_array && !keep_array) ||
base_type_eq(pointer_typet(expr_type), result.type(), ns));
base_type_eq(pointer_type(expr_type), result.type(), ns));
return result;
}
@ -281,7 +281,7 @@ void goto_symext::dereference_rec(
index_exprt index_expr=to_index_expr(expr);
address_of_exprt address_of_expr(index_expr.array());
address_of_expr.type()=pointer_typet(expr.type());
address_of_expr.type()=pointer_type(expr.type());
dereference_exprt tmp;
tmp.pointer()=plus_exprt(address_of_expr, index_expr.index());
@ -318,7 +318,7 @@ void goto_symext::dereference_rec(
to_address_of_expr(tc_op).object().type().id()==ID_array &&
base_type_eq(
expr.type(),
pointer_typet(to_address_of_expr(tc_op).object().type().subtype()),
pointer_type(to_address_of_expr(tc_op).object().type().subtype()),
ns))
{
expr=

9
src/java_bytecode/java_bytecode_convert_class.cpp
View File

@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include "java_bytecode_convert_method.h"
#include "java_bytecode_language.h"
#include <util/c_types.h>
#include <util/namespace.h>
#include <util/std_expr.h>
@ -294,7 +295,7 @@ void java_bytecode_convert_classt::add_array_types()
struct_type.components().push_back(comp1);
struct_typet::componentt
comp2("data", pointer_typet(java_type_from_char(l)));
comp2("data", pointer_type(java_type_from_char(l)));
struct_type.components().push_back(comp2);
symbolt symbol;
@ -366,7 +367,7 @@ void java_bytecode_convert_classt::add_string_type()
// Use a pointer-to-unbounded-array instead of a pointer-to-char.
// Saves some casting in the string refinement algorithm but may
// be unnecessary.
string_type.components()[2].type()=pointer_typet(
string_type.components()[2].type()=pointer_type(
array_typet(java_char_type(), infinity_exprt(java_int_type())));
string_type.add_base(symbol_typet("java::java.lang.Object"));
@ -392,9 +393,9 @@ void java_bytecode_convert_classt::add_string_type()
string_equals_type.return_type()=java_boolean_type();
code_typet::parametert thisparam;
thisparam.set_this();
thisparam.type()=pointer_typet(symbol_typet(string_symbol.name));
thisparam.type()=java_reference_type(symbol_typet(string_symbol.name));
code_typet::parametert otherparam;
otherparam.type()=pointer_typet(symbol_typet("java::java.lang.Object"));
otherparam.type()=java_reference_type(symbol_typet("java::java.lang.Object"));
string_equals_type.parameters().push_back(thisparam);
string_equals_type.parameters().push_back(otherparam);
string_equals_symbol.type=std::move(string_equals_type);

51
src/java_bytecode/java_bytecode_convert_method.cpp
View File

@ -9,29 +9,29 @@ Author: Daniel Kroening, kroening@kroening.com
/// \file
/// JAVA Bytecode Language Conversion
#include "java_bytecode_convert_method.h"
#ifdef DEBUG
#include <iostream>
#endif
#include "java_bytecode_convert_method.h"
#include "java_bytecode_convert_method_class.h"
#include "bytecode_info.h"
#include "java_types.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/ieee_float.h>
#include <util/namespace.h>
#include <util/prefix.h>
#include <util/simplify_expr.h>
#include <util/std_expr.h>
#include <util/string2int.h>
#include <util/prefix.h>
#include <util/arith_tools.h>
#include <util/ieee_float.h>
#include <util/simplify_expr.h>
#include <linking/zero_initializer.h>
#include <goto-programs/cfg.h>
#include <analyses/cfg_dominators.h>
#include "java_bytecode_convert_method_class.h"
#include "bytecode_info.h"
#include "java_types.h"
#include <limits>
#include <algorithm>
#include <functional>
@ -242,7 +242,8 @@ void java_bytecode_convert_method_lazy(
code_typet &code_type=to_code_type(member_type);
code_typet::parameterst &parameters=code_type.parameters();
code_typet::parametert this_p;
const reference_typet object_ref_type(symbol_typet(class_symbol.name));
const reference_typet object_ref_type=
java_reference_type(symbol_typet(class_symbol.name));
this_p.type()=object_ref_type;
this_p.set_this();
parameters.insert(parameters.begin(), this_p);
@ -437,7 +438,7 @@ static member_exprt to_member(const exprt &pointer, const exprt &fieldref)
symbol_typet class_type(fieldref.get(ID_class));
exprt pointer2=
typecast_exprt(pointer, pointer_typet(class_type));
typecast_exprt(pointer, java_reference_type(class_type));
const dereference_exprt obj_deref(pointer2, class_type);
@ -1016,7 +1017,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
assert(op.size()==1 && results.size()==1);
code_blockt block;
// TODO throw NullPointerException instead
const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
const exprt not_equal_null(
binary_relation_exprt(lhs, ID_notequal, rhs));
@ -1103,7 +1104,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
else
code_type.set(ID_java_super_method_call, true);
}
pointer_typet object_ref_type(thistype);
reference_typet object_ref_type=java_reference_type(thistype);
code_typet::parametert this_p(object_ref_type);
this_p.set_this();
this_p.set_base_name("this");
@ -1227,7 +1228,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
const member_exprt data_ptr(
deref,
"data",
pointer_typet(java_type_from_char(type_char)));
pointer_type(java_type_from_char(type_char)));
plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type());
typet element_type=data_ptr.type().subtype();
@ -1292,7 +1293,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
const member_exprt data_ptr(
deref,
"data",
pointer_typet(java_type_from_char(type_char)));
pointer_type(java_type_from_char(type_char)));
plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type());
typet element_type=data_ptr.type().subtype();
@ -1327,7 +1328,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
// these need to be references to java.lang.String
results[0]=arg0;
symbol_typet string_type("java::java.lang.String");
results[0].type()=pointer_typet(string_type);
results[0].type()=java_reference_type(string_type);
}
else if(arg0.id()==ID_type)
{
@ -1500,7 +1501,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
irep_idt number=to_constant_expr(arg0).get_value();
assert(op.size()==1 && results.empty());
code_ifthenelset code_branch;
const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
code_branch.cond()=binary_relation_exprt(lhs, ID_notequal, rhs);
code_branch.then_case()=code_gotot(label(number));
@ -1514,7 +1515,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
assert(op.size()==1 && results.empty());
irep_idt number=to_constant_expr(arg0).get_value();
code_ifthenelset code_branch;
const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
code_branch.cond()=binary_relation_exprt(lhs, ID_equal, rhs);
code_branch.then_case()=code_gotot(label(number));
@ -1820,7 +1821,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
{
// use temporary since the stack symbol might get duplicated
assert(op.empty() && results.size()==1);
const pointer_typet ref_type(arg0.type());
const reference_typet ref_type=java_reference_type(arg0.type());
exprt java_new_expr=side_effect_exprt(ID_java_new, ref_type);
if(!i_it->source_location.get_line().empty())
@ -1865,7 +1866,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
else
element_type='a';
const pointer_typet ref_type=java_array_type(element_type);
const reference_typet ref_type=
java_array_type(element_type);
side_effect_exprt java_new_array(ID_java_new_array, ref_type);
java_new_array.copy_to_operands(op[0]);
@ -1905,7 +1907,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
op=pop(dimension);
assert(results.size()==1);
const pointer_typet ref_type(arg0.type());
const reference_typet ref_type=
java_reference_type(arg0.type());
side_effect_exprt java_new_array(ID_java_new_array, ref_type);
java_new_array.operands()=op;
@ -2020,7 +2023,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
code_typet type;
type.return_type()=void_typet();
type.parameters().resize(1);
type.parameters()[0].type()=reference_typet(void_typet());
type.parameters()[0].type()=java_reference_type(void_typet());
code_function_callt call;
call.function()=symbol_exprt("java::monitorenter", type);
call.lhs().make_nil();
@ -2034,7 +2037,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
code_typet type;
type.return_type()=void_typet();
type.parameters().resize(1);
type.parameters()[0].type()=reference_typet(void_typet());
type.parameters()[0].type()=java_reference_type(void_typet());
code_function_callt call;
call.function()=symbol_exprt("java::monitorexit", type);
call.lhs().make_nil();

3
src/java_bytecode/java_bytecode_internal_additions.cpp
View File

@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include <util/std_types.h>
#include <util/cprover_prefix.h>
#include <util/c_types.h>
void java_internal_additions(symbol_tablet &dest)
@ -35,7 +34,7 @@ void java_internal_additions(symbol_tablet &dest)
symbolt symbol;
symbol.base_name="__CPROVER_malloc_object";
symbol.name=CPROVER_PREFIX "malloc_object";
symbol.type=pointer_typet(empty_typet());
symbol.type=pointer_type(empty_typet());
symbol.mode=ID_C;
symbol.is_lvalue=true;
symbol.is_state_var=true;

10
src/java_bytecode/java_bytecode_vtable.cpp
View File

@ -118,7 +118,7 @@ public:
struct_typet::componentt entry_component;
entry_component.set_name(ifc_name);
entry_component.set_base_name(ifc_method->get_base_name());
entry_component.type()=pointer_typet(implementation.type());
entry_component.type()=pointer_type(implementation.type());
vtable_type.components().push_back(entry_component);
const irep_idt &impl_name(implementation.get_name());
@ -288,7 +288,7 @@ static void add_vtable_pointer_member(
{
struct_typet::componentt comp;
comp.type()=pointer_typet(symbol_typet(vt_name));
comp.type()=pointer_type(symbol_typet(vt_name));
comp.set_name(ID_vtable_pointer);
comp.set_base_name(ID_vtable_pointer);
comp.set_pretty_name(ID_vtable_pointer);
@ -391,7 +391,7 @@ static exprt get_ref(
if(ID_symbol==type_id)
return get_ref(address_of_exprt(this_obj), target_type);
assert(ID_pointer==type_id);
const typecast_exprt cast(this_obj, pointer_typet(target_type));
const typecast_exprt cast(this_obj, pointer_type(target_type));
return dereference_exprt(cast, target_type);
}
@ -436,13 +436,13 @@ exprt make_vtable_function(
}
const symbol_typet vtable_type(vtnamest::get_type(class_id));
const pointer_typet vt_ptr_type(vtable_type);
const pointer_typet vt_ptr_type=pointer_type(vtable_type);
const symbol_typet target_type(class_id);
const exprt this_ref(get_ref(this_obj, target_type));
const typet ref_type(this_ref.type());
const member_exprt vtable_member(this_ref, ID_vtable_pointer, vt_ptr_type);
const dereference_exprt vtable(vtable_member, vtable_type); // TODO: cast?
const pointer_typet func_ptr_type(func.type());
const pointer_typet func_ptr_type=pointer_type(func.type());
const member_exprt func_ptr(vtable, func_name, func_ptr_type);
const dereference_exprt virtual_func(func_ptr, func.type());
return virtual_func;

2
src/java_bytecode/java_entry_point.cpp
View File

@ -556,7 +556,7 @@ bool java_entry_point(
exc_symbol.is_static_lifetime=false;
exc_symbol.name=id2string(symbol.name)+EXC_SUFFIX;
exc_symbol.base_name=id2string(symbol.name)+EXC_SUFFIX;
exc_symbol.type=typet(ID_pointer, empty_typet());
exc_symbol.type=java_reference_type(empty_typet());
symbol_table.add(exc_symbol);
exprt::operandst main_arguments=

10
src/java_bytecode/java_object_factory.cpp
View File

@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include <util/arith_tools.h>
#include <util/fresh_symbol.h>
#include <util/std_types.h>
#include <util/c_types.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/namespace.h>
@ -167,7 +167,7 @@ exprt java_object_factoryt::allocate_object(
// malloc expression
exprt malloc_expr=side_effect_exprt(ID_malloc);
malloc_expr.copy_to_operands(object_size);
typet result_type=pointer_typet(allocate_type);
typet result_type=pointer_type(allocate_type);
malloc_expr.type()=result_type;
// Create a symbol for the malloc expression so we can initialize
// without having to do it potentially through a double-deref, which
@ -175,7 +175,7 @@ exprt java_object_factoryt::allocate_object(
symbolt &malloc_sym=new_tmp_symbol(
symbol_table,
loc,
pointer_typet(allocate_type),
pointer_type(allocate_type),
"malloc_site");
symbols_created.push_back(&malloc_sym);
code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr);
@ -532,9 +532,9 @@ void java_object_factoryt::gen_nondet_array_init(
exprt length_expr=member_exprt(deref_expr, "length", comps[1].type());
exprt init_array_expr=member_exprt(deref_expr, "data", comps[2].type());
if(init_array_expr.type()!=pointer_typet(element_type))
if(init_array_expr.type()!=pointer_type(element_type))
init_array_expr=
typecast_exprt(init_array_expr, pointer_typet(element_type));
typecast_exprt(init_array_expr, pointer_type(element_type));
// Interpose a new symbol, as the goto-symex stage can't handle array indexing
// via a cast.

2
src/jsil/jsil_internal_additions.cpp
View File

@ -43,7 +43,7 @@ void jsil_internal_additions(symbol_tablet &dest)
symbolt symbol;
symbol.base_name="__CPROVER_malloc_object";
symbol.name=CPROVER_PREFIX "malloc_object";
symbol.type=pointer_typet(empty_typet());
symbol.type=pointer_type(empty_typet());
symbol.mode=ID_C;
symbol.is_lvalue=true;
symbol.is_state_var=true;

4
src/path-symex/path_symex.cpp
View File

@ -249,7 +249,7 @@ void path_symext::symex_malloc(
if(object_type.id()==ID_array)
{
rhs.type()=pointer_typet(value_symbol.type.subtype());
rhs.type()=pointer_type(value_symbol.type.subtype());
index_exprt index_expr(value_symbol.type.subtype());
index_expr.array()=value_symbol.symbol_expr();
index_expr.index()=from_integer(0, index_type());
@ -258,7 +258,7 @@ void path_symext::symex_malloc(
else
{
rhs.op0()=value_symbol.symbol_expr();
rhs.type()=pointer_typet(value_symbol.type);
rhs.type()=pointer_type(value_symbol.type);
}
if(rhs.type()!=lhs.type())

2
src/pointer-analysis/dereference.cpp
View File

@ -275,7 +275,7 @@ exprt dereferencet::dereference_typecast(
plus_exprt(offset, typecast_exprt(op, offset.type()));
exprt new_typecast=
typecast_exprt(integer, pointer_typet(type));
typecast_exprt(integer, pointer_type(type));
return dereference_exprt(new_typecast, type);
}

13
src/solvers/smt1/smt1_conv.cpp
View File

@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include <util/base_type.h>
#include <util/ieee_float.h>
#include <util/byte_operators.h>
#include <util/c_types.h>
#include <ansi-c/string_constant.h>
@ -286,12 +287,14 @@ void smt1_convt::convert_address_of_rec(
exprt new_index_expr=expr;
new_index_expr.op1()=from_integer(0, index.type());
exprt address_of_expr(ID_address_of, pointer_typet());
address_of_expr.type().subtype()=array.type().subtype();
address_of_expr.copy_to_operands(new_index_expr);
address_of_exprt address_of_expr(
new_index_expr,
pointer_type(array.type().subtype()));
exprt plus_expr(ID_plus, address_of_expr.type());
plus_expr.copy_to_operands(address_of_expr, index);
plus_exprt plus_expr(
address_of_expr,
index,
address_of_expr.type());
convert_expr(plus_expr, true);
}

23
src/solvers/smt2/smt2_conv.cpp
View File

@ -14,15 +14,16 @@ Author: Daniel Kroening, kroening@kroening.com
#include <cassert>
#include <util/arith_tools.h>
#include <util/base_type.h>
#include <util/c_types.h>
#include <util/expr_util.h>
#include <util/fixedbv.h>
#include <util/ieee_float.h>
#include <util/invariant.h>
#include <util/pointer_offset_size.h>
#include <util/std_types.h>
#include <util/std_expr.h>
#include <util/fixedbv.h>
#include <util/pointer_offset_size.h>
#include <util/ieee_float.h>
#include <util/base_type.h>
#include <util/string2int.h>
#include <util/invariant.h>
#include <ansi-c/string_constant.h>
@ -512,12 +513,14 @@ void smt2_convt::convert_address_of_rec(
exprt new_index_expr=expr;
new_index_expr.op1()=from_integer(0, index.type());
exprt address_of_expr(ID_address_of, pointer_typet());
address_of_expr.type().subtype()=array.type().subtype();
address_of_expr.copy_to_operands(new_index_expr);
address_of_exprt address_of_expr(
new_index_expr,
pointer_type(array.type().subtype()));
exprt plus_expr(ID_plus, address_of_expr.type());
plus_expr.copy_to_operands(address_of_expr, index);
plus_exprt plus_expr(
address_of_expr,
index,
address_of_expr.type());
convert_expr(plus_expr);
}

19
src/util/std_expr.cpp
View File

@ -13,10 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
#include "arith_tools.h"
#include "byte_operators.h"
#include "c_types.h"
#include "config.h"
#include "namespace.h"
#include "pointer_offset_size.h"
#include "std_types.h"
bool constant_exprt::value_is_zero_string() const
@ -171,3 +169,20 @@ extractbits_exprt::extractbits_exprt(
upper()=constant_exprt::integer_constant(_upper);
lower()=constant_exprt::integer_constant(_lower);
}
/*******************************************************************\
Function: address_of_exprt::address_of_exprt
Inputs:
Outputs:
Purpose:
\*******************************************************************/
address_of_exprt::address_of_exprt(const exprt &_op):
unary_exprt(ID_address_of, _op, pointer_type(_op.type()))
{
}

12
src/util/std_expr.h
View File

@ -2590,19 +2590,19 @@ inline extractbits_exprt &to_extractbits_expr(exprt &expr)
/*! \brief Operator to return the address of an object
*/
class address_of_exprt:public exprt
class address_of_exprt:public unary_exprt
{
public:
explicit address_of_exprt(const exprt &op):
exprt(ID_address_of, pointer_typet(op.type()))
explicit address_of_exprt(const exprt &op);
address_of_exprt(const exprt &op, const pointer_typet &_type):
unary_exprt(ID_address_of, op, _type)
{
copy_to_operands(op);
}
address_of_exprt():
exprt(ID_address_of, pointer_typet())
unary_exprt(ID_address_of, pointer_typet())
{
operands().resize(1);
}
exprt &object()