Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 10 additions & 12 deletions src/cpp/cpp_constructor.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -30,10 +30,9 @@ std::optional<codet> cpp_typecheckt::cpp_constructor(

elaborate_class_template(object_tc.type());

typet tmp_type(follow(object_tc.type()));
CHECK_RETURN(!is_reference(tmp_type));
CHECK_RETURN(!is_reference(object_tc.type()));

if(tmp_type.id()==ID_array)
if(object_tc.type().id() == ID_array)
{
// We allow only one operand and it must be tagged with '#array_ini'.
// Note that the operand is an array that is used for copy-initialization.
Expand All @@ -53,11 +52,10 @@ std::optional<codet> cpp_typecheckt::cpp_constructor(
operands.empty() || operands.size() == 1,
"array constructor must have at most one operand");

if(operands.empty() && cpp_is_pod(tmp_type))
if(operands.empty() && cpp_is_pod(object_tc.type()))
return {};

const exprt &size_expr=
to_array_type(tmp_type).size();
const exprt &size_expr = to_array_type(object_tc.type()).size();

if(size_expr.id() == ID_infinity)
return {}; // don't initialize
Expand All @@ -74,7 +72,7 @@ std::optional<codet> cpp_typecheckt::cpp_constructor(
throw 0;
}

/*if(cpp_is_pod(tmp_type))
/*if(cpp_is_pod(object_tc.type()))
{
code_expressiont new_code;
exprt op_tc=operands.front();
Expand Down Expand Up @@ -119,7 +117,7 @@ std::optional<codet> cpp_typecheckt::cpp_constructor(
return std::move(new_code);
}
}
else if(cpp_is_pod(tmp_type))
else if(cpp_is_pod(object_tc.type()))
{
exprt::operandst operands_tc=operands;

Expand Down Expand Up @@ -152,11 +150,11 @@ std::optional<codet> cpp_typecheckt::cpp_constructor(
throw 0;
}
}
else if(tmp_type.id()==ID_union)
else if(object_tc.type().id() == ID_union_tag)
{
UNREACHABLE; // Todo: union
}
else if(tmp_type.id()==ID_struct)
else if(object_tc.type().id() == ID_struct_tag)
{
exprt::operandst operands_tc=operands;

Expand All @@ -166,8 +164,8 @@ std::optional<codet> cpp_typecheckt::cpp_constructor(
add_implicit_dereference(op);
}

const struct_typet &struct_type=
to_struct_type(tmp_type);
const struct_typet &struct_type =
follow_tag(to_struct_tag_type(object_tc.type()));

// set most-derived bits
code_blockt block;
Expand Down
14 changes: 6 additions & 8 deletions src/cpp/cpp_destructor.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -22,17 +22,15 @@ std::optional<codet> cpp_typecheckt::cpp_destructor(
{
elaborate_class_template(object.type());

typet tmp_type(follow(object.type()));
CHECK_RETURN(!is_reference(tmp_type));
CHECK_RETURN(!is_reference(object.type()));

// PODs don't need a destructor
if(cpp_is_pod(tmp_type))
if(cpp_is_pod(object.type()))
return {};

if(tmp_type.id()==ID_array)
if(object.type().id() == ID_array)
{
const exprt &size_expr=
to_array_type(tmp_type).size();
const exprt &size_expr = to_array_type(object.type()).size();

if(size_expr.id() == ID_infinity)
return {}; // don't initialize
Expand Down Expand Up @@ -70,8 +68,8 @@ std::optional<codet> cpp_typecheckt::cpp_destructor(
}
else
{
const struct_typet &struct_type=
to_struct_type(tmp_type);
const struct_typet &struct_type =
follow_tag(to_struct_tag_type(object.type()));

// enter struct scope
cpp_save_scopet save_scope(cpp_scopes);
Expand Down
6 changes: 3 additions & 3 deletions src/cpp/cpp_typecheck.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -67,9 +67,9 @@ const struct_typet &cpp_typecheckt::this_struct_type()
CHECK_RETURN(this_expr.is_not_nil());
CHECK_RETURN(this_expr.type().id() == ID_pointer);

const typet &t = follow(to_pointer_type(this_expr.type()).base_type());
CHECK_RETURN(t.id() == ID_struct);
return to_struct_type(t);
const typet &t = to_pointer_type(this_expr.type()).base_type();
CHECK_RETURN(t.id() == ID_struct_tag);
return follow_tag(to_struct_tag_type(t));
}

std::string cpp_typecheckt::to_string(const exprt &expr)
Expand Down
21 changes: 13 additions & 8 deletions src/cpp/cpp_typecheck.h
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
#include <set>
#include <unordered_set>

class pointer_typet;
class reference_typet;

bool cpp_typecheck(
cpp_parse_treet &cpp_parse_tree,
symbol_table_baset &symbol_table,
Expand Down Expand Up @@ -524,14 +527,18 @@ class cpp_typecheckt:public c_typecheck_baset
bool user_defined_conversion_sequence(
const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank);

bool reference_related(
const exprt &expr, const typet &type) const;
bool reference_related(const exprt &expr, const reference_typet &type) const;

bool reference_compatible(
const exprt &expr, const typet &type, unsigned &rank) const;
const exprt &expr,
const reference_typet &type,
unsigned &rank) const;

bool reference_binding(
exprt expr, const typet &type, exprt &new_expr, unsigned &rank);
exprt expr,
const reference_typet &type,
exprt &new_expr,
unsigned &rank);

bool implicit_conversion_sequence(
const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank);
Expand All @@ -542,7 +549,7 @@ class cpp_typecheckt:public c_typecheck_baset
bool implicit_conversion_sequence(
const exprt &expr, const typet &type, exprt &new_expr);

void reference_initializer(exprt &expr, const typet &type);
void reference_initializer(exprt &expr, const reference_typet &type);

void implicit_typecast(exprt &expr, const typet &type) override;

Expand All @@ -556,9 +563,7 @@ class cpp_typecheckt:public c_typecheck_baset
const struct_typet &from,
const struct_typet &to) const;

void make_ptr_typecast(
exprt &expr,
const typet &dest_type);
void make_ptr_typecast(exprt &expr, const pointer_typet &dest_type);

// the C++ typecasts

Expand Down
22 changes: 13 additions & 9 deletions src/cpp/cpp_typecheck_code.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -9,15 +9,15 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
/// \file
/// C++ Language Type Checking

#include "cpp_typecheck.h"

#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/c_types.h>
#include <util/pointer_expr.h>
#include <util/source_location.h>

#include "cpp_declarator_converter.h"
#include "cpp_exception_id.h"
#include "cpp_typecheck.h"
#include "cpp_typecheck_fargs.h"
#include "cpp_util.h"

Expand Down Expand Up @@ -258,8 +258,7 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code)
PRECONDITION(this_expr.is_not_nil());

make_ptr_typecast(
this_expr,
code_type.parameters().front().type());
this_expr, to_pointer_type(code_type.parameters().front().type()));

function_call.arguments().push_back(this_expr);

Expand Down Expand Up @@ -354,7 +353,8 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code)
throw 0;
}

reference_initializer(code.op0(), symbol_expr.type());
reference_initializer(
code.op0(), to_reference_type(symbol_expr.type()));

// assign the pointers
symbol_expr.type().remove(ID_C_reference);
Expand Down Expand Up @@ -421,8 +421,13 @@ void cpp_typecheckt::typecheck_decl(codet &code)

CHECK_RETURN(type.is_not_nil());

if(declaration.declarators().empty() &&
follow(type).get_bool(ID_C_is_anonymous))
if(
declaration.declarators().empty() &&
((type.id() == ID_struct_tag &&
follow_tag(to_struct_tag_type(type)).get_bool(ID_C_is_anonymous)) ||
(type.id() == ID_union_tag &&
follow_tag(to_union_tag_type(type)).get_bool(ID_C_is_anonymous)) ||
type.get_bool(ID_C_is_anonymous)))
{
if(type.id() != ID_union_tag)
{
Expand Down Expand Up @@ -470,8 +475,7 @@ void cpp_typecheckt::typecheck_decl(codet &code)
{
decl_statement.copy_to_operands(symbol.value);
DATA_INVARIANT(
has_auto(symbol.type) ||
follow(decl_statement.op1().type()) == follow(symbol.type),
has_auto(symbol.type) || decl_statement.op1().type() == symbol.type,
"declarator type should match symbol type");
}

Expand Down
67 changes: 44 additions & 23 deletions src/cpp/cpp_typecheck_compound_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1019,15 +1019,21 @@ void cpp_typecheckt::typecheck_compound_body(symbolt &symbol)
throw 0;
}

typet final_type=follow(declaration.type());

// anonymous member?
if(declaration.declarators().empty() &&
final_type.get_bool(ID_C_is_anonymous))
if(
declaration.declarators().empty() &&
((declaration.type().id() == ID_struct_tag &&
follow_tag(to_struct_tag_type(declaration.type()))
.get_bool(ID_C_is_anonymous)) ||
(declaration.type().id() == ID_union_tag &&
follow_tag(to_union_tag_type(declaration.type()))
.get_bool(ID_C_is_anonymous)) ||
declaration.type().get_bool(ID_C_is_anonymous)))
{
// we only allow this on struct/union types
if(final_type.id()!=ID_union &&
final_type.id()!=ID_struct)
if(
declaration.type().id() != ID_union_tag &&
declaration.type().id() != ID_struct_tag)
{
error().source_location=declaration.type().source_location();
error() << "member declaration does not declare anything"
Expand Down Expand Up @@ -1423,8 +1429,14 @@ void cpp_typecheckt::convert_anon_struct_union_member(
const irep_idt &access,
struct_typet::componentst &components)
{
const struct_union_typet &final_type =
declaration.type().id() == ID_struct_tag
? static_cast<const struct_union_typet &>(
follow_tag(to_struct_tag_type(declaration.type())))
: static_cast<const struct_union_typet &>(
follow_tag(to_union_tag_type(declaration.type())));
symbolt &struct_union_symbol =
symbol_table.get_writeable_ref(follow(declaration.type()).get(ID_name));
symbol_table.get_writeable_ref(final_type.get(ID_name));

if(declaration.storage_spec().is_static() ||
declaration.storage_spec().is_mutable())
Expand Down Expand Up @@ -1477,13 +1489,15 @@ bool cpp_typecheckt::get_component(
const irep_idt &component_name,
exprt &member)
{
const typet &followed_type=follow(object.type());

PRECONDITION(
followed_type.id() == ID_struct || followed_type.id() == ID_union);
object.type().id() == ID_struct_tag || object.type().id() == ID_union_tag);

struct_union_typet final_type=
to_struct_union_type(followed_type);
struct_union_typet final_type =
object.type().id() == ID_struct_tag
? static_cast<const struct_union_typet &>(
follow_tag(to_struct_tag_type(object.type())))
: static_cast<const struct_union_typet &>(
follow_tag(to_union_tag_type(object.type())));

const struct_union_typet::componentst &components=
final_type.components();
Expand Down Expand Up @@ -1529,14 +1543,22 @@ bool cpp_typecheckt::get_component(

return true; // component found
}
else if(follow(component.type()).find(ID_C_unnamed_object).is_not_nil())
else if(
(component.type().id() == ID_struct_tag &&
follow_tag(to_struct_tag_type(component.type()))
.find(ID_C_unnamed_object)
.is_not_nil()) ||
(component.type().id() == ID_union_tag &&
follow_tag(to_union_tag_type(component.type()))
.find(ID_C_unnamed_object)
.is_not_nil()) ||
component.type().find(ID_C_unnamed_object).is_not_nil())
{
// could be anonymous union or struct

const typet &component_type=follow(component.type());

if(component_type.id()==ID_union ||
component_type.id()==ID_struct)
if(
component.type().id() == ID_union_tag ||
component.type().id() == ID_struct_tag)
{
// recursive call!
if(get_component(source_location, tmp, component_name, member))
Expand Down Expand Up @@ -1680,18 +1702,17 @@ bool cpp_typecheckt::subtype_typecast(

void cpp_typecheckt::make_ptr_typecast(
exprt &expr,
const typet &dest_type)
const pointer_typet &dest_type)
{
typet src_type=expr.type();

PRECONDITION(src_type.id() == ID_pointer);
PRECONDITION(dest_type.id() == ID_pointer);

const struct_typet &src_struct = to_struct_type(
static_cast<const typet &>(follow(to_pointer_type(src_type).base_type())));
const struct_typet &src_struct =
follow_tag(to_struct_tag_type(to_pointer_type(src_type).base_type()));

const struct_typet &dest_struct = to_struct_type(
static_cast<const typet &>(follow(to_pointer_type(dest_type).base_type())));
const struct_typet &dest_struct =
follow_tag(to_struct_tag_type(dest_type.base_type()));

PRECONDITION(
subtype_typecast(src_struct, dest_struct) ||
Expand Down
Loading