numberings now use size_t

kroening · kroening · commit a95d946ba965 · 2016-02-17T17:57:00.000Z
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@6391 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
diff --git a/src/util/numbering.h b/src/util/numbering.h
@@ -19,7 +19,7 @@ template <typename T>
 class numbering:public std::vector<T>
 {
 public:
-  typedef unsigned int number_type;
+  typedef std::size_t number_type;
 
   number_type number(const T &a)
   {

Original file line number	Diff line number	Diff line change
`@@ -19,7 +19,7 @@ template <typename T>`
`19`	`19`	`class numbering:public std::vector<T>`
`20`	`20`	`{`
`21`	`21`	`public:`
`22`		`- typedef unsigned int number_type;`
	`22`	`+ typedef std::size_t number_type;`
`23`	`23`
`24`	`24`	`number_type number(const T &a)`
`25`	`25`	`{`