Skip to content

Commit b8c5745

Browse files
committed
Remove deprecated code_typet constructor
It has been deprecated for 9 months.
1 parent 8ebcf97 commit b8c5745

File tree

1 file changed

+0
-10
lines changed

1 file changed

+0
-10
lines changed

src/util/std_types.h

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -737,16 +737,6 @@ class code_typet:public typet
737737
return_type().swap(_return_type);
738738
}
739739

740-
/// \deprecated
741-
DEPRECATED(SINCE(2018, 6, 4, "Use the two argument constructor instead"))
742-
code_typet():typet(ID_code)
743-
{
744-
// make sure these properties are always there to avoid problems
745-
// with irept comparisons
746-
add(ID_parameters);
747-
add_type(ID_return_type);
748-
}
749-
750740
// used to be argumentt -- now uses standard terminology
751741

752742
class parametert:public exprt

0 commit comments

Comments
 (0)