diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index a8a62957528..fef704dcca0 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -79,7 +79,7 @@ bool compilet::doit()
 {
   goto_model.goto_functions.clear();
 
-  add_compiler_specific_defines(config);
+  add_compiler_specific_defines();
 
   // Parse command line for source and object file names
   for(const auto &arg : cmdline.args)
@@ -381,7 +381,7 @@ bool compilet::link()
     convert_symbols(goto_model.goto_functions);
   }
 
-  if(write_object_file(output_file_executable, goto_model))
+  if(write_bin_object_file(output_file_executable, goto_model))
     return true;
 
   return add_written_cprover_symbols(goto_model.symbol_table);
@@ -441,7 +441,7 @@ bool compilet::compile()
       else
         cfn = output_file_object;
 
-      if(write_object_file(cfn, goto_model))
+      if(write_bin_object_file(cfn, goto_model))
         return true;
 
       if(add_written_cprover_symbols(goto_model.symbol_table))
@@ -580,31 +580,21 @@ bool compilet::parse_stdin()
   return false;
 }
 
-/// writes the goto functions in the function table to a binary format object
+/// Writes the goto functions of \p src_goto_model to a binary format object
 /// file.
-/// \par parameters: file_name, functions table
-/// \return true on error, false otherwise
-bool compilet::write_object_file(
-  const std::string &file_name,
-  const goto_modelt &goto_model)
-{
-  return write_bin_object_file(file_name, goto_model);
-}
-
-/// writes the goto functions in the function table to a binary format object
-/// file.
-/// \par parameters: file_name, functions table
+/// \param file_name: Target file to serialize \p src_goto_model to
+/// \param src_goto_model: goto model to serialize
 /// \return true on error, false otherwise
 bool compilet::write_bin_object_file(
   const std::string &file_name,
-  const goto_modelt &goto_model)
+  const goto_modelt &src_goto_model)
 {
   statistics() << "Writing binary format object `"
                << file_name << "'" << eom;
 
   // symbols
-  statistics() << "Symbols in table: " << goto_model.symbol_table.symbols.size()
-               << eom;
+  statistics() << "Symbols in table: "
+               << src_goto_model.symbol_table.symbols.size() << eom;
 
   std::ofstream outfile(file_name, std::ios::binary);
 
@@ -614,13 +604,14 @@ bool compilet::write_bin_object_file(
     return true;
   }
 
-  if(write_goto_binary(outfile, goto_model))
+  if(write_goto_binary(outfile, src_goto_model))
     return true;
 
-  const auto cnt = function_body_count(goto_model.goto_functions);
+  const auto cnt = function_body_count(src_goto_model.goto_functions);
 
-  statistics() << "Functions: " << goto_model.goto_functions.function_map.size()
-               << "; " << cnt << " have a body." << eom;
+  statistics() << "Functions: "
+               << src_goto_model.goto_functions.function_map.size() << "; "
+               << cnt << " have a body." << eom;
 
   outfile.close();
   wrote_object=true;
@@ -690,7 +681,7 @@ compilet::function_body_count(const goto_functionst &functions) const
   return count;
 }
 
-void compilet::add_compiler_specific_defines(configt &config) const
+void compilet::add_compiler_specific_defines() const
 {
   config.ansi_c.defines.push_back(
     std::string("__GOTO_CC_VERSION__=") + CBMC_VERSION);
diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h
index a423e356cfb..3ffde8ee4f1 100644
--- a/src/goto-cc/compile.h
+++ b/src/goto-cc/compile.h
@@ -71,8 +71,6 @@ class compilet : public messaget
 
   bool parse_source(const std::string &);
 
-  bool write_object_file(const std::string &, const goto_modelt &);
-
   bool write_bin_object_file(const std::string &, const goto_modelt &);
 
   /// \brief Has this compiler written any object files?
@@ -98,7 +96,7 @@ class compilet : public messaget
 
   std::size_t function_body_count(const goto_functionst &) const;
 
-  void add_compiler_specific_defines(class configt &config) const;
+  void add_compiler_specific_defines() const;
 
   void convert_symbols(goto_functionst &dest);
 
diff --git a/src/goto-cc/gcc_cmdline.cpp b/src/goto-cc/gcc_cmdline.cpp
index a44a00c8349..254ffe38fe3 100644
--- a/src/goto-cc/gcc_cmdline.cpp
+++ b/src/goto-cc/gcc_cmdline.cpp
@@ -221,13 +221,13 @@ bool gcc_cmdlinet::parse(int argc, const char **argv)
   assert(argc>0);
   add_arg(argv[0]);
 
-  argst args;
-  args.reserve(argc-1);
+  argst current_args;
+  current_args.reserve(argc - 1);
 
   for(int i=1; i<argc; i++)
-    args.push_back(argv[i]);
+    current_args.push_back(argv[i]);
 
-  bool result=parse_arguments(args, false);
+  bool result = parse_arguments(current_args, false);
 
   parse_specs();
 
@@ -235,11 +235,11 @@ bool gcc_cmdlinet::parse(int argc, const char **argv)
 }
 
 bool gcc_cmdlinet::parse_arguments(
-  const argst &args,
+  const argst &args_to_parse,
   bool in_spec_file)
 {
-  for(argst::const_iterator it=args.begin();
-      it!=args.end();
+  for(argst::const_iterator it = args_to_parse.begin();
+      it != args_to_parse.end();
       ++it)
   {
     const std::string &argv_i=*it;
@@ -292,7 +292,7 @@ bool gcc_cmdlinet::parse_arguments(
         if(argv_i==*o) // separated
         {
           found=true;
-          if(next!=args.end())
+          if(next != args_to_parse.end())
           {
             set(argv_i, *next);
             ++it;
@@ -364,7 +364,7 @@ bool gcc_cmdlinet::parse_arguments(
         if(argv_i==*o) // separated
         {
           found=true;
-          if(next!=args.end())
+          if(next != args_to_parse.end())
           {
             set(argv_i, *next);
             if(!in_spec_file)
@@ -390,7 +390,7 @@ bool gcc_cmdlinet::parse_arguments(
         if(argv_i==*o) // separated
         {
           found=true;
-          if(next!=args.end())
+          if(next != args_to_parse.end())
           {
             set(argv_i, *next);
             if(!in_spec_file)
@@ -438,17 +438,17 @@ void gcc_cmdlinet::parse_specs_line(const std::string &line, bool in_spec_file)
   assert(!line.empty());
   assert(line[0]!=' ' && line[0]!='\t');
 
-  argst args;
+  argst args_from_specs;
 
   for(std::string::size_type arg_start=0, arg_end=0;
       arg_end!=std::string::npos;
       arg_start=line.find_first_not_of("\t ", arg_end))
   {
     arg_end=line.find_first_of("\t ", arg_start);
-    args.push_back(line.substr(arg_start, arg_end-arg_start));
+    args_from_specs.push_back(line.substr(arg_start, arg_end - arg_start));
   }
 
-  parse_arguments(args, in_spec_file);
+  parse_arguments(args_from_specs, in_spec_file);
 }
 
 /// Parse GCC spec files https://gcc.gnu.org/onlinedocs/gcc/Spec-Files.html
diff --git a/src/goto-cc/gcc_cmdline.h b/src/goto-cc/gcc_cmdline.h
index 6afc77fd39f..fe72c6e61cb 100644
--- a/src/goto-cc/gcc_cmdline.h
+++ b/src/goto-cc/gcc_cmdline.h
@@ -29,7 +29,7 @@ class gcc_cmdlinet:public goto_cc_cmdlinet
 protected:
   typedef std::vector<std::string> argst;
 
-  bool parse_arguments(const argst &args, bool in_spec_file);
+  bool parse_arguments(const argst &args_to_parse, bool in_spec_file);
   void parse_specs();
   void parse_specs_line(const std::string &line, bool in_spec_file);
 };
diff --git a/src/goto-cc/gcc_version.cpp b/src/goto-cc/gcc_version.cpp
index 832f9be8512..e900944ad00 100644
--- a/src/goto-cc/gcc_version.cpp
+++ b/src/goto-cc/gcc_version.cpp
@@ -95,7 +95,7 @@ void gcc_versiont::get(const std::string &executable)
         out << "default_cxx_standard __cplusplus\n";
       }
 
-      int result = run(
+      result = run(
         executable,
         {executable, "-E", "-x", "c++", "-", "-o", "-"},
         cpp_in(),
@@ -104,10 +104,9 @@ void gcc_versiont::get(const std::string &executable)
 
       if(result >= 0)
       {
-        std::ifstream in(cpp_out());
-        std::string line;
+        std::ifstream in2(cpp_out());
 
-        while(!in.fail() && std::getline(in, line))
+        while(!in2.fail() && std::getline(in2, line))
         {
           if(line.empty() || line[0] == '#')
             continue;
diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp
index 154e7137bca..0fa28a6a8c5 100644
--- a/src/goto-cc/linker_script_merge.cpp
+++ b/src/goto-cc/linker_script_merge.cpp
@@ -105,7 +105,7 @@ int linker_script_merget::add_linker_script_definitions()
     return fail;
   }
 
-  fail = compiler.write_object_file(goto_binary, original_goto_model);
+  fail = compiler.write_bin_object_file(goto_binary, original_goto_model);
 
   if(fail!=0)
     error() << "Could not write linkerscript-augmented binary" << eom;
diff --git a/src/goto-cc/ms_cl_cmdline.cpp b/src/goto-cc/ms_cl_cmdline.cpp
index 85cf0221c29..ad1df7e69de 100644
--- a/src/goto-cc/ms_cl_cmdline.cpp
+++ b/src/goto-cc/ms_cl_cmdline.cpp
@@ -47,48 +47,46 @@ const char *non_ms_cl_options[]=
   nullptr
 };
 
-bool ms_cl_cmdlinet::parse(const std::vector<std::string> &options)
+bool ms_cl_cmdlinet::parse(const std::vector<std::string> &arguments)
 {
-  for(std::size_t i=0; i<options.size(); i++)
+  for(std::size_t i = 0; i < arguments.size(); i++)
   {
     // is it a non-cl option?
-    if(std::string(options[i], 0, 2)=="--")
+    if(std::string(arguments[i], 0, 2) == "--")
     {
-      process_non_cl_option(options[i]);
+      process_non_cl_option(arguments[i]);
 
-      if(options[i]=="--verbosity" ||
-         options[i]=="--function")
+      if(arguments[i] == "--verbosity" || arguments[i] == "--function")
       {
-        if(i<options.size()-1)
+        if(i < arguments.size() - 1)
         {
-          set(options[i], options[i+1]);
+          set(arguments[i], arguments[i + 1]);
           i++; // skip ahead
         }
       }
     }
-    else if(!options[i].empty() && options[i][0]=='@')
+    else if(!arguments[i].empty() && arguments[i][0] == '@')
     {
       // potentially recursive
-      process_response_file(
-        std::string(options[i], 1, std::string::npos));
+      process_response_file(std::string(arguments[i], 1, std::string::npos));
     }
-    else if(options[i]=="/link" ||
-            options[i]=="-link")
+    else if(arguments[i] == "/link" || arguments[i] == "-link")
     {
       // anything that follows goes to the linker
-      i=options.size()-1;
+      i = arguments.size() - 1;
     }
-    else if(options[i].size()==2 &&
-            (options[i]=="/D" || options[i]=="-D") &&
-            i!=options.size()-1)
+    else if(
+      arguments[i].size() == 2 &&
+      (arguments[i] == "/D" || arguments[i] == "-D") &&
+      i != arguments.size() - 1)
     {
       // this requires special treatment, as you can do "/D something"
-      std::string tmp="/D"+options[i+1];
+      std::string tmp = "/D" + arguments[i + 1];
       i++;
       process_cl_option(tmp);
     }
     else
-      process_cl_option(options[i]);
+      process_cl_option(arguments[i]);
   }
 
   return false;
@@ -123,13 +121,13 @@ bool ms_cl_cmdlinet::parse(int argc, const char **argv)
 {
   // should really use "wide" argv from wmain()
 
-  std::vector<std::string> options;
+  std::vector<std::string> arguments;
 
   // skip argv[0]
   for(int i=1; i<argc; i++)
-    options.push_back(argv[i]);
+    arguments.push_back(argv[i]);
 
-  return parse(options);
+  return parse(arguments);
 }
 
 static std::istream &my_wgetline(std::istream &in, std::wstring &dest)
@@ -242,7 +240,7 @@ void ms_cl_cmdlinet::process_response_file_line(const std::string &line)
   if(line[0]=='#')
     return; // comment
 
-  std::vector<std::string> options;
+  std::vector<std::string> arguments;
   std::string option;
   bool in_quotes=false;
   for(std::size_t i=0; i<line.size(); i++)
@@ -252,7 +250,7 @@ void ms_cl_cmdlinet::process_response_file_line(const std::string &line)
     if(ch==' ' && !in_quotes)
     {
       if(!option.empty())
-        options.push_back(option);
+        arguments.push_back(option);
       option.clear();
     }
     else if(ch=='"')
@@ -264,9 +262,9 @@ void ms_cl_cmdlinet::process_response_file_line(const std::string &line)
   }
 
   if(!option.empty())
-    options.push_back(option);
+    arguments.push_back(option);
 
-  parse(options);
+  parse(arguments);
 }
 
 /// \return none
diff --git a/src/goto-cc/ms_link_cmdline.cpp b/src/goto-cc/ms_link_cmdline.cpp
index 315fd030942..543128d7897 100644
--- a/src/goto-cc/ms_link_cmdline.cpp
+++ b/src/goto-cc/ms_link_cmdline.cpp
@@ -28,31 +28,31 @@ const char *non_ms_link_options[]=
   "--verbosity"
 };
 
-bool ms_link_cmdlinet::parse(const std::vector<std::string> &options)
+bool ms_link_cmdlinet::parse(const std::vector<std::string> &arguments)
 {
-  for(std::size_t i = 0; i < options.size(); i++)
+  for(std::size_t i = 0; i < arguments.size(); i++)
   {
     // is it a non-link option?
-    if(std::string(options[i], 0, 2) == "--")
+    if(std::string(arguments[i], 0, 2) == "--")
     {
-      process_non_link_option(options[i]);
+      process_non_link_option(arguments[i]);
 
-      if(options[i] == "--verbosity")
+      if(arguments[i] == "--verbosity")
       {
-        if(i < options.size() - 1)
+        if(i < arguments.size() - 1)
         {
-          set(options[i], options[i + 1]);
+          set(arguments[i], arguments[i + 1]);
           i++; // skip ahead
         }
       }
     }
-    else if(!options[i].empty() && options[i][0] == '@')
+    else if(!arguments[i].empty() && arguments[i][0] == '@')
     {
       // potentially recursive
-      process_response_file(std::string(options[i], 1, std::string::npos));
+      process_response_file(std::string(arguments[i], 1, std::string::npos));
     }
     else
-      process_link_option(options[i]);
+      process_link_option(arguments[i]);
   }
 
   return false;
@@ -65,13 +65,13 @@ bool ms_link_cmdlinet::parse(int argc, const char **argv)
 {
   // should really use "wide" argv from wmain()
 
-  std::vector<std::string> options;
+  std::vector<std::string> arguments;
 
   // skip argv[0]
   for(int i = 1; i < argc; i++)
-    options.push_back(argv[i]);
+    arguments.push_back(argv[i]);
 
-  return parse(options);
+  return parse(arguments);
 }
 
 static std::istream &my_wgetline(std::istream &in, std::wstring &dest)
@@ -182,7 +182,7 @@ void ms_link_cmdlinet::process_response_file_line(const std::string &line)
   if(line[0] == '#')
     return; // comment
 
-  std::vector<std::string> options;
+  std::vector<std::string> arguments;
   std::string option;
   bool in_quotes = false;
   for(std::size_t i = 0; i < line.size(); i++)
@@ -192,7 +192,7 @@ void ms_link_cmdlinet::process_response_file_line(const std::string &line)
     if(ch == ' ' && !in_quotes)
     {
       if(!option.empty())
-        options.push_back(option);
+        arguments.push_back(option);
       option.clear();
     }
     else if(ch == '"')
@@ -204,9 +204,9 @@ void ms_link_cmdlinet::process_response_file_line(const std::string &line)
   }
 
   if(!option.empty())
-    options.push_back(option);
+    arguments.push_back(option);
 
-  parse(options);
+  parse(arguments);
 }
 
 /// \return none