diff --git a/jbmc/src/java_bytecode/character_refine_preprocess.cpp b/jbmc/src/java_bytecode/character_refine_preprocess.cpp
index b4c313075c1..b127409c562 100644
--- a/jbmc/src/java_bytecode/character_refine_preprocess.cpp
+++ b/jbmc/src/java_bytecode/character_refine_preprocess.cpp
@@ -338,6 +338,7 @@ codet character_refine_preprocesst::convert_high_surrogate(
 exprt character_refine_preprocesst::expr_of_is_ascii_lower_case(
   const exprt &chr, const typet &type)
 {
+  (void)type; // unused parameter
   return in_interval_expr(chr, 'a', 'z');
 }
 
@@ -348,6 +349,7 @@ exprt character_refine_preprocesst::expr_of_is_ascii_lower_case(
 exprt character_refine_preprocesst::expr_of_is_ascii_upper_case(
   const exprt &chr, const typet &type)
 {
+  (void)type; // unused parameter
   return in_interval_expr(chr, 'A', 'Z');
 }
 
@@ -402,6 +404,7 @@ codet character_refine_preprocesst::convert_is_alphabetic(
 exprt character_refine_preprocesst::expr_of_is_bmp_code_point(
   const exprt &chr, const typet &type)
 {
+  (void)type; // unused parameter
   return and_exprt(
     binary_relation_exprt(chr, ID_le, from_integer(0xFFFF, chr.type())),
     binary_relation_exprt(chr, ID_ge, from_integer(0, chr.type())));
@@ -424,6 +427,7 @@ codet character_refine_preprocesst::convert_is_bmp_code_point(
 exprt character_refine_preprocesst::expr_of_is_defined(
   const exprt &chr, const typet &type)
 {
+  (void)type; // unused parameter
   // The following intervals are undefined in unicode, according to
   // the Unicode Character Database: http://www.unicode.org/Public/UCD/latest/
   exprt::operandst intervals;
@@ -488,6 +492,7 @@ codet character_refine_preprocesst::convert_is_defined_int(
 exprt character_refine_preprocesst::expr_of_is_digit(
   const exprt &chr, const typet &type)
 {
+  (void)type; // unused parameter
   exprt latin_digit=in_interval_expr(chr, '0', '9');
   exprt arabic_indic_digit=in_interval_expr(chr, 0x660, 0x669);
   exprt extended_digit=in_interval_expr(chr, 0x6F0, 0x6F9);
@@ -526,6 +531,7 @@ codet character_refine_preprocesst::convert_is_digit_int(
 exprt character_refine_preprocesst::expr_of_is_high_surrogate(
   const exprt &chr, const typet &type)
 {
+  (void)type; // unused parameter
   return in_interval_expr(chr, 0xD800, 0xDBFF);
 }
 
@@ -550,6 +556,7 @@ codet character_refine_preprocesst::convert_is_high_surrogate(
 exprt character_refine_preprocesst::expr_of_is_identifier_ignorable(
   const exprt &chr, const typet &type)
 {
+  (void)type; // unused parameter
   or_exprt ignorable(
     in_interval_expr(chr, 0x0000, 0x0008),
      or_exprt(
@@ -777,6 +784,7 @@ codet character_refine_preprocesst::convert_is_low_surrogate(
 exprt character_refine_preprocesst::expr_of_is_mirrored(
   const exprt &chr, const typet &type)
 {
+  (void)type; // unused parameter
   return in_list_expr(chr, {0x28, 0x29, 0x3C, 0x3E, 0x5B, 0x5D, 0x7B, 0x7D});
 }
 
@@ -819,6 +827,7 @@ codet character_refine_preprocesst::convert_is_space(conversion_inputt &target)
 exprt character_refine_preprocesst::expr_of_is_space_char(
   const exprt &chr, const typet &type)
 {
+  (void)type; // unused parameter
   std::list<mp_integer> space_characters=
     {0x20, 0x00A0, 0x1680, 0x202F, 0x205F, 0x3000, 0x2028, 0x2029};
   exprt condition0=in_list_expr(chr, space_characters);
@@ -853,6 +862,7 @@ codet character_refine_preprocesst::convert_is_space_char_int(
 exprt character_refine_preprocesst::expr_of_is_supplementary_code_point(
   const exprt &chr, const typet &type)
 {
+  (void)type; // unused parameter
   return binary_relation_exprt(chr, ID_gt, from_integer(0xFFFF, chr.type()));
 }
 
@@ -873,6 +883,7 @@ codet character_refine_preprocesst::convert_is_supplementary_code_point(
 exprt character_refine_preprocesst::expr_of_is_surrogate(
   const exprt &chr, const typet &type)
 {
+  (void)type; // unused parameter
   return in_interval_expr(chr, 0xD800, 0xDFFF);
 }
 
@@ -909,6 +920,7 @@ codet character_refine_preprocesst::convert_is_surrogate_pair(
 exprt character_refine_preprocesst::expr_of_is_title_case(
   const exprt &chr, const typet &type)
 {
+  (void)type; // unused parameter
   std::list<mp_integer>title_case_chars=
     {0x01C5, 0x01C8, 0x01CB, 0x01F2, 0x1FBC, 0x1FCC, 0x1FFC};
   exprt::operandst conditions;
@@ -946,6 +958,7 @@ codet character_refine_preprocesst::convert_is_title_case_int(
 exprt character_refine_preprocesst::expr_of_is_letter_number(
   const exprt &chr, const typet &type)
 {
+  (void)type; // unused parameter
   // The following set of characters is the general category "Nl" in the
   // Unicode specification.
   exprt cond0=in_interval_expr(chr, 0x16EE, 0x16F0);
@@ -1059,6 +1072,7 @@ codet character_refine_preprocesst::convert_is_upper_case_int(
 exprt character_refine_preprocesst::expr_of_is_valid_code_point(
   const exprt &chr, const typet &type)
 {
+  (void)type; // unused parameter
   return binary_relation_exprt(chr, ID_le, from_integer(0x10FFFF, chr.type()));
 }
 
@@ -1083,6 +1097,7 @@ codet character_refine_preprocesst::convert_is_valid_code_point(
 exprt character_refine_preprocesst::expr_of_is_whitespace(
   const exprt &chr, const typet &type)
 {
+  (void)type; // unused parameter
   exprt::operandst conditions;
   std::list<mp_integer> space_characters=
     {0x20, 0x1680, 0x205F, 0x3000, 0x2028, 0x2029};
diff --git a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
index f7500891a9f..27413c16309 100644
--- a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
@@ -342,6 +342,7 @@ static void instrument_end_thread(
   const symbol_tablet &symbol_table)
 {
   PRECONDITION(f_code.arguments().size() == 1);
+  (void)symbol_table; // unused parameter
 
   // Build id, used to construct appropriate labels.
   // Note: java does not have labels so this should be safe
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp
index 0e7860469c7..2a897a1daef 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp
@@ -1198,7 +1198,7 @@ bool java_bytecode_languaget::to_expr(
   exprt &expr,
   const namespacet &ns)
 {
-  #if 0
+#if 0
   expr.make_nil();
 
   // no preprocessing yet...
@@ -1234,7 +1234,13 @@ bool java_bytecode_languaget::to_expr(
   java_bytecode_parser.clear();
 
   return result;
-  #endif
+#else
+  // unused parameters
+  (void)code;
+  (void)module;
+  (void)expr;
+  (void)ns;
+#endif
 
   return true; // fail for now
 }
@@ -1249,5 +1255,6 @@ java_bytecode_languaget::~java_bytecode_languaget()
 std::vector<load_extra_methodst>
 java_bytecode_languaget::build_extra_entry_points(const optionst &options) const
 {
+  (void)options; // unused parameter
   return {};
 }
diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck.cpp
index 78a56171060..4bb90c5f5a9 100644
--- a/jbmc/src/java_bytecode/java_bytecode_typecheck.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_typecheck.cpp
@@ -90,7 +90,7 @@ bool java_bytecode_typecheck(
   message_handlert &message_handler,
   const namespacet &ns)
 {
-  #if 0
+#if 0
   symbol_tablet symbol_table;
   java_bytecode_parse_treet java_bytecode_parse_tree;
 
@@ -119,7 +119,12 @@ bool java_bytecode_typecheck(
   }
 
   return java_bytecode_typecheck.get_error_found();
-  #endif
+#else
+  // unused parameters
+  (void)expr;
+  (void)message_handler;
+  (void)ns;
+#endif
 
   // fail for now
   return true;
diff --git a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp
index 9c69e5eb056..c8e5669be68 100644
--- a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp
+++ b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp
@@ -70,6 +70,8 @@ tvt java_enum_static_init_unwind_handler(
   unsigned &unwind_max,
   const symbol_tablet &symbol_table)
 {
+  (void)loop_number; // unused parameter
+
   const irep_idt enum_function_id = find_enum_function_on_stack(context);
   if(enum_function_id.empty())
     return tvt::unknown();
diff --git a/jbmc/src/java_bytecode/java_local_variable_table.cpp b/jbmc/src/java_bytecode/java_local_variable_table.cpp
index 9b880900cff..18127f2385b 100644
--- a/jbmc/src/java_bytecode/java_local_variable_table.cpp
+++ b/jbmc/src/java_bytecode/java_local_variable_table.cpp
@@ -549,6 +549,8 @@ static void merge_variable_table_entries(
             << merge_into.var.name << "; new live range "
             << merge_into.var.start_pc << '-'
             << merge_into.var.start_pc + merge_into.var.length << '\n';
+#else
+  (void)debug_out; // unused parameter
 #endif
 
   // Nuke the now-subsumed var-table entries:
diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp
index 5d6731b7c00..e0ec682857a 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.cpp
+++ b/jbmc/src/java_bytecode/select_pointer_type.cpp
@@ -29,6 +29,7 @@ pointer_typet select_pointer_typet::convert_pointer_type(
     &generic_parameter_specialization_map,
   const namespacet &ns) const
 {
+  (void)ns; // unused parameter
   // if we have a map of generic parameters -> types and the pointer is
   // a generic parameter, specialize it with concrete types
   if(!generic_parameter_specialization_map.empty())
@@ -229,5 +230,8 @@ std::set<symbol_typet> select_pointer_typet::get_parameter_alternative_types(
   const irep_idt &parameter_name,
   const namespacet &ns) const
 {
+  // unused parameters
+  (void)function_name;
+  (void)parameter_name;
   return {};
 }
diff --git a/src/analyses/ai_domain.h b/src/analyses/ai_domain.h
index 700103faee8..4cd9c562fb6 100644
--- a/src/analyses/ai_domain.h
+++ b/src/analyses/ai_domain.h
@@ -104,6 +104,7 @@ class ai_domain_baset
   /// return true if unchanged
   virtual bool ai_simplify(exprt &condition, const namespacet &ns) const
   {
+    (void)condition; // unused parameter
     return true;
   }
 
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index e30002d5ff5..18a69721e90 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -237,6 +237,8 @@ bool constant_propagator_domaint::two_way_propagate_rec(
 {
 #ifdef DEBUG
   std::cout << "two_way_propagate_rec: " << format(expr) << '\n';
+#else
+  (void)expr; // unused parameter
 #endif
 
   bool change=false;
@@ -268,6 +270,8 @@ bool constant_propagator_domaint::two_way_propagate_rec(
        assign_rec(values, rhs, lhs, ns);
     change = values.meet(copy_values, ns);
   }
+#else
+  (void)cp;   // unused parameter
 #endif
 
 #ifdef DEBUG
diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
index 5164db6e3bc..f853a6dced1 100644
--- a/src/analyses/local_may_alias.cpp
+++ b/src/analyses/local_may_alias.cpp
@@ -328,7 +328,8 @@ void local_may_aliast::build(const goto_functiont &goto_function)
 
   loc_infos.resize(cfg.nodes.size());
 
-  #if 0
+  (void)goto_function; // unused parameter
+#if 0
   // feed in sufficiently bad defaults
   for(code_typet::parameterst::const_iterator
       it=goto_function.type.parameters().begin();
@@ -340,9 +341,9 @@ void local_may_aliast::build(const goto_functiont &goto_function)
       loc_infos[0].points_to[objects.number(identifier)].objects.insert(
         unknown_object);
   }
-  #endif
+#endif
 
-  #if 0
+#if 0
   for(localst::locals_mapt::const_iterator
       l_it=locals.locals_map.begin();
       l_it!=locals.locals_map.end();
@@ -352,7 +353,7 @@ void local_may_aliast::build(const goto_functiont &goto_function)
       loc_infos[0].aliases.make_union(
         objects.number(l_it->second), unknown_object);
   }
-  #endif
+#endif
 
   while(!work_queue.empty())
   {
diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp
index cec22dd21fa..958660dee27 100644
--- a/src/analyses/uncaught_exceptions_analysis.cpp
+++ b/src/analyses/uncaught_exceptions_analysis.cpp
@@ -182,6 +182,7 @@ void uncaught_exceptions_analysist::collect_uncaught_exceptions(
 void uncaught_exceptions_analysist::output(
   const goto_functionst &goto_functions) const
 {
+  (void)goto_functions; // unused parameter
 #ifdef DEBUG
   forall_goto_functions(it, goto_functions)
   {
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index dc7b8a1e55e..ed46f902c5a 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -750,11 +750,13 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     remove_vector(goto_model);
     remove_complex(goto_model);
 
-    #if 0
+#if 0
     // add generic checks
     status() << "Generic Property Instrumentation" << eom;
     goto_check(options, goto_model);
-    #endif
+#else
+    (void)options; // unused parameter
+#endif
 
     // recalculate numbers, etc.
     goto_model.goto_functions.update();
diff --git a/src/goto-cc/hybrid_binary.cpp b/src/goto-cc/hybrid_binary.cpp
index 92ca21dd610..5f0730d7037 100644
--- a/src/goto-cc/hybrid_binary.cpp
+++ b/src/goto-cc/hybrid_binary.cpp
@@ -93,6 +93,10 @@ int hybrid_binary(
   }
 
 #else
+  // unused parameters
+  (void)compiler_or_linker;
+  (void)goto_binary_file;
+  (void)output_file;
   message.error() << "binary merging not implemented for this platform"
                   << messaget::eom;
   result = 1;
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
index 9c5a9d95f98..874b6f04639 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
@@ -450,6 +450,10 @@ bool polynomial_acceleratort::fit_const(
   exprt &target,
   polynomialt &poly)
 {
+  // unused parameters
+  (void)body;
+  (void)target;
+  (void)poly;
   return false;
 
 #if 0
diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp
index f2947ac231b..5104e13b7af 100644
--- a/src/goto-instrument/accelerate/scratch_program.cpp
+++ b/src/goto-instrument/accelerate/scratch_program.cpp
@@ -185,6 +185,7 @@ void scratch_programt::append_loop(
   append(program);
 
   // Update any back jumps to the loop header.
+  (void)loop_header; // unused parameter
   assume(false_exprt());
 
   goto_programt::targett end=add_instruction(SKIP);
diff --git a/src/goto-instrument/cover_basic_blocks.h b/src/goto-instrument/cover_basic_blocks.h
index b36da3039cf..607acf9b9a9 100644
--- a/src/goto-instrument/cover_basic_blocks.h
+++ b/src/goto-instrument/cover_basic_blocks.h
@@ -14,9 +14,9 @@ Author: Daniel Kroening
 
 #include <unordered_set>
 
-#include <goto-programs/goto_model.h>
+#include <util/message.h>
 
-class message_handlert;
+#include <goto-programs/goto_model.h>
 
 class cover_blocks_baset
 {
@@ -49,6 +49,9 @@ class cover_blocks_baset
     const goto_programt &goto_program,
     message_handlert &message_handler)
   {
+    // unused parameters
+    (void)goto_program;
+    (void)message_handler;
   }
 };
 
diff --git a/src/goto-instrument/cover_filter.cpp b/src/goto-instrument/cover_filter.cpp
index 2c9c6c3f6d6..f3c824cd8f2 100644
--- a/src/goto-instrument/cover_filter.cpp
+++ b/src/goto-instrument/cover_filter.cpp
@@ -51,6 +51,7 @@ bool include_pattern_filtert::operator()(
   const irep_idt &identifier,
   const goto_functionst::goto_functiont &goto_function) const
 {
+  (void)goto_function; // unused parameter
   std::smatch string_matcher;
   return std::regex_match(id2string(identifier), string_matcher, regex_matcher);
 }
@@ -67,6 +68,7 @@ bool trivial_functions_filtert::operator()(
   const irep_idt &identifier,
   const goto_functionst::goto_functiont &goto_function) const
 {
+  (void)identifier; // unused parameter
   unsigned long count_assignments = 0, count_goto = 0;
   forall_goto_program_instructions(i_it, goto_function.body)
   {
diff --git a/src/goto-instrument/full_slicer_class.h b/src/goto-instrument/full_slicer_class.h
index c700de2e4fb..ccd60107f00 100644
--- a/src/goto-instrument/full_slicer_class.h
+++ b/src/goto-instrument/full_slicer_class.h
@@ -99,6 +99,8 @@ class full_slicert
   {
 #ifdef DEBUG_FULL_SLICERT
     cfg[entry].required_by.insert(reason->location_number);
+#else
+    (void)reason; // unused parameter
 #endif
     queue.push(entry);
   }
diff --git a/src/goto-instrument/rw_set.h b/src/goto-instrument/rw_set.h
index 1c5e9fdb66b..842640c3106 100644
--- a/src/goto-instrument/rw_set.h
+++ b/src/goto-instrument/rw_set.h
@@ -87,7 +87,10 @@ class rw_set_baset
   void output(std::ostream &out) const;
 
 protected:
-  virtual void track_deref(const entryt &, bool read) {}
+  virtual void track_deref(const entryt &, bool read)
+  {
+    (void)read; // unused parameter
+  }
   virtual void set_track_deref() {}
   virtual void reset_track_deref() {}
 
diff --git a/src/goto-instrument/wmm/data_dp.cpp b/src/goto-instrument/wmm/data_dp.cpp
index d88f20859eb..f01bcf69896 100644
--- a/src/goto-instrument/wmm/data_dp.cpp
+++ b/src/goto-instrument/wmm/data_dp.cpp
@@ -185,5 +185,7 @@ void data_dpt::print(messaget &message)
     for(l_it=m_it->second.begin(); l_it!=m_it->second.end(); ++l_it)
       message.debug()<< "loc: "<<*l_it << messaget::eom;
   }
+#else
+  (void)message; // unused parameter
 #endif
 }
diff --git a/src/goto-instrument/wmm/instrumenter_strategies.cpp b/src/goto-instrument/wmm/instrumenter_strategies.cpp
index bd809a7a23f..6acf938246e 100644
--- a/src/goto-instrument/wmm/instrumenter_strategies.cpp
+++ b/src/goto-instrument/wmm/instrumenter_strategies.cpp
@@ -344,6 +344,7 @@ void inline instrumentert::instrument_minimum_interference_inserter(
 
   glp_delete_prob(lp);
 #else
+  (void)set_of_cycles; // unused parameter
   throw "sorry, minimum interference option requires glpk; "
         "please recompile goto-instrument with glpk";
 #endif
diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp
index 2f0ab8d23cf..39964ab9841 100644
--- a/src/goto-instrument/wmm/shared_buffers.cpp
+++ b/src/goto-instrument/wmm/shared_buffers.cpp
@@ -243,9 +243,8 @@ void shared_bufferst::flush_read(
   const source_locationt &source_location,
   const irep_idt &write_object)
 {
-/* option 1 */
-
 #if 0
+  // option 1
   const varst &vars=(*this)(write_object);
 
   const symbol_exprt fresh_var_expr=symbol_exprt(vars.read_new_var, vars.type);
@@ -266,10 +265,15 @@ void shared_bufferst::flush_read(
 
   assignment(goto_program, target, source_location, vars.read_delayed,
              false_exprt());
+#else
+  // option 2: do nothing
+  // unused parameters
+  (void)goto_program;
+  (void)target;
+  (void)target;
+  (void)source_location;
+  (void)write_object;
 #endif
-
-/* option 2 */
-/* do nothing */
 }
 
 /// instruments write
diff --git a/src/goto-programs/osx_fat_reader.cpp b/src/goto-programs/osx_fat_reader.cpp
index 6d543205aec..54c3e3fcc45 100644
--- a/src/goto-programs/osx_fat_reader.cpp
+++ b/src/goto-programs/osx_fat_reader.cpp
@@ -32,6 +32,8 @@ bool is_osx_fat_magic(char hdr[4])
     case FAT_CIGAM:
       return true;
   }
+#else
+  (void)hdr; // unused parameter
 #endif
 
   return false;
@@ -75,6 +77,8 @@ osx_fat_readert::osx_fat_readert(std::ifstream &in) :
                 cpusubtype==CPU_SUBTYPE_HPPA_7100LC &&
                 size > 0;
   }
+#else
+  (void)in;  // unused parameter
 #endif
 }
 
diff --git a/src/langapi/language.cpp b/src/langapi/language.cpp
index c75e810026c..4c43ce92ca0 100644
--- a/src/langapi/language.cpp
+++ b/src/langapi/language.cpp
@@ -115,6 +115,9 @@ irep_idt languaget::generate_opaque_stub_body(
   symbolt &symbol,
   symbol_tablet &symbol_table)
 {
+  // unused parameters
+  (void)symbol;
+  (void)symbol_table;
   return ID_nil;
 }
 
@@ -131,6 +134,10 @@ parameter_symbolt languaget::build_stub_parameter_symbol(
   size_t parameter_index,
   const code_typet::parametert &parameter)
 {
+  // unused parameters
+  (void)function_symbol;
+  (void)parameter_index;
+  (void)parameter;
   error() << "language " << id()
           << " doesn't implement build_stub_parameter_symbol. "
           << "This means cannot use opaque functions." << eom;
diff --git a/src/langapi/language.h b/src/langapi/language.h
index b9cdb4c50d3..ba98703748c 100644
--- a/src/langapi/language.h
+++ b/src/langapi/language.h
@@ -17,14 +17,14 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <string>
 #include <memory> // unique_ptr
 
-#include <util/symbol.h>
-#include <util/std_types.h>
 #include <util/message.h>
+#include <util/std_types.h>
+#include <util/symbol.h>
+#include <util/symbol_table_base.h>
 
 #include <goto-programs/system_library_symbols.h>
 
 class symbol_tablet;
-class symbol_table_baset;
 class exprt;
 class namespacet;
 class optionst;
@@ -49,7 +49,14 @@ class languaget:public messaget
   virtual bool preprocess(
     std::istream &instream,
     const std::string &path,
-    std::ostream &outstream) { return false; }
+    std::ostream &outstream)
+  {
+    // unused parameters
+    (void)instream;
+    (void)path;
+    (void)outstream;
+    return false;
+  }
 
   virtual bool parse(
     std::istream &instream,
@@ -75,18 +82,26 @@ class languaget:public messaget
   // add modules provided by currently parsed file to set
 
   virtual void modules_provided(std::set<std::string> &modules)
-  { }
+  {
+    (void)modules; // unused parameter
+  }
 
   // add lazy functions provided to set
 
   virtual void methods_provided(std::unordered_set<irep_idt> &methods) const
-  { }
+  {
+    (void)methods; // unused parameter
+  }
 
   // populate a lazy method
   virtual void
   convert_lazy_method(
     const irep_idt &function_id, symbol_table_baset &symbol_table)
-  { }
+  {
+    // unused parameters
+    (void)function_id;
+    (void)symbol_table;
+  }
 
   /// Final adjustments, e.g. initializing stub functions and globals that
   /// were discovered during function loading
diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index ecdd1187b47..433c553152a 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -532,6 +532,9 @@ class value_sett
     const namespacet &,
     object_mapt &rhs_values) const
   {
+    // unused parameters
+    (void)rhs;
+    (void)rhs_values;
   }
 
   /// Subclass customisation point to apply global side-effects to this domain,
@@ -543,6 +546,9 @@ class value_sett
     const exprt &rhs,
     const namespacet &)
   {
+    // unused parameters
+    (void)lhs;
+    (void)rhs;
   }
 };
 
diff --git a/src/util/memory_info.cpp b/src/util/memory_info.cpp
index 881d709c5d7..5eb531a5509 100644
--- a/src/util/memory_info.cpp
+++ b/src/util/memory_info.cpp
@@ -33,7 +33,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 void memory_info(std::ostream &out)
 {
-  #if defined(__linux__) && defined(__GLIBC__)
+#if defined(__linux__) && defined(__GLIBC__)
   // NOLINTNEXTLINE(readability/identifiers)
   struct mallinfo m = mallinfo();
   out << "  non-mmapped space allocated from system: " << m.arena << "\n";
@@ -45,20 +45,21 @@ void memory_info(std::ostream &out)
   out << "  space available in freed fastbin blocks: " << m.fsmblks << "\n";
   out << "  total allocated space: " << m.uordblks << "\n";
   out << "  total free space: " << m.fordblks << "\n";
-  #endif
+#endif
 
-  #ifdef _WIN32
-  #if 0
+#ifdef _WIN32
+  (void)out; // unused parameter
+#if 0
   PROCESS_MEMORY_COUNTERS pmc;
   if(GetProcessMemoryInfo(GetCurrentProcess(), &pmc, sizeof(pmc)))
   {
     out << "  PeakWorkingSetSize: " << pmc.PeakWorkingSetSize << "\n";
     out << "  WorkingSetSize: " << pmc.WorkingSetSize << "\n";
   }
-  #endif
-  #endif
+#endif
+#endif
 
-  #ifdef __APPLE__
+#ifdef __APPLE__
   // NOLINTNEXTLINE(readability/identifiers)
   struct task_basic_info t_info;
   mach_msg_type_number_t t_info_count = TASK_BASIC_INFO_COUNT;
@@ -73,5 +74,5 @@ void memory_info(std::ostream &out)
       << static_cast<double>(t.max_size_in_use)/1000000 << "m\n";
   out << "  size_allocated: "
       << static_cast<double>(t.size_allocated)/1000000 << "m\n";
-  #endif
+#endif
 }
diff --git a/src/util/signal_catcher.cpp b/src/util/signal_catcher.cpp
index 80422e55fd1..7e1c6f4f2e6 100644
--- a/src/util/signal_catcher.cpp
+++ b/src/util/signal_catcher.cpp
@@ -73,6 +73,7 @@ void remove_signal_catcher()
 void signal_catcher(int sig)
 {
 #if defined(_WIN32)
+  (void)sig; // unused parameter
 #else
 
 #if 0
diff --git a/src/util/tempdir.cpp b/src/util/tempdir.cpp
index 7a5b4527fd4..08f207fd6a1 100644
--- a/src/util/tempdir.cpp
+++ b/src/util/tempdir.cpp
@@ -39,53 +39,55 @@ std::string get_temporary_directory(const std::string &name_template)
 {
   std::string result;
 
-  #ifdef _WIN32
-    DWORD dwBufSize = MAX_PATH+1;
-    char lpPathBuffer[MAX_PATH+1];
-    DWORD dwRetVal = GetTempPathA(dwBufSize, lpPathBuffer);
-
-    if(dwRetVal > dwBufSize || (dwRetVal == 0))
-    {
-      throw system_exceptiont("Couldn't get temporary path");
-    }
-
-    // GetTempFileNameA produces <path>\<pre><uuuu>.TMP
-    // where <pre> = "TLO"
-    // Thus, we must make the buffer 1+3+4+1+3=12 characters longer.
-
-    char t[MAX_PATH];
-    UINT uRetVal=GetTempFileNameA(lpPathBuffer, "TLO", 0, t);
-    if(uRetVal == 0)
-    {
-      throw system_exceptiont(
-        std::string("Couldn't get new temporary file name in directory") +
-        lpPathBuffer);
-    }
-
-    unlink(t);
-    if(_mkdir(t) != 0)
-    {
-      throw system_exceptiont(
-        std::string("Couldn't create temporary directory at ") + t);
-    }
-    result=std::string(t);
-
-  #else
-    std::string prefixed_name_template="/tmp/";
-    const char *TMPDIR_env=getenv("TMPDIR");
-    if(TMPDIR_env!=nullptr)
-      prefixed_name_template=TMPDIR_env;
-    if(*prefixed_name_template.rbegin()!='/')
-      prefixed_name_template+='/';
-    prefixed_name_template+=name_template;
-
-    std::vector<char> t(prefixed_name_template.begin(), prefixed_name_template.end());
-    t.push_back('\0'); // add the zero
-    const char *td = mkdtemp(t.data());
-    if(!td)
-      throw system_exceptiont("Failed to create temporary directory");
-    result=std::string(td);
-  #endif
+#ifdef _WIN32
+  (void)name_template; // unused parameter
+  DWORD dwBufSize = MAX_PATH + 1;
+  char lpPathBuffer[MAX_PATH + 1];
+  DWORD dwRetVal = GetTempPathA(dwBufSize, lpPathBuffer);
+
+  if(dwRetVal > dwBufSize || (dwRetVal == 0))
+  {
+    throw system_exceptiont("Couldn't get temporary path");
+  }
+
+  // GetTempFileNameA produces <path>\<pre><uuuu>.TMP
+  // where <pre> = "TLO"
+  // Thus, we must make the buffer 1+3+4+1+3=12 characters longer.
+
+  char t[MAX_PATH];
+  UINT uRetVal = GetTempFileNameA(lpPathBuffer, "TLO", 0, t);
+  if(uRetVal == 0)
+  {
+    throw system_exceptiont(
+      std::string("Couldn't get new temporary file name in directory") +
+      lpPathBuffer);
+  }
+
+  unlink(t);
+  if(_mkdir(t) != 0)
+  {
+    throw system_exceptiont(
+      std::string("Couldn't create temporary directory at ") + t);
+  }
+  result = std::string(t);
+
+#else
+  std::string prefixed_name_template = "/tmp/";
+  const char *TMPDIR_env = getenv("TMPDIR");
+  if(TMPDIR_env != nullptr)
+    prefixed_name_template = TMPDIR_env;
+  if(*prefixed_name_template.rbegin() != '/')
+    prefixed_name_template += '/';
+  prefixed_name_template += name_template;
+
+  std::vector<char> t(
+    prefixed_name_template.begin(), prefixed_name_template.end());
+  t.push_back('\0'); // add the zero
+  const char *td = mkdtemp(t.data());
+  if(!td)
+    throw system_exceptiont("Failed to create temporary directory");
+  result = std::string(td);
+#endif
 
   return result;
 }
diff --git a/src/util/timestamper.cpp b/src/util/timestamper.cpp
index f063e041cf5..24895927fd6 100644
--- a/src/util/timestamper.cpp
+++ b/src/util/timestamper.cpp
@@ -19,6 +19,7 @@ std::unique_ptr<const timestampert>
 timestampert::make(timestampert::clockt clock_type)
 {
 #ifdef _WIN32
+  (void)clock_type; // unused parameter
   return std::unique_ptr<const timestampert>(new timestampert());
 #else
   switch(clock_type)