Add precondition ensuring mode is not empty

romainbrenguier · romainbrenguier · commit fbed57e5623b · 2018-05-02T14:56:32.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
@@ -2105,6 +2105,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
`@@ -2105,6 +2105,7 @@ symbolt &goto_convertt::new_tmp_symbol(`
`2105`	`2105`	`const source_locationt &source_location,`
`2106`	`2106`	`const irep_idt &mode)`
`2107`	`2107`	`{`
	`2108`	`+ PRECONDITION(!mode.empty());`
`2108`	`2109`	`symbolt &new_symbol = get_fresh_aux_symbol(`
`2109`	`2110`	`type,`
`2110`	`2111`	`tmp_symbol_prefix,`