Skip to content

Commit

Permalink
Merge pull request diffblue#2317 from tautschnig/c++-attributes-lists
Browse files Browse the repository at this point in the history
C++ initializer lists and GCC attributes
  • Loading branch information
Daniel Kroening authored Jun 13, 2018
2 parents cad7b3a + 1d95ab4 commit 9441a92
Show file tree
Hide file tree
Showing 14 changed files with 312 additions and 73 deletions.
2 changes: 1 addition & 1 deletion regression/cpp/List_initialization1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG
CORE
main.cpp
-std=c++11
^EXIT=0$
Expand Down
22 changes: 22 additions & 0 deletions regression/cpp/gcc_vector1/main.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
#ifdef __GNUC__

typedef float __m128 __attribute__ ((__vector_size__ (16), __may_alias__));

__m128 setzero(void)
{
return (__m128){ 0.0f, 0.0f, 0.0f, 0.0f };
}

#else

void setzero()
{
}

#endif

int main(int argc, char* argv[])
{
setzero();
return 0;
}
8 changes: 8 additions & 0 deletions regression/cpp/gcc_vector1/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
main.cpp

^EXIT=0$
^SIGNAL=0$
--
^CONVERSION ERROR$
^warning: ignoring
11 changes: 3 additions & 8 deletions src/ansi-c/scanner.l
Original file line number Diff line number Diff line change
Expand Up @@ -948,14 +948,9 @@ __decltype { if(PARSER.cpp98 &&
PARSER.mode==configt::ansi_ct::flavourt::CODEWARRIOR ||
PARSER.mode==configt::ansi_ct::flavourt::ARM)
{
if(PARSER.cpp98)
BEGIN(IGNORE_PARENS);
else
{
BEGIN(GCC_ATTRIBUTE1);
loc();
return TOK_GCC_ATTRIBUTE;
}
BEGIN(GCC_ATTRIBUTE1);
loc();
return TOK_GCC_ATTRIBUTE;
}
else
return make_identifier();
Expand Down
8 changes: 6 additions & 2 deletions src/cpp/cpp_convert_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ class cpp_convert_typet
unsigned unsigned_cnt, signed_cnt, char_cnt, int_cnt, short_cnt,
long_cnt, const_cnt, restrict_cnt, constexpr_cnt, volatile_cnt,
double_cnt, float_cnt, complex_cnt, cpp_bool_cnt, proper_bool_cnt,
extern_cnt, wchar_t_cnt, char16_t_cnt, char32_t_cnt,
extern_cnt, noreturn_cnt, wchar_t_cnt, char16_t_cnt, char32_t_cnt,
int8_cnt, int16_cnt, int32_cnt, int64_cnt, ptr32_cnt, ptr64_cnt,
float128_cnt, int128_cnt;

Expand All @@ -53,7 +53,7 @@ void cpp_convert_typet::read(const typet &type)
unsigned_cnt=signed_cnt=char_cnt=int_cnt=short_cnt=
long_cnt=const_cnt=restrict_cnt=constexpr_cnt=volatile_cnt=
double_cnt=float_cnt=complex_cnt=cpp_bool_cnt=proper_bool_cnt=
extern_cnt=wchar_t_cnt=char16_t_cnt=char32_t_cnt=
extern_cnt=noreturn_cnt=wchar_t_cnt=char16_t_cnt=char32_t_cnt=
int8_cnt=int16_cnt=int32_cnt=int64_cnt=
ptr32_cnt=ptr64_cnt=float128_cnt=int128_cnt=0;

Expand Down Expand Up @@ -132,6 +132,10 @@ void cpp_convert_typet::read_rec(const typet &type)
constexpr_cnt++;
else if(type.id()==ID_extern)
extern_cnt++;
else if(type.id()==ID_noreturn)
{
noreturn_cnt++;
}
else if(type.id()==ID_function_type)
{
read_function_type(type);
Expand Down
2 changes: 0 additions & 2 deletions src/cpp/cpp_typecheck.h
Original file line number Diff line number Diff line change
Expand Up @@ -484,8 +484,6 @@ class cpp_typecheckt:public c_typecheck_baset
void typecheck_method_application(
side_effect_expr_function_callt &expr);

void typecheck_assign(codet &code);

public:
//
// Type Conversions
Expand Down
25 changes: 3 additions & 22 deletions src/cpp/cpp_typecheck_code.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -388,6 +388,9 @@ void cpp_typecheckt::typecheck_decl(codet &code)
return;
}

// mark as 'already typechecked'
make_already_typechecked(type);

codet new_code(ID_decl_block);
new_code.reserve_operands(declaration.declarators().size());

Expand Down Expand Up @@ -453,25 +456,3 @@ void cpp_typecheckt::typecheck_block(codet &code)

c_typecheck_baset::typecheck_block(code);
}

void cpp_typecheckt::typecheck_assign(codet &code)
{
if(code.operands().size()!=2)
{
error().source_location=code.find_source_location();
error() << "assignment statement expected to have two operands"
<< eom;
throw 0;
}

// turn into a side effect
side_effect_exprt expr(code.get(ID_statement));
expr.operands() = code.operands();
typecheck_expr(expr);

code_expressiont code_expr;
code_expr.expression()=expr;
code_expr.add_source_location() = code.source_location();

code.swap(code_expr);
}
7 changes: 7 additions & 0 deletions src/cpp/cpp_typecheck_conversions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1508,6 +1508,13 @@ void cpp_typecheckt::implicit_typecast(exprt &expr, const typet &type)
{
exprt e=expr;

if(
e.id() == ID_initializer_list && cpp_is_pod(type) &&
e.operands().size() == 1)
{
e = expr.op0();
}

if(!implicit_conversion_sequence(e, type, expr))
{
show_instantiation_stack(error());
Expand Down
4 changes: 4 additions & 0 deletions src/cpp/cpp_typecheck_declaration.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,10 @@ void cpp_typecheckt::convert_non_template_declaration(
if(!is_typedef)
elaborate_class_template(declaration_type);

// mark as 'already typechecked'
if(!declaration.declarators().empty())
make_already_typechecked(declaration_type);

// Special treatment for anonymous unions
if(declaration.declarators().empty() &&
follow(declaration.type()).get_bool(ID_C_is_anonymous))
Expand Down
19 changes: 19 additions & 0 deletions src/cpp/cpp_typecheck_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -939,6 +939,25 @@ void cpp_typecheckt::typecheck_expr_explicit_typecast(exprt &expr)
else
typecheck_type(expr.type());

// We allow (TYPE){ initializer_list }
// This is called "compound literal", and is syntactic
// sugar for a (possibly local) declaration.
if(expr.op0().id()==ID_initializer_list)
{
// just do a normal initialization
do_initializer(expr.op0(), expr.type(), false);

// This produces a struct-expression,
// union-expression, array-expression,
// or an expression for a pointer or scalar.
// We produce a compound_literal expression.
exprt tmp(ID_compound_literal, expr.type());
tmp.move_to_operands(expr.op0());
expr=tmp;
expr.set(ID_C_lvalue, true); // these are l-values
return;
}

exprt new_expr;

if(const_typecast(expr.op0(), expr.type(), new_expr) ||
Expand Down
8 changes: 8 additions & 0 deletions src/cpp/cpp_typecheck_fargs.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -129,6 +129,14 @@ bool cpp_typecheck_fargst::match(
std::cout << "OK " << rank << '\n';
#endif
}
else if(
operand.id() == ID_initializer_list && cpp_typecheck.cpp_is_pod(type) &&
operand.operands().size() == 1 &&
cpp_typecheck.implicit_conversion_sequence(
operand.op0(), type, new_expr, rank))
{
distance += rank;
}
else
{
#if 0
Expand Down
8 changes: 8 additions & 0 deletions src/cpp/cpp_typecheck_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -140,6 +140,10 @@ void cpp_typecheckt::typecheck_type(typet &type)
if(type.subtype().get_bool(ID_C_volatile))
type.set(ID_C_volatile, true);
}
else if(type.id()==ID_vector)
{
typecheck_vector_type(to_vector_type(type));
}
else if(type.id()==ID_code)
{
code_typet &code_type=to_code_type(type);
Expand Down Expand Up @@ -259,6 +263,10 @@ void cpp_typecheckt::typecheck_type(typet &type)
else if(type.id()==ID_nullptr)
{
}
else if(type.id()==ID_already_typechecked)
{
c_typecheck_baset::typecheck_type(type);
}
else
{
error().source_location=type.source_location();
Expand Down
2 changes: 1 addition & 1 deletion src/cpp/cpp_util.h
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ exprt cpp_symbol_expr(const symbolt &symbol);

inline void already_typechecked(irept &irep)
{
exprt tmp("already_typechecked");
exprt tmp(ID_already_typechecked);
tmp.copy_to_operands(static_cast<exprt &>(irep));
irep.swap(tmp);
}
Expand Down
Loading

0 comments on commit 9441a92

Please sign in to comment.