Remove meaningless precondition in object factory

antlechner · antlechner · commit a6a0bec79077 · 2019-04-11T11:01:55.000+01:00
The id() of struct_typets is always ID_struct.
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -763,7 +763,6 @@ void java_object_factoryt::gen_nondet_struct_init(
 {
   const namespacet ns(symbol_table);
   PRECONDITION(ns.follow(expr.type()).id()==ID_struct);
-  PRECONDITION(struct_type.id()==ID_struct);
 
   typedef struct_typet::componentst componentst;
   const irep_idt &struct_tag=struct_type.get_tag();

Original file line number	Diff line number	Diff line change
`@@ -763,7 +763,6 @@ void java_object_factoryt::gen_nondet_struct_init(`
`763`	`763`	`{`
`764`	`764`	`const namespacet ns(symbol_table);`
`765`	`765`	`PRECONDITION(ns.follow(expr.type()).id()==ID_struct);`
`766`		`- PRECONDITION(struct_type.id()==ID_struct);`
`767`	`766`
`768`	`767`	`typedef struct_typet::componentst componentst;`
`769`	`768`	`const irep_idt &struct_tag=struct_type.get_tag();`