print string constants

Daniel Kroening · Daniel Kroening · commit 376fd21a9553 · 2016-04-05T16:05:47.000+01:00
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -2300,6 +2300,10 @@ std::string expr2ct::convert_constant(
         return convert(src.op0(), precedence);
     }
   }
+  else if(type.id()==ID_string)
+  {
+    return '"'+id2string(src.get_value())+'"';
+  }
   else
     return convert_norep(src, precedence);
 

Original file line number	Diff line number	Diff line change
`@@ -2300,6 +2300,10 @@ std::string expr2ct::convert_constant(`
`2300`	`2300`	`return convert(src.op0(), precedence);`
`2301`	`2301`	`}`
`2302`	`2302`	`}`
	`2303`	`+ else if(type.id()==ID_string)`
	`2304`	`+ {`
	`2305`	`+ return '"'+id2string(src.get_value())+'"';`
	`2306`	`+ }`
`2303`	`2307`	`else`
`2304`	`2308`	`return convert_norep(src, precedence);`
`2305`	`2309`