Move string into map rather than copy it

NathanJPhillips · NathanJPhillips · commit 1c73c4dc4180 · 2019-05-23T14:18:00.000+01:00
diff --git a/jbmc/src/java_bytecode/jar_file.cpp b/jbmc/src/java_bytecode/jar_file.cpp
@@ -20,10 +20,7 @@ void jar_filet::initialize_file_index()
 {
   const size_t file_count=m_zip_archive.get_num_files();
   for(size_t index=0; index<file_count; index++)
-  {
-    const auto filename=m_zip_archive.get_filename(index);
-    m_name_to_index.emplace(filename, index);
-  }
+    m_name_to_index.emplace(m_zip_archive.get_filename(index), index);
 }
 
 /// This constructor creates a jar_file object whose contents

Original file line number	Diff line number	Diff line change
`@@ -20,10 +20,7 @@ void jar_filet::initialize_file_index()`
`20`	`20`	`{`
`21`	`21`	`const size_t file_count=m_zip_archive.get_num_files();`
`22`	`22`	`for(size_t index=0; index<file_count; index++)`
`23`		`- {`
`24`		`- const auto filename=m_zip_archive.get_filename(index);`
`25`		`- m_name_to_index.emplace(filename, index);`
`26`		`- }`
	`23`	`+ m_name_to_index.emplace(m_zip_archive.get_filename(index), index);`
`27`	`24`	`}`
`28`	`25`
`29`	`26`	`/// This constructor creates a jar_file object whose contents`