Replace assert by invariant

romainbrenguier · romainbrenguier · commit 36ed947e0903 · 2018-06-13T09:07:31.000+01:00
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1068,10 +1068,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
       if(i_it->statement=="jsr" ||
          i_it->statement=="jsr_w")
       {
-        assert(
-          next!=instructions.end() &&
-          "jsr without valid return address?");
         auto next = std::next(i_it);
+        DATA_INVARIANT(
+          next != instructions.end(), "jsr should have valid return address");
         targets.insert(next->address);
         jsr_ret_targets.push_back(next->address);
       }

Original file line number	Diff line number	Diff line change
`@@ -1068,10 +1068,9 @@ codet java_bytecode_convert_methodt::convert_instructions(`
`1068`	`1068`	`if(i_it->statement=="jsr" \|\|`
`1069`	`1069`	`i_it->statement=="jsr_w")`
`1070`	`1070`	`{`
`1071`		`- assert(`
`1072`		`- next!=instructions.end() &&`
`1073`		`- "jsr without valid return address?");`
`1074`	`1071`	`auto next = std::next(i_it);`
	`1072`	`+ DATA_INVARIANT(`
	`1073`	`+ next != instructions.end(), "jsr should have valid return address");`
`1075`	`1074`	`targets.insert(next->address);`
`1076`	`1075`	`jsr_ret_targets.push_back(next->address);`
`1077`	`1076`	`}`