Skip to content

Commit fe04e59

Browse files
committed
Locate var args use even when va_arg_next is not used
Fixes: #934
1 parent ac270c5 commit fe04e59

File tree

3 files changed

+36
-0
lines changed

3 files changed

+36
-0
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
#include<stdarg.h>
2+
#include<stdlib.h>
3+
4+
void bb_verror_msg(const char *s, va_list p, const char *strerr) {
5+
}
6+
7+
void bb_error_msg(const char *s, ...)
8+
{
9+
va_list p;
10+
va_start(p, s);
11+
bb_verror_msg(s, p, NULL);
12+
va_end(p);
13+
}
14+
15+
int main() {
16+
bb_error_msg("FOOO");
17+
return 0;
18+
}
19+
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--dump-c
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
va_list
7+
--
8+
^warning: ignoring

src/goto-instrument/goto_program2code.cpp

+9
Original file line numberDiff line numberDiff line change
@@ -110,14 +110,23 @@ void goto_program2codet::scan_for_varargs()
110110
forall_goto_program_instructions(target, goto_program)
111111
if(target->is_assign())
112112
{
113+
const exprt &l=to_code_assign(target->code).lhs();
113114
const exprt &r=to_code_assign(target->code).rhs();
114115

116+
// find va_arg_next
115117
if(r.id()==ID_side_effect &&
116118
to_side_effect_expr(r).get_statement()==ID_gcc_builtin_va_arg_next)
117119
{
118120
assert(r.has_operands());
119121
va_list_expr.insert(r.op0());
120122
}
123+
// try our modelling of va_start
124+
else if(l.type().id()==ID_pointer &&
125+
l.type().get(ID_C_typedef)=="va_list" &&
126+
l.id()==ID_symbol &&
127+
r.id()==ID_typecast &&
128+
to_typecast_expr(r).op().id()==ID_address_of)
129+
va_list_expr.insert(l);
121130
}
122131

123132
if(!va_list_expr.empty())

0 commit comments

Comments
 (0)