Cleanup invariants in read_bin_goto_object

hannes-steffenhagen-diffblue · hannes-steffenhagen-diffblue · commit 458217126366 · 2018-09-17T16:15:24.000+01:00
diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp
@@ -145,7 +145,10 @@ static bool read_bin_goto_object_v4(
       {
         unsigned n=*nit;
         rev_target_mapt::const_iterator entry=rev_target_map.find(n);
-        assert(entry!=rev_target_map.end());
+        INVARIANT(
+          entry != rev_target_map.end(),
+          "Something from the target map should also be in the reverse target "
+          "map");
         ins->targets.push_back(entry->second);
       }
     }

Original file line number	Diff line number	Diff line change
`@@ -145,7 +145,10 @@ static bool read_bin_goto_object_v4(`
`145`	`145`	`{`
`146`	`146`	`unsigned n=*nit;`
`147`	`147`	`rev_target_mapt::const_iterator entry=rev_target_map.find(n);`
`148`		`- assert(entry!=rev_target_map.end());`
	`148`	`+ INVARIANT(`
	`149`	`+ entry != rev_target_map.end(),`
	`150`	`+ "Something from the target map should also be in the reverse target "`
	`151`	`+ "map");`
`149`	`152`	`ins->targets.push_back(entry->second);`
`150`	`153`	`}`
`151`	`154`	`}`