Use std::distance in size()

NathanJPhillips · NathanJPhillips · commit cabb7627c380 · 2018-07-03T16:29:26.000+01:00
diff --git a/cbmc/src/util/overlay_map.h b/cbmc/src/util/overlay_map.h
@@ -76,10 +76,7 @@ class overlay_mapt
   size_t size() const
   {
     // TODO: improve this!
-    size_t count = 0;
-    for(auto it = cbegin(); it != cend(); ++it)
-      ++count;
-    return count;
+    return std::distance(cbegin(), cend());
   }
 
   bool empty() const

Original file line number	Diff line number	Diff line change
`@@ -76,10 +76,7 @@ class overlay_mapt`
`76`	`76`	`size_t size() const`
`77`	`77`	`{`
`78`	`78`	`// TODO: improve this!`
`79`		`- size_t count = 0;`
`80`		`- for(auto it = cbegin(); it != cend(); ++it)`
`81`		`- ++count;`
`82`		`- return count;`
	`79`	`+ return std::distance(cbegin(), cend());`
`83`	`80`	`}`
`84`	`81`
`85`	`82`	`bool empty() const`