set mode of gcc_builtin_va_arg symbol; partially addresses issue #2663

Daniel Kroening · Daniel Kroening · commit b1c3955d9da3 · 2018-08-14T22:06:03.000+01:00
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -481,6 +481,7 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
   symbol.base_name=ID_gcc_builtin_va_arg;
   symbol.name=ID_gcc_builtin_va_arg;
   symbol.type=symbol_type;
+  symbol.mode=ID_C;
 
   symbol_table.insert(std::move(symbol));
 }

Original file line number	Diff line number	Diff line change
`@@ -481,6 +481,7 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)`
`481`	`481`	`symbol.base_name=ID_gcc_builtin_va_arg;`
`482`	`482`	`symbol.name=ID_gcc_builtin_va_arg;`
`483`	`483`	`symbol.type=symbol_type;`
	`484`	`+ symbol.mode=ID_C;`
`484`	`485`
`485`	`486`	`symbol_table.insert(std::move(symbol));`
`486`	`487`	`}`