Fixes from reviews

Andreas Paschos · NlightNFotis · commit 9a60cdbafa02 · 2018-09-25T15:54:50.000+01:00
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
@@ -180,10 +180,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
     }
     else
     {
-      INVARIANT(
-        false,
-        i.code.find_source_location().as_string() +
-          ": finish_gotos: unexpected goto");
+      UNREACHABLE;
     }
   }
 
@@ -198,7 +195,7 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program)
     exprt destination=i.code.op0();
 
     DATA_INVARIANT(
-      destination.id() != ID_dereference, "dereference ID not allowed here");
+      destination.id() == ID_dereference, "dereference ID not allowed here");
     DATA_INVARIANT(destination.operands().size() == 1, "expected 1 argument");
 
     exprt pointer=destination.op0();

Original file line number	Diff line number	Diff line change
`@@ -180,10 +180,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)`
`180`	`180`	`}`
`181`	`181`	`else`
`182`	`182`	`{`
`183`		`- INVARIANT(`
`184`		`- false,`
`185`		`- i.code.find_source_location().as_string() +`
`186`		`- ": finish_gotos: unexpected goto");`
	`183`	`+ UNREACHABLE;`
`187`	`184`	`}`
`188`	`185`	`}`
`189`	`186`
`@@ -198,7 +195,7 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program)`
`198`	`195`	`exprt destination=i.code.op0();`
`199`	`196`
`200`	`197`	`DATA_INVARIANT(`
`201`		`- destination.id() != ID_dereference, "dereference ID not allowed here");`
	`198`	`+ destination.id() == ID_dereference, "dereference ID not allowed here");`
`202`	`199`	`DATA_INVARIANT(destination.operands().size() == 1, "expected 1 argument");`
`203`	`200`
`204`	`201`	`exprt pointer=destination.op0();`