Merge pull request #7675 from tautschnig/features/nondet-type-info

tautschnig · web-flow · commit 3de13ccb5a99 · 2023-05-18T13:19:08.000+02:00
Expr-to-C: output type information with nondet_symbol
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -1663,7 +1663,7 @@ std::string expr2ct::convert_symbol(const exprt &src)
 std::string expr2ct::convert_nondet_symbol(const nondet_symbol_exprt &src)
 {
   const irep_idt id=src.get_identifier();
-  return "nondet_symbol("+id2string(id)+")";
+  return "nondet_symbol<" + convert(src.type()) + ">(" + id2string(id) + ")";
 }
 
 std::string expr2ct::convert_predicate_symbol(const exprt &src)

Original file line number	Diff line number	Diff line change
`@@ -1663,7 +1663,7 @@ std::string expr2ct::convert_symbol(const exprt &src)`
`1663`	`1663`	`std::string expr2ct::convert_nondet_symbol(const nondet_symbol_exprt &src)`
`1664`	`1664`	`{`
`1665`	`1665`	`const irep_idt id=src.get_identifier();`
`1666`		`- return "nondet_symbol("+id2string(id)+")";`
	`1666`	`+ return "nondet_symbol<" + convert(src.type()) + ">(" + id2string(id) + ")";`
`1667`	`1667`	`}`
`1668`	`1668`
`1669`	`1669`	`std::string expr2ct::convert_predicate_symbol(const exprt &src)`