remove deprecated array_of_exprt constructor

Daniel Kroening · Daniel Kroening · commit 073dfd4e8469 · 2019-03-22T22:48:06.000Z
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
@@ -1575,11 +1575,6 @@ inline index_exprt &to_index_expr(exprt &expr)
 class array_of_exprt:public unary_exprt
 {
 public:
-  DEPRECATED("use array_of_exprt(what, type) instead")
-  array_of_exprt():unary_exprt(ID_array_of)
-  {
-  }
-
   explicit array_of_exprt(exprt _what, array_typet _type)
     : unary_exprt(ID_array_of, std::move(_what), std::move(_type))
   {

Original file line number	Diff line number	Diff line change
`@@ -1575,11 +1575,6 @@ inline index_exprt &to_index_expr(exprt &expr)`
`1575`	`1575`	`class array_of_exprt:public unary_exprt`
`1576`	`1576`	`{`
`1577`	`1577`	`public:`
`1578`		`- DEPRECATED("use array_of_exprt(what, type) instead")`
`1579`		`- array_of_exprt():unary_exprt(ID_array_of)`
`1580`		`- {`
`1581`		`- }`
`1582`		`-`
`1583`	`1578`	`explicit array_of_exprt(exprt _what, array_typet _type)`
`1584`	`1579`	`: unary_exprt(ID_array_of, std::move(_what), std::move(_type))`
`1585`	`1580`	`{`