cleanup for alignof

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@1701 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2012-09-17 16:13:04 +00:00
parent 2844b9ea77
commit 30eeabb738
8 changed files with 43 additions and 8 deletions

View File

@ -123,7 +123,7 @@ void ansi_c_convertt::convert_expr(exprt &expr)
exprt &designator=static_cast<exprt &>(expr.add(ID_designator));
convert_expr(designator);
}
else if(expr.id()==ID_builtin_alignof)
else if(expr.id()==ID_alignof)
{
if(expr.operands().size()==0)
{

View File

@ -111,7 +111,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
typecheck_expr_typecast(expr);
else if(expr.id()==ID_sizeof)
typecheck_expr_sizeof(expr);
else if(expr.id()==ID_builtin_alignof)
else if(expr.id()==ID_alignof)
typecheck_expr_alignof(expr);
else if(expr.id()==ID_plus || expr.id()==ID_minus ||
expr.id()==ID_mult || expr.id()==ID_div ||

View File

@ -3622,9 +3622,10 @@ std::string expr2ct::convert(
return convert_function(src, "gcc_builtin_va_arg", precedence=15);
}
else if(src.id()==ID_builtin_alignof)
else if(src.id()==ID_alignof)
{
return convert_function(src, "builtin_alignof", precedence=15);
// C uses "_Alignof", C++ uses "alignof"
return convert_function(src, "alignof", precedence=15);
}
else if(has_prefix(src.id_string(), "byte_extract"))

View File

@ -401,13 +401,13 @@ offsetof_member_designator:
alignof: TOK_ALIGNOF '(' unary_expression ')'
{ $$=$1;
set($$, ID_builtin_alignof);
set($$, ID_alignof);
mto($$, $3);
}
| TOK_ALIGNOF '(' type_name ')'
{
$$=$1;
stack($$).id(ID_builtin_alignof);
stack($$).id(ID_alignof);
stack($$).add(ID_type_arg).swap(stack($3));
}
;

View File

@ -124,6 +124,7 @@ protected:
bool rThrowExpr(exprt &);
bool rSizeofExpr(exprt &);
bool rTypeidExpr(exprt &);
bool rAlignofExpr(exprt &);
bool isAllocateExpr(int);
bool rAllocateExpr(exprt &);
bool rAllocateType(exprt &, typet &, exprt &);
@ -4245,6 +4246,8 @@ bool Parser::rUnaryExpr(exprt &exp)
}
else if(t==TOK_SIZEOF)
return rSizeofExpr(exp);
else if(t==TOK_ALIGNOF)
return rAlignofExpr(exp);
else if(t==TOK_THROW)
return rThrowExpr(exp);
else if(t==TOK_REAL || t==TOK_IMAG)
@ -4413,6 +4416,35 @@ bool Parser::rSizeofExpr(exprt &exp)
return true;
}
/*
alignof.expr
| ALIGNOF '(' type.name ')'
*/
bool Parser::rAlignofExpr(exprt &exp)
{
Token tk;
if(lex->GetToken(tk)!=TOK_ALIGNOF)
return false;
typet tname;
Token op, cp;
lex->GetToken(op);
if(!rTypeName(tname))
return false;
if(lex->GetToken(cp)!=')')
return false;
exp=exprt(ID_alignof);
exp.add(ID_type_arg).swap(tname);
set_location(exp, tk);
return true;
}
bool Parser::isAllocateExpr(int t)
{
if(t==TOK_SCOPE)

View File

@ -181,7 +181,7 @@ pragma "#"{horizontal_white}*pragma{horizontal_white}.*"\n"
({v_tab}|{c_return}|{form_feed})+
({horizontal_white}|{v_tab}|{c_return}|{form_feed})*"\n"
__alignof__ { loc(); return TOK_SIZEOF; }
__alignof__ { loc(); return TOK_ALIGNOF; }
"__asm" { if(PARSER.mode==cpp_parsert::MSC)
{
@ -250,6 +250,7 @@ __signed { loc(); return TOK_SIGNED; }
__signed__ { loc(); return TOK_SIGNED; }
__vector { /* ignore */ }
__volatile__ { loc(); return TOK_VOLATILE; }
alignof { loc(); return TOK_ALIGNOF; }
typeof { loc(); return TOK_TYPEOF; }
__typeof { loc(); return TOK_TYPEOF; }
__typeof__ { loc(); return TOK_TYPEOF; }

View File

@ -104,6 +104,7 @@ TOK_REAL,
TOK_IMAG,
TOK_NULLPTR,
TOK_ASM_STRING,
TOK_ALIGNOF,
TOK_Ignore,
TOK_GCC_ASM,

View File

@ -290,7 +290,7 @@ X
continuous_assign
blocking_assign
non_blocking_assign
builtin_alignof
alignof
gcc_builtin_va_arg
gcc_builtin_types_compatible_p
gcc_builtin_va_arg_next