Clean-up in gen_nondet_instruction_info

romainbrenguier · romainbrenguier · commit e4b8c4400efc · 2018-07-17T15:03:07.000+01:00
diff --git a/jbmc/src/java_bytecode/replace_java_nondet.cpp b/jbmc/src/java_bytecode/replace_java_nondet.cpp
@@ -93,10 +93,9 @@ get_nondet_instruction_info(const goto_programt::const_targett &instr)
     return nondet_instruction_infot();
   }
   const auto &code = instr->code;
-  if(code.get_statement() != ID_function_call)
-  {
-    return nondet_instruction_infot();
-  }
+  INVARIANT(
+    code.get_statement() == ID_function_call,
+    "function_call should have ID_function_call");
   const auto &function_call = to_code_function_call(code);
   return is_nondet_returning_object(function_call);
 }

Original file line number	Diff line number	Diff line change
`@@ -93,10 +93,9 @@ get_nondet_instruction_info(const goto_programt::const_targett &instr)`
`93`	`93`	`return nondet_instruction_infot();`
`94`	`94`	`}`
`95`	`95`	`const auto &code = instr->code;`
`96`		`- if(code.get_statement() != ID_function_call)`
`97`		`- {`
`98`		`- return nondet_instruction_infot();`
`99`		`- }`
	`96`	`+ INVARIANT(`
	`97`	`+ code.get_statement() == ID_function_call,`
	`98`	`+ "function_call should have ID_function_call");`
`100`	`99`	`const auto &function_call = to_code_function_call(code);`
`101`	`100`	`return is_nondet_returning_object(function_call);`
`102`	`101`	`}`