Add precondition ensuring mode is not empty

romainbrenguier · romainbrenguier · commit 09d8c40b4551 · 2018-05-01T14:31:41.000+01:00
This ensures goto_convert does not create symbols with empty mode, which
could create issues in the later steps of cbmc analysis.
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
@@ -2095,6 +2095,7 @@ symbolt &goto_convertt::new_tmp_symbol(
   const source_locationt &source_location,
   const irep_idt &mode)
 {
+  PRECONDITION(!mode.empty());
   symbolt &new_symbol = get_fresh_aux_symbol(
     type,
     tmp_symbol_prefix,

Original file line number	Diff line number	Diff line change
`@@ -2095,6 +2095,7 @@ symbolt &goto_convertt::new_tmp_symbol(`
`2095`	`2095`	`const source_locationt &source_location,`
`2096`	`2096`	`const irep_idt &mode)`
`2097`	`2097`	`{`
	`2098`	`+ PRECONDITION(!mode.empty());`
`2098`	`2099`	`symbolt &new_symbol = get_fresh_aux_symbol(`
`2099`	`2100`	`type,`
`2100`	`2101`	`tmp_symbol_prefix,`