refinement for __builtin_constant_p

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@2818 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2013-07-31 13:33:48 +00:00
parent c45af23b67
commit 3751ed075c
4 changed files with 57 additions and 3 deletions

View File

@ -0,0 +1,29 @@
#include <assert.h>
enum { E1=1 } var;
struct whatnot
{
} whatnot_var;
int main()
{
// this is gcc only
#ifdef __GNUC__
assert(__builtin_constant_p("some string"));
assert(__builtin_constant_p(1.0f));
assert(__builtin_constant_p(E1));
assert(!__builtin_constant_p(var));
assert(!__builtin_constant_p(main));
assert(!__builtin_constant_p(whatnot_var));
assert(!__builtin_constant_p(&var));
assert(__builtin_constant_p(__builtin_constant_p(var)));
// side-effects are _not_ evaluated
int i=0;
assert(!__builtin_constant_p(i++));
assert(i==0);
#endif
}

View File

@ -0,0 +1,8 @@
CORE
main.c
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
^CONVERSION ERROR$

View File

@ -2398,8 +2398,25 @@ void c_typecheck_baset::do_special_functions(
// try to produce constant
exprt tmp1=expr.arguments().front();
simplify(tmp1, *this);
exprt tmp2=from_integer(tmp1.is_constant(), expr.type());
bool is_constant=false;
// Need to do some special treatment for string literals,
// which are (void *)&("lit"[0])
if(tmp1.id()==ID_typecast &&
tmp1.operands().size()==1 &&
tmp1.op0().id()==ID_address_of &&
tmp1.op0().operands().size()==1 &&
tmp1.op0().op0().id()==ID_index &&
tmp1.op0().op0().operands().size()==2 &&
tmp1.op0().op0().op0().id()==ID_string_constant)
{
is_constant=true;
}
else
is_constant=tmp1.is_constant();
exprt tmp2=from_integer(is_constant, expr.type());
tmp2.location()=location;
expr.swap(tmp2);
}

View File

@ -4,7 +4,7 @@ void __builtin_va_end(void *ap);
void __builtin_va_copy(__builtin_va_list dest, __builtin_va_list src);
void *__builtin_va_arg_pack();
int __builtin_va_arg_pack_len();
int __builtin_constant_p(int);
int __builtin_constant_p();
int __builtin_abs(int);
long int __builtin_labs(long);
double __builtin_cos(double);