Avoid default constructing code_ifthenelset

tautschnig · tautschnig · commit 339641c29c1c · 2019-01-26T18:06:53.000Z
The default constructor is deprecated.
diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
@@ -229,7 +229,7 @@ code_ifthenelset java_bytecode_instrumentt::check_class_cast(
   if(null_check_op.type()!=voidptr)
     null_check_op.make_typecast(voidptr);
 
-  codet check_code;
+  optionalt<codet> check_code;
   if(throw_runtime_exceptions)
   {
     check_code=
@@ -251,7 +251,7 @@ code_ifthenelset java_bytecode_instrumentt::check_class_cast(
 
   return code_ifthenelset(
     notequal_exprt(std::move(null_check_op), null_pointer_exprt(voidptr)),
-    std::move(check_code));
+    std::move(*check_code));
 }
 
 /// Checks whether \p expr is null and throws NullPointerException/

Original file line number	Diff line number	Diff line change
`@@ -229,7 +229,7 @@ code_ifthenelset java_bytecode_instrumentt::check_class_cast(`
`229`	`229`	`if(null_check_op.type()!=voidptr)`
`230`	`230`	`null_check_op.make_typecast(voidptr);`
`231`	`231`
`232`		`- codet check_code;`
	`232`	`+ optionalt<codet> check_code;`
`233`	`233`	`if(throw_runtime_exceptions)`
`234`	`234`	`{`
`235`	`235`	`check_code=`
`@@ -251,7 +251,7 @@ code_ifthenelset java_bytecode_instrumentt::check_class_cast(`
`251`	`251`
`252`	`252`	`return code_ifthenelset(`
`253`	`253`	`notequal_exprt(std::move(null_check_op), null_pointer_exprt(voidptr)),`
`254`		`- std::move(check_code));`
	`254`	`+ std::move(*check_code));`
`255`	`255`	`}`
`256`	`256`
`257`	`257`	`/// Checks whether \p expr is null and throws NullPointerException/`