Support va_list types defined via one-element arrays
Some SV-COMP device driver benchmarks define a va_list type as in the included regression test. As one-element arrays shouldn't make a substantial difference we can easily support this case.
This commit is contained in:
parent
97003017c3
commit
e832e5409f
|
@ -0,0 +1,47 @@
|
|||
#ifdef __GNUC__
|
||||
|
||||
struct __va_list_tag;
|
||||
typedef struct __va_list_tag __va_list_tag;
|
||||
typedef __builtin_va_list __gnuc_va_list[1U];
|
||||
typedef __gnuc_va_list va_list[1U];
|
||||
|
||||
void foo(int n, ...);
|
||||
|
||||
int main()
|
||||
{
|
||||
foo(1, 1u);
|
||||
foo(2, 2l);
|
||||
foo(3, 3.0);
|
||||
return 0;
|
||||
}
|
||||
|
||||
void foo(int n, ...)
|
||||
{
|
||||
va_list args;
|
||||
__builtin_va_start((__va_list_tag *)(&args), n);
|
||||
|
||||
switch(n)
|
||||
{
|
||||
case 1:
|
||||
__CPROVER_assert(__builtin_va_arg(&args, unsigned) == 1, "1");
|
||||
break;
|
||||
case 2:
|
||||
__CPROVER_assert(__builtin_va_arg(&args, long) == 2, "2");
|
||||
break;
|
||||
case 3:
|
||||
__CPROVER_assert(__builtin_va_arg(&args, double) == 3.0, "3");
|
||||
break;
|
||||
}
|
||||
|
||||
__builtin_va_end((__va_list_tag *)(&args));
|
||||
}
|
||||
|
||||
#else
|
||||
|
||||
// __builtin_va_list is GCC/Clang-only
|
||||
|
||||
int main()
|
||||
{
|
||||
}
|
||||
|
||||
#endif
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
--
|
||||
^warning: ignoring
|
|
@ -602,19 +602,23 @@ void goto_convertt::do_array_op(
|
|||
|
||||
exprt make_va_list(const exprt &expr)
|
||||
{
|
||||
// we first strip any typecast
|
||||
if(expr.id()==ID_typecast)
|
||||
return make_va_list(to_typecast_expr(expr).op());
|
||||
exprt result = skip_typecast(expr);
|
||||
|
||||
// if it's an address of an lvalue, we take that
|
||||
if(expr.id() == ID_address_of)
|
||||
if(result.id() == ID_address_of)
|
||||
{
|
||||
const auto &address_of_expr = to_address_of_expr(expr);
|
||||
const auto &address_of_expr = to_address_of_expr(result);
|
||||
if(is_lvalue(address_of_expr.object()))
|
||||
return address_of_expr.object();
|
||||
result = address_of_expr.object();
|
||||
}
|
||||
|
||||
return expr;
|
||||
while(result.type().id() == ID_array &&
|
||||
to_array_type(result.type()).size().is_one())
|
||||
{
|
||||
result = index_exprt{result, from_integer(0, index_type())};
|
||||
}
|
||||
|
||||
return result;
|
||||
}
|
||||
|
||||
/// add function calls to function queue for later processing
|
||||
|
|
Loading…
Reference in New Issue