Skip to content

Commit

Permalink
Merge pull request diffblue#2201 from diffblue/remove-incomplete-type…
Browse files Browse the repository at this point in the history
…-constructors

Remove incomplete type constructors
  • Loading branch information
Daniel Kroening authored May 30, 2018
2 parents a6652d2 + 1fe7cd7 commit 72e99a0
Show file tree
Hide file tree
Showing 11 changed files with 55 additions and 61 deletions.
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1185,7 +1185,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
{
if(cur_pc==it->handler_pc)
{
if(catch_type!=typet() || it->catch_type==symbol_typet())
if(catch_type != typet() || it->catch_type == symbol_typet(irep_idt()))
{
catch_type=symbol_typet("java::java.lang.Throwable");
break;
Expand Down
5 changes: 5 additions & 0 deletions jbmc/src/java_bytecode/java_bytecode_parse_tree.h
Original file line number Diff line number Diff line change
Expand Up @@ -105,6 +105,11 @@ class java_bytecode_parse_treet
struct exceptiont
{
public:
exceptiont()
: start_pc(0), end_pc(0), handler_pc(0), catch_type(irep_idt())
{
}

std::size_t start_pc;
std::size_t end_pc;
std::size_t handler_pc;
Expand Down
11 changes: 8 additions & 3 deletions jbmc/src/java_bytecode/java_string_library_preprocess.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1249,7 +1249,8 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
symbol_table_baset &symbol_table,
code_blockt &code)
{
symbol_typet object_type;
optionalt<symbol_typet> object_type;

typet value_type;
if(type_name==ID_boolean)
{
Expand Down Expand Up @@ -1296,6 +1297,8 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
else
UNREACHABLE;

DATA_INVARIANT(object_type.has_value(), "must have symbol for primitive");

// declare tmp_type_name to hold the value
std::string aux_name="tmp_"+id2string(type_name);
symbolt symbol=get_fresh_aux_symbol(
Expand All @@ -1304,7 +1307,9 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(

// Check that the type of the object is in the symbol table,
// otherwise there is no safe way of finding its value.
if(const auto maybe_symbol=symbol_table.lookup(object_type.get_identifier()))
if(
const auto maybe_symbol =
symbol_table.lookup(object_type->get_identifier()))
{
struct_typet struct_type=to_struct_type(maybe_symbol->type);
// Check that the type has a value field
Expand All @@ -1321,7 +1326,7 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
}
}

warning() << object_type.get_identifier()
warning() << object_type->get_identifier()
<< " not available to format function" << eom;
code.add(code_declt(value), loc);
return value;
Expand Down
18 changes: 12 additions & 6 deletions jbmc/unit/java_bytecode/java_types/generic_type_index.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -17,9 +17,12 @@ SCENARIO("generic_type_index", "[core][java_types]")
const auto symbol_type = symbol_typet("java::GenericClass");
const auto generic_symbol_type = java_generic_symbol_typet(
symbol_type, "LGenericClass<TX;Tvalue;>;", "PrefixClassName");
java_generic_parametert paramX("PrefixClassName::X", symbol_typet());
java_generic_parametert value("PrefixClassName::value", symbol_typet());
java_generic_parametert paramZ("PrefixClassName::Z", symbol_typet());
java_generic_parametert paramX(
"PrefixClassName::X", symbol_typet(irep_idt()));
java_generic_parametert value(
"PrefixClassName::value", symbol_typet(irep_idt()));
java_generic_parametert paramZ(
"PrefixClassName::Z", symbol_typet(irep_idt()));

WHEN("Looking for parameter indexes")
{
Expand All @@ -43,9 +46,12 @@ SCENARIO("generic_type_index", "[core][java_types]")
const auto symbol_type = symbol_typet("java::java.util.Map");
const auto generic_symbol_type = java_generic_symbol_typet(
symbol_type, "Ljava/util/Map<TK;TV;>;", "java.util.HashMap");
java_generic_parametert param0("java.util.HashMap::K", symbol_typet());
java_generic_parametert param1("java.util.HashMap::V", symbol_typet());
java_generic_parametert param2("java.util.HashMap::T", symbol_typet());
java_generic_parametert param0(
"java.util.HashMap::K", symbol_typet(irep_idt()));
java_generic_parametert param1(
"java.util.HashMap::V", symbol_typet(irep_idt()));
java_generic_parametert param2(
"java.util.HashMap::T", symbol_typet(irep_idt()));

WHEN("Looking for parameter indexes")
{
Expand Down
4 changes: 1 addition & 3 deletions src/ansi-c/ansi_c_convert_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -601,10 +601,8 @@ void ansi_c_convert_typet::write(typet &type)

if(vector_size.is_not_nil())
{
vector_typet new_type;
new_type.size()=vector_size;
vector_typet new_type(type, vector_size);
new_type.add_source_location()=vector_size.source_location();
new_type.subtype().swap(type);
type=new_type;
}

Expand Down
3 changes: 1 addition & 2 deletions src/ansi-c/c_typecheck_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -792,9 +792,8 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
}
}

symbol_typet symbol_type;
symbol_typet symbol_type(identifier);
symbol_type.add_source_location()=type.source_location();
symbol_type.set_identifier(identifier);

c_qualifierst original_qualifiers(type);
type.swap(symbol_type);
Expand Down
4 changes: 1 addition & 3 deletions src/cpp/parse.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -5987,9 +5987,7 @@ bool Parser::rNewDeclarator(typet &decl)
if(lex.get_token(cb)!=']')
return false;

array_typet array_type;
array_type.size().swap(expr);
array_type.subtype().swap(decl);
array_typet array_type(decl, expr);
set_location(array_type, ob);

decl.swap(array_type);
Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/remove_virtual_functions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -177,7 +177,7 @@ void remove_virtual_functionst::remove_virtual_function(
// So long as `this` is already not `void*` typed, the second parameter
// is ignored:
exprt this_class_identifier =
get_class_identifier_field(this_expr, symbol_typet(), ns);
get_class_identifier_field(this_expr, symbol_typet(irep_idt()), ns);

// If instructed, add an ASSUME(FALSE) to handle the case where we don't
// match any expected type:
Expand Down
4 changes: 1 addition & 3 deletions src/goto-programs/string_instrumentation.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -791,9 +791,7 @@ void string_instrumentationt::do_strerror(
new_symbol_size.is_lvalue=true;
new_symbol_size.is_static_lifetime=true;

array_typet type;
type.subtype()=char_type();
type.size()=new_symbol_size.symbol_expr();
array_typet type(char_type(), new_symbol_size.symbol_expr());
symbolt new_symbol_buf;
new_symbol_buf.mode=ID_C;
new_symbol_buf.type=type;
Expand Down
30 changes: 16 additions & 14 deletions src/solvers/smt2/smt2_parser.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1028,26 +1028,27 @@ typet smt2_parsert::function_signature_definition()
return sort();
}

mathematical_function_typet result;
mathematical_function_typet::domaint domain;

while(peek()!=CLOSE)
{
if(next_token()!=OPEN)
{
error() << "expected '(' at beginning of parameter" << eom;
return result;
return nil_typet();
}

if(next_token()!=SYMBOL)
{
error() << "expected symbol in parameter" << eom;
return result;
return nil_typet();
}

auto &var=result.add_variable();
mathematical_function_typet::variablet var;
std::string id=buffer;
var.set_identifier(id);
var.type()=sort();
domain.push_back(var);

auto &entry=id_map[id];
entry.type=var.type();
Expand All @@ -1056,15 +1057,15 @@ typet smt2_parsert::function_signature_definition()
if(next_token()!=CLOSE)
{
error() << "expected ')' at end of parameter" << eom;
return result;
return nil_typet();
}
}

next_token(); // eat the ')'

result.codomain()=sort();
typet codomain = sort();

return result;
return mathematical_function_typet(domain, codomain);
}

typet smt2_parsert::function_signature_declaration()
Expand All @@ -1081,37 +1082,38 @@ typet smt2_parsert::function_signature_declaration()
return sort();
}

mathematical_function_typet result;
mathematical_function_typet::domaint domain;

while(peek()!=CLOSE)
{
if(next_token()!=OPEN)
{
error() << "expected '(' at beginning of parameter" << eom;
return result;
return nil_typet();
}

if(next_token()!=SYMBOL)
{
error() << "expected symbol in parameter" << eom;
return result;
return nil_typet();
}

auto &var=result.add_variable();
mathematical_function_typet::variablet var;
var.type()=sort();
domain.push_back(var);

if(next_token()!=CLOSE)
{
error() << "expected ')' at end of parameter" << eom;
return result;
return nil_typet();
}
}

next_token(); // eat the ')'

result.codomain()=sort();
typet codomain = sort();

return result;
return mathematical_function_typet(domain, codomain);
}

void smt2_parsert::command(const std::string &c)
Expand Down
33 changes: 8 additions & 25 deletions src/util/std_types.h
Original file line number Diff line number Diff line change
Expand Up @@ -110,10 +110,6 @@ class real_typet:public typet
class symbol_typet:public typet
{
public:
symbol_typet():typet(ID_symbol)
{
}

explicit symbol_typet(const irep_idt &identifier):typet(ID_symbol)
{
set_identifier(identifier);
Expand Down Expand Up @@ -492,10 +488,6 @@ inline union_typet &to_union_type(typet &type)
class tag_typet:public typet
{
public:
explicit tag_typet(const irep_idt &_id):typet(_id)
{
}

explicit tag_typet(
const irep_idt &_id,
const irep_idt &identifier):typet(_id)
Expand Down Expand Up @@ -980,10 +972,6 @@ inline code_typet &to_code_type(typet &type)
class array_typet:public type_with_subtypet
{
public:
array_typet():type_with_subtypet(ID_array)
{
}

array_typet(
const typet &_subtype,
const exprt &_size):type_with_subtypet(ID_array, _subtype)
Expand Down Expand Up @@ -1575,10 +1563,6 @@ inline const string_typet &to_string_type(const typet &type)
class range_typet:public typet
{
public:
range_typet():typet(ID_range)
{
}

range_typet(const mp_integer &_from, const mp_integer &_to)
{
set_from(_from);
Expand Down Expand Up @@ -1613,10 +1597,6 @@ inline const range_typet &to_range_type(const typet &type)
class vector_typet:public type_with_subtypet
{
public:
vector_typet():type_with_subtypet(ID_vector)
{
}

vector_typet(
const typet &_subtype,
const exprt &_size):type_with_subtypet(ID_vector, _subtype)
Expand Down Expand Up @@ -1706,11 +1686,6 @@ inline complex_typet &to_complex_type(typet &type)
class mathematical_function_typet:public typet
{
public:
mathematical_function_typet():typet(ID_mathematical_function)
{
subtypes().resize(2);
}

// the domain of the function is composed of zero, one, or
// many variables
class variablet:public irept
Expand Down Expand Up @@ -1740,6 +1715,14 @@ class mathematical_function_typet:public typet

using domaint=std::vector<variablet>;

mathematical_function_typet(const domaint &_domain, const typet &_codomain)
: typet(ID_mathematical_function)
{
subtypes().resize(2);
domain() = _domain;
codomain() = _codomain;
}

domaint &domain()
{
return (domaint &)subtypes()[0].subtypes();
Expand Down

0 comments on commit 72e99a0

Please sign in to comment.