Remove void_typet

tautschnig · tautschnig · commit 75d5d2896211 · 2019-02-05T21:56:12.000Z
void_typet had 25 uses across the codebase, while its equivalent empty_typet has
84 uses. Only sometimes using "void_typet" requires that empty_typet and
void_typet forever stay the same.
diff --git a/src/util/std_types.h b/src/util/std_types.h
@@ -54,11 +54,6 @@ class empty_typet:public typet
   }
 };
 
-/// The void type, the same as \ref empty_typet.
-class void_typet:public empty_typet
-{
-};
-
 /// A reference into the symbol table
 class symbol_typet:public typet
 {

Original file line number	Diff line number	Diff line change
`@@ -54,11 +54,6 @@ class empty_typet:public typet`
`54`	`54`	`}`
`55`	`55`	`};`
`56`	`56`
`57`		`-/// The void type, the same as \ref empty_typet.`
`58`		`-class void_typet:public empty_typet`
`59`		`-{`
`60`		`-};`
`61`		`-`
`62`	`57`	`/// A reference into the symbol table`
`63`	`58`	`class symbol_typet:public typet`
`64`	`59`	`{`