Skip to content

Commit 1a22d3e

Browse files
committed
Expr-to-C: output type information with nondet_symbol
This is a debugging aid to make the output of `--program-only` more helpful when trying to see whether a call to malloc/calloc included type information (via a sizeof annotation).
1 parent 889a84b commit 1a22d3e

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/ansi-c/expr2c.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -1663,7 +1663,7 @@ std::string expr2ct::convert_symbol(const exprt &src)
16631663
std::string expr2ct::convert_nondet_symbol(const nondet_symbol_exprt &src)
16641664
{
16651665
const irep_idt id=src.get_identifier();
1666-
return "nondet_symbol("+id2string(id)+")";
1666+
return "nondet_symbol<" + convert(src.type()) + ">(" + id2string(id) + ")";
16671667
}
16681668

16691669
std::string expr2ct::convert_predicate_symbol(const exprt &src)

0 commit comments

Comments
 (0)