Remove names of unused parameters

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -165,23 +165,23 @@ std::set<std::string> java_bytecode_languaget::extensions() const
   return { "class", "jar" };
 }
 
-void java_bytecode_languaget::modules_provided(std::set<std::string> &modules)
+void java_bytecode_languaget::modules_provided(std::set<std::string> &)
 {
   // modules.insert(translation_unit(parse_path));
 }
 
 /// ANSI-C preprocessing
 bool java_bytecode_languaget::preprocess(
-  std::istream &instream,
-  const std::string &path,
-  std::ostream &outstream)
+  std::istream &,
+  const std::string &,
+  std::ostream &)
 {
   // there is no preprocessing!
   return true;
 }
 
 bool java_bytecode_languaget::parse(
-  std::istream &instream,
+  std::istream &,
   const std::string &path)
 {
   PRECONDITION(language_options_initialized);
@@ -601,7 +601,7 @@ static void create_stub_global_symbols(
 
 bool java_bytecode_languaget::typecheck(
   symbol_tablet &symbol_table,
-  const std::string &module)
+  const std::string &)
 {
   PRECONDITION(language_options_initialized);
 
@@ -1089,7 +1089,7 @@ bool java_bytecode_languaget::convert_single_method(
   return true;
 }
 
-bool java_bytecode_languaget::final(symbol_table_baset &symbol_table)
+bool java_bytecode_languaget::final(symbol_table_baset &)
 {
   PRECONDITION(language_options_initialized);
   return false;

jbmc/src/java_bytecode/java_types.h

@@ -93,7 +93,7 @@ inline annotated_typet &to_annotated_type(typet &type)
 }
 
 template <>
-inline bool can_cast_type<annotated_typet>(const typet &type)
+inline bool can_cast_type<annotated_typet>(const typet &)
 {
   return true;
 }

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -616,7 +616,7 @@ void remove_exceptions(
   remove_exceptions_typest type)
 {
   remove_exceptionst::function_may_throwt any_function_may_throw =
-    [](const irep_idt &id) { return true; };
+    [](const irep_idt &) { return true; };
 
   remove_exceptionst remove_exceptions(
     symbol_table,

src/analyses/ai.cpp

@@ -319,7 +319,7 @@ bool ai_baset::do_function_call(
   locationt l_call, locationt l_return,
   const goto_functionst &goto_functions,
   const goto_functionst::function_mapt::const_iterator f_it,
-  const exprt::operandst &arguments,
+  const exprt::operandst &,
   const namespacet &ns)
 {
   // initialize state, if necessary

src/analyses/ai.h

@@ -385,10 +385,10 @@ private:
 
   // not implemented in sequential analyses
   bool merge_shared(
-    const statet &src,
-    goto_programt::const_targett from,
-    goto_programt::const_targett to,
-    const namespacet &ns) override
+    const statet &,
+    goto_programt::const_targett,
+    goto_programt::const_targett,
+    const namespacet &) override
   {
     throw "not implemented";
   }

src/analyses/constant_propagator.cpp

@@ -224,7 +224,7 @@ void constant_propagator_domaint::transform(
 /// handles equalities and conjunctions containing equalities
 bool constant_propagator_domaint::two_way_propagate_rec(
   const exprt &expr,
-  const namespacet &ns,
+  const namespacet &,
   const constant_propagator_ait *cp)
 {
 #ifdef DEBUG
@@ -391,7 +391,7 @@ void constant_propagator_domaint::valuest::output(
 
 void constant_propagator_domaint::output(
   std::ostream &out,
-  const ai_baset &ai,
+  const ai_baset &,
   const namespacet &ns) const
 {
   values.output(out, ns);
@@ -503,8 +503,8 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src)
 /// \return Return true if "this" has changed.
 bool constant_propagator_domaint::merge(
   const constant_propagator_domaint &other,
-  locationt from,
-  locationt to)
+  locationt,
+  locationt)
 {
   return values.merge(other.values);
 }

src/analyses/custom_bitvector_analysis.cpp

@@ -545,7 +545,7 @@ void custom_bitvector_domaint::transform(
 void custom_bitvector_domaint::output(
   std::ostream &out,
   const ai_baset &ai,
-  const namespacet &ns) const
+  const namespacet &) const
 {
   if(has_values.is_known())
   {
@@ -591,8 +591,8 @@ void custom_bitvector_domaint::output(
 
 bool custom_bitvector_domaint::merge(
   const custom_bitvector_domaint &b,
-  locationt from,
-  locationt to)
+  locationt,
+  locationt)
 {
   bool changed=has_values.is_false();
   has_values=tvt::unknown();

src/analyses/dependence_graph.cpp

@@ -24,8 +24,8 @@ Date: August 2013
 
 bool dep_graph_domaint::merge(
   const dep_graph_domaint &src,
-  goto_programt::const_targett from,
-  goto_programt::const_targett to)
+  goto_programt::const_targett,
+  goto_programt::const_targett)
 {
   // An abstract state at location `to` may be non-bottom even if
   // `merge(..., `to`) has not been called so far. This is due to the special
@@ -151,7 +151,7 @@ static bool may_be_def_use_pair(
 }
 
 void dep_graph_domaint::data_dependencies(
-  goto_programt::const_targett from,
+  goto_programt::const_targett,
   goto_programt::const_targett to,
   dependence_grapht &dep_graph,
   const namespacet &ns)
@@ -237,8 +237,8 @@ void dep_graph_domaint::transform(
 
 void dep_graph_domaint::output(
   std::ostream &out,
-  const ai_baset &ai,
-  const namespacet &ns) const
+  const ai_baset &,
+  const namespacet &) const
 {
   if(!control_deps.empty())
   {
@@ -275,8 +275,8 @@ void dep_graph_domaint::output(
 /// \par parameters: The abstract interpreter and the namespace.
 /// \return The domain, formatted as a JSON object.
 jsont dep_graph_domaint::output_json(
-  const ai_baset &ai,
-  const namespacet &ns) const
+  const ai_baset &,
+  const namespacet &) const
 {
   json_arrayt graph;
 

src/analyses/escape_analysis.cpp

@@ -163,9 +163,9 @@ void escape_domaint::get_rhs_aliases_address_of(
 
 void escape_domaint::transform(
   locationt from,
-  locationt to,
-  ai_baset &ai,
-  const namespacet &ns)
+  locationt,
+  ai_baset &,
+  const namespacet &)
 {
   if(has_values.is_false())
     return;
@@ -255,8 +255,8 @@ void escape_domaint::transform(
 
 void escape_domaint::output(
   std::ostream &out,
-  const ai_baset &ai,
-  const namespacet &ns) const
+  const ai_baset &,
+  const namespacet &) const
 {
   if(has_values.is_known())
   {
@@ -301,8 +301,8 @@ void escape_domaint::output(
 
 bool escape_domaint::merge(
   const escape_domaint &b,
-  locationt from,
-  locationt to)
+  locationt,
+  locationt)
 {
   bool changed=has_values.is_false();
   has_values=tvt::unknown();

src/analyses/escape_analysis.h

@@ -112,7 +112,7 @@ public:
   void instrument(goto_modelt &);
 
 protected:
-  virtual void initialize(const goto_functionst &_goto_functions)
+  virtual void initialize(const goto_functionst &)
   {
   }
 

src/analyses/flow_insensitive_analysis.cpp

@@ -77,8 +77,8 @@ void flow_insensitive_analysis_baset::output(
 }
 
 void flow_insensitive_analysis_baset::output(
-  const goto_programt &goto_program,
-  const irep_idt &identifier,
+  const goto_programt &,
+  const irep_idt &,
   std::ostream &out) const
 {
   get_state().output(ns, out);
@@ -199,7 +199,7 @@ bool flow_insensitive_analysis_baset::do_function_call(
   locationt l_call,
   const goto_functionst &goto_functions,
   const goto_functionst::function_mapt::const_iterator f_it,
-  const exprt::operandst &arguments,
+  const exprt::operandst &,
   statet &state)
 {
   const goto_functionst::goto_functiont &goto_function=f_it->second;
@@ -405,14 +405,12 @@ bool flow_insensitive_analysis_baset::fixedpoint(
   return fixedpoint(it->second.body, goto_functions);
 }
 
-void flow_insensitive_analysis_baset::update(
-  const goto_functionst &goto_functions)
+void flow_insensitive_analysis_baset::update(const goto_functionst &)
 {
   // no need to copy value sets around
 }
 
-void flow_insensitive_analysis_baset::update(
-  const goto_programt &goto_program)
+void flow_insensitive_analysis_baset::update(const goto_programt &)
 {
   // no need to copy value sets around
 }

src/analyses/flow_insensitive_analysis.h

@@ -44,16 +44,16 @@ public:
   }
 
   virtual void output(
-    const namespacet &ns,
-    std::ostream &out) const
+    const namespacet &,
+    std::ostream &) const
   {
   }
 
   typedef std::unordered_set<exprt, irep_hash> expr_sett;
 
   virtual void get_reference_set(
-    const namespacet &ns,
-    const exprt &expr,
+    const namespacet &,
+    const exprt &,
     expr_sett &expr_set)
   {
     // dummy, overload me!
@@ -95,8 +95,7 @@ public:
   {
   }
 
-  virtual void initialize(
-    const goto_programt &goto_program)
+  virtual void initialize(const goto_programt &)
   {
     if(!initialized)
     {
@@ -104,8 +103,7 @@ public:
     }
   }
 
-  virtual void initialize(
-    const goto_functionst &goto_functions)
+  virtual void initialize(const goto_functionst &)
   {
     if(!initialized)
     {

src/analyses/global_may_alias.cpp

@@ -77,9 +77,9 @@ void global_may_alias_domaint::get_rhs_aliases_address_of(
 
 void global_may_alias_domaint::transform(
   locationt from,
-  locationt to,
-  ai_baset &ai,
-  const namespacet &ns)
+  locationt,
+  ai_baset &,
+  const namespacet &)
 {
   if(has_values.is_false())
     return;
@@ -120,8 +120,8 @@ void global_may_alias_domaint::transform(
 
 void global_may_alias_domaint::output(
   std::ostream &out,
-  const ai_baset &ai,
-  const namespacet &ns) const
+  const ai_baset &,
+  const namespacet &) const
 {
   if(has_values.is_known())
   {
@@ -158,8 +158,8 @@ void global_may_alias_domaint::output(
 
 bool global_may_alias_domaint::merge(
   const global_may_alias_domaint &b,
-  locationt from,
-  locationt to)
+  locationt,
+  locationt)
 {
   bool changed=has_values.is_false();
   has_values=tvt::unknown();

src/analyses/global_may_alias.h

@@ -87,7 +87,7 @@ private:
 class global_may_alias_analysist:public ait<global_may_alias_domaint>
 {
 protected:
-  virtual void initialize(const goto_functionst &_goto_functions)
+  virtual void initialize(const goto_functionst &)
   {
   }
 };

src/analyses/goto_rw.cpp

@@ -34,8 +34,7 @@ range_domain_baset::~range_domain_baset()
 {
 }
 
-void range_domaint::output(
-  const namespacet &ns, std::ostream &out) const
+void range_domaint::output(const namespacet &, std::ostream &out) const
 {
   out << "[";
   for(const_iterator itr=begin();
@@ -123,8 +122,8 @@ void rw_range_sett::get_objects_if(
 void rw_range_sett::get_objects_dereference(
   get_modet mode,
   const dereference_exprt &deref,
-  const range_spect &range_start,
-  const range_spect &size)
+  const range_spect &,
+  const range_spect &)
 {
   const exprt &pointer=deref.pointer();
   get_objects_rec(get_modet::READ, pointer);

src/analyses/goto_rw.h

@@ -141,7 +141,7 @@ public:
   enum class get_modet { LHS_W, READ };
 
   virtual void get_objects_rec(
-    goto_programt::const_targett _target,
+    goto_programt::const_targett,
     get_modet mode,
     const exprt &expr)
   {

src/analyses/interval_domain.cpp

@@ -22,8 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 void interval_domaint::output(
   std::ostream &out,
-  const ai_baset &ai,
-  const namespacet &ns) const
+  const ai_baset &,
+  const namespacet &) const
 {
   if(bottom)
   {
@@ -59,7 +59,7 @@ void interval_domaint::output(
 void interval_domaint::transform(
   locationt from,
   locationt to,
-  ai_baset &ai,
+  ai_baset &,
   const namespacet &ns)
 {
   const goto_programt::instructiont &instruction=*from;

src/analyses/interval_domain.h

@@ -47,8 +47,8 @@ protected:
 public:
   bool merge(
     const interval_domaint &b,
-    locationt from,
-    locationt to)
+    locationt,
+    locationt)
   {
     return join(b);
   }

src/analyses/invariant_set.cpp

@@ -884,7 +884,7 @@ exprt invariant_sett::get_constant(const exprt &expr) const
 
 std::string inv_object_storet::to_string(
   unsigned a,
-  const irep_idt &identifier) const
+  const irep_idt &) const
 {
   return id2string(map[a]);
 }

src/analyses/invariant_set_domain.cpp

@@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 void invariant_set_domaint::transform(
   locationt from_l,
   locationt to_l,
-  ai_baset &ai,
+  ai_baset &,
   const namespacet &ns)
 {
   switch(from_l->type)

src/analyses/invariant_set_domain.h

@@ -31,8 +31,8 @@ public:
 
   bool merge(
     const invariant_set_domaint &other,
-    locationt from,
-    locationt to)
+    locationt,
+    locationt)
   {
     bool changed=invariant_set.make_union(other.invariant_set) ||
                  has_values.is_false();
@@ -43,8 +43,8 @@ public:
 
   void output(
     std::ostream &out,
-    const ai_baset &ai,
-    const namespacet &ns) const final override
+    const ai_baset &,
+    const namespacet &) const final override
   {
     if(has_values.is_known())
       out << has_values.to_string() << '\n';

src/analyses/is_threaded.cpp

@@ -30,8 +30,8 @@ public:
 
   bool merge(
     const is_threaded_domaint &src,
-    locationt from,
-    locationt to)
+    locationt,
+    locationt)
   {
     INVARIANT(src.reachable,
               "Abstract states are only merged at reachable locations");
@@ -47,7 +47,7 @@ public:
   }
 
   void
-  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
+  transform(locationt from, locationt, ai_baset &, const namespacet &)
     final override
   {
     INVARIANT(reachable,

src/analyses/reaching_definitions.cpp

@@ -125,7 +125,7 @@ void rd_range_domaint::transform(
 }
 
 void rd_range_domaint::transform_dead(
-  const namespacet &ns,
+  const namespacet &,
   locationt from)
 {
   const irep_idt &identifier=
@@ -430,7 +430,7 @@ void rd_range_domaint::kill(
 }
 
 void rd_range_domaint::kill_inf(
-  const irep_idt &identifier,
+  const irep_idt &,
   const range_spect &range_start)
 {
   assert(range_start>=0);
@@ -628,8 +628,8 @@ bool rd_range_domaint::merge_inner(
 /// \return returns true iff there is something new
 bool rd_range_domaint::merge(
   const rd_range_domaint &other,
-  locationt from,
-  locationt to)
+  locationt,
+  locationt)
 {
   bool changed=has_values.is_false();
   has_values=tvt::unknown();
@@ -664,8 +664,8 @@ bool rd_range_domaint::merge(
 /// \return returns true iff there is something new
 bool rd_range_domaint::merge_shared(
   const rd_range_domaint &other,
-  goto_programt::const_targett from,
-  goto_programt::const_targett to,
+  goto_programt::const_targett,
+  goto_programt::const_targett,
   const namespacet &ns)
 {
   // TODO: dirty vars

src/analyses/reaching_definitions.h

@@ -119,8 +119,8 @@ public:
 
   void output(
     std::ostream &out,
-    const ai_baset &ai,
-    const namespacet &ns) const final override
+    const ai_baset &,
+    const namespacet &) const final override
   {
     output(out);
   }

src/analyses/static_analysis.cpp

@@ -93,7 +93,7 @@ void static_analysis_baset::output(
 
 void static_analysis_baset::output(
   const goto_programt &goto_program,
-  const irep_idt &identifier,
+  const irep_idt &,
   std::ostream &out) const
 {
   forall_goto_program_instructions(i_it, goto_program)
@@ -248,7 +248,7 @@ void static_analysis_baset::do_function_call(
   locationt l_call, locationt l_return,
   const goto_functionst &goto_functions,
   const goto_functionst::function_mapt::const_iterator f_it,
-  const exprt::operandst &arguments,
+  const exprt::operandst &,
   statet &new_state)
 {
   const goto_functionst::goto_functiont &goto_function=f_it->second;

src/analyses/static_analysis.h

@@ -43,8 +43,8 @@ public:
   // will go away,
   // to be replaced by a factory class option to static_analysist
   virtual void initialize(
-    const namespacet &ns,
-    locationt l)
+    const namespacet &,
+    locationt)
   {
   }
 
@@ -62,8 +62,8 @@ public:
     locationt to)=0;
 
   virtual void output(
-    const namespacet &ns,
-    std::ostream &out) const
+    const namespacet &,
+    std::ostream &) const
   {
   }
 
@@ -71,8 +71,8 @@ public:
 
   // will go away
   virtual void get_reference_set(
-    const namespacet &ns,
-    const exprt &expr,
+    const namespacet &,
+    const exprt &,
     std::list<exprt> &dest)
   {
     // dummy, overload me!
@@ -363,9 +363,9 @@ private:
 
   // not implemented in sequential analyses
   virtual bool merge_shared(
-    statet &a,
-    const statet &b,
-    goto_programt::const_targett to)
+    statet &,
+    const statet &,
+    goto_programt::const_targett)
   {
     throw "not implemented";
   }

src/analyses/uncaught_exceptions_analysis.cpp

@@ -59,7 +59,7 @@ void uncaught_exceptions_domaint::join(
 void uncaught_exceptions_domaint::transform(
   const goto_programt::const_targett from,
   uncaught_exceptions_analysist &uea,
-  const namespacet &ns)
+  const namespacet &)
 {
   const goto_programt::instructiont &instruction=*from;
 

src/analyses/uninitialized_domain.cpp

@@ -20,8 +20,8 @@ Date: January 2010
 
 void uninitialized_domaint::transform(
   locationt from,
-  locationt to,
-  ai_baset &ai,
+  locationt,
+  ai_baset &,
   const namespacet &ns)
 {
   if(has_values.is_false())
@@ -67,8 +67,8 @@ void uninitialized_domaint::assign(const exprt &lhs)
 
 void uninitialized_domaint::output(
   std::ostream &out,
-  const ai_baset &ai,
-  const namespacet &ns) const
+  const ai_baset &,
+  const namespacet &) const
 {
   if(has_values.is_known())
     out << has_values.to_string() << '\n';
@@ -82,8 +82,8 @@ void uninitialized_domaint::output(
 /// \return returns true iff there is something new
 bool uninitialized_domaint::merge(
   const uninitialized_domaint &other,
-  locationt from,
-  locationt to)
+  locationt,
+  locationt)
 {
   auto old_uninitialized=uninitialized.size();
 

src/ansi-c/ansi_c_language.cpp

@@ -180,7 +180,7 @@ bool ansi_c_languaget::type_to_name(
 
 bool ansi_c_languaget::to_expr(
   const std::string &code,
-  const std::string &module,
+  const std::string &,
   exprt &expr,
   const namespacet &ns)
 {

src/ansi-c/c_typecheck_code.cpp

@@ -565,7 +565,7 @@ void c_typecheck_baset::typecheck_gcc_switch_case_range(codet &code)
   make_constant(code.op1());
 }
 
-void c_typecheck_baset::typecheck_gcc_local_label(codet &code)
+void c_typecheck_baset::typecheck_gcc_local_label(codet &)
 {
   // these are just declarations, e.g.,
   // __label__ here, there;

src/ansi-c/c_typecheck_expr.cpp

@@ -2797,7 +2797,7 @@ void c_typecheck_baset::typecheck_function_call_arguments(
   }
 }
 
-void c_typecheck_baset::typecheck_expr_constant(exprt &expr)
+void c_typecheck_baset::typecheck_expr_constant(exprt &)
 {
   // nothing to do
 }

src/cpp/cpp_declarator_converter.cpp

@@ -582,7 +582,7 @@ irep_idt cpp_declarator_convertert::get_pretty_name()
 }
 
 void cpp_declarator_convertert::operator_overloading_rules(
-  const symbolt &symbol)
+  const symbolt &)
 {
 }
 

src/cpp/cpp_language.cpp

@@ -229,7 +229,7 @@ bool cpp_languaget::from_type(
 bool cpp_languaget::type_to_name(
   const typet &type,
   std::string &name,
-  const namespacet &ns)
+  const namespacet &)
 {
   name=cpp_type2name(type);
   return false;
@@ -237,7 +237,7 @@ bool cpp_languaget::type_to_name(
 
 bool cpp_languaget::to_expr(
   const std::string &code,
-  const std::string &module,
+  const std::string &,
   exprt &expr,
   const namespacet &ns)
 {

src/cpp/cpp_typecheck.h

@@ -379,7 +379,7 @@ protected:
 
   void put_compound_into_scope(const struct_union_typet::componentt &component);
   void typecheck_compound_body(symbolt &symbol);
-  void typecheck_compound_body(struct_union_typet &type) { UNREACHABLE; }
+  void typecheck_compound_body(struct_union_typet &) { UNREACHABLE; }
   void typecheck_enum_body(symbolt &symbol);
   void typecheck_method_bodies();
   void typecheck_compound_bases(struct_typet &type);

src/cpp/cpp_typecheck_expr.cpp

@@ -1084,7 +1084,7 @@ void cpp_typecheckt::typecheck_expr_delete(exprt &expr)
   expr.set(ID_destructor, destructor_code);
 }
 
-void cpp_typecheckt::typecheck_expr_typecast(exprt &expr)
+void cpp_typecheckt::typecheck_expr_typecast(exprt &)
 {
   // should not be called
   #if 0

src/goto-cc/linker_script_merge.cpp

@@ -129,7 +129,7 @@ linker_script_merget::linker_script_merget(
       replacement_predicatet("address of array's first member",
         [](const exprt &expr) -> const symbol_exprt&
         { return to_symbol_expr(expr.op0().op0()); },
-        [](const exprt &expr, const namespacet &ns)
+        [](const exprt &expr, const namespacet &)
         {
           return expr.id()==ID_address_of &&
                  expr.type().id()==ID_pointer &&
@@ -146,7 +146,7 @@ linker_script_merget::linker_script_merget(
       replacement_predicatet("address of array",
         [](const exprt &expr) -> const symbol_exprt&
         { return to_symbol_expr(expr.op0()); },
-        [](const exprt &expr, const namespacet &ns)
+        [](const exprt &expr, const namespacet &)
         {
           return expr.id()==ID_address_of &&
                  expr.type().id()==ID_pointer &&
@@ -168,7 +168,7 @@ linker_script_merget::linker_script_merget(
       replacement_predicatet("array variable",
         [](const exprt &expr) -> const symbol_exprt&
         { return to_symbol_expr(expr); },
-        [](const exprt &expr, const namespacet &ns)
+        [](const exprt &expr, const namespacet &)
         {
           return expr.id()==ID_symbol &&
                  expr.type().id()==ID_array;
@@ -176,7 +176,7 @@ linker_script_merget::linker_script_merget(
       replacement_predicatet("pointer (does not need pointerizing)",
         [](const exprt &expr) -> const symbol_exprt&
         { return to_symbol_expr(expr); },
-        [](const exprt &expr, const namespacet &ns)
+        [](const exprt &expr, const namespacet &)
         {
           return expr.id()==ID_symbol &&
                  expr.type().id()==ID_pointer;

src/goto-instrument/accelerate/accelerate.cpp

@@ -457,7 +457,7 @@ symbolt acceleratet::make_symbol(std::string name, typet type)
   return ret;
 }
 
-void acceleratet::decl(symbol_exprt &sym, goto_programt::targett t)
+void acceleratet::decl(symbol_exprt &, goto_programt::targett)
 {
 #if 0
   goto_programt::targett decl=program.insert_before(t);

src/goto-instrument/cover_instrument_condition.cpp

@@ -19,7 +19,7 @@ Author: Daniel Kroening
 void cover_condition_instrumentert::instrument(
   goto_programt &goto_program,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &basic_blocks) const
+  const cover_blocks_baset &) const
 {
   if(is_non_cover_assertion(i_it))
     i_it->make_skip();

src/goto-instrument/cover_instrument_decision.cpp

@@ -18,7 +18,7 @@ Author: Daniel Kroening
 void cover_decision_instrumentert::instrument(
   goto_programt &goto_program,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &basic_blocks) const
+  const cover_blocks_baset &) const
 {
   if(is_non_cover_assertion(i_it))
     i_it->make_skip();

src/goto-instrument/cover_instrument_mcdc.cpp

@@ -623,7 +623,7 @@ void minimize_mcdc_controlling(
 void cover_mcdc_instrumentert::instrument(
   goto_programt &goto_program,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &basic_blocks) const
+  const cover_blocks_baset &) const
 {
   if(is_non_cover_assertion(i_it))
     i_it->make_skip();

src/goto-instrument/cover_instrument_other.cpp

@@ -16,9 +16,9 @@ Author: Daniel Kroening
 #include "cover_util.h"
 
 void cover_path_instrumentert::instrument(
-  goto_programt &goto_program,
+  goto_programt &,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &basic_blocks) const
+  const cover_blocks_baset &) const
 {
   if(is_non_cover_assertion(i_it))
     i_it->make_skip();
@@ -27,9 +27,9 @@ void cover_path_instrumentert::instrument(
 }
 
 void cover_assertion_instrumentert::instrument(
-  goto_programt &goto_program,
+  goto_programt &,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &basic_blocks) const
+  const cover_blocks_baset &) const
 {
   // turn into 'assert(false)' to avoid simplification
   if(is_non_cover_assertion(i_it))
@@ -41,9 +41,9 @@ void cover_assertion_instrumentert::instrument(
 }
 
 void cover_cover_instrumentert::instrument(
-  goto_programt &goto_program,
+  goto_programt &,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &basic_blocks) const
+  const cover_blocks_baset &) const
 {
   // turn __CPROVER_cover(x) into 'assert(!x)'
   if(i_it->is_function_call())

src/goto-instrument/goto_program2code.cpp

@@ -1403,7 +1403,7 @@ goto_programt::const_targett goto_program2codet::convert_start_thread(
 
 goto_programt::const_targett goto_program2codet::convert_throw(
     goto_programt::const_targett target,
-    codet &dest)
+    codet &)
 {
   // this isn't really clear as throw is not supported in expr2cpp either
   UNREACHABLE;
@@ -1412,8 +1412,8 @@ goto_programt::const_targett goto_program2codet::convert_throw(
 
 goto_programt::const_targett goto_program2codet::convert_catch(
     goto_programt::const_targett target,
-    goto_programt::const_targett upper_bound,
-    codet &dest)
+    goto_programt::const_targett,
+    codet &)
 {
   // this isn't really clear as catch is not supported in expr2cpp either
   UNREACHABLE;

src/goto-instrument/horn_encoding.cpp

@@ -17,6 +17,6 @@ Date: June 2015
 
 void horn_encoding(
   const goto_modelt &,
-  std::ostream &out)
+  std::ostream &)
 {
 }

src/goto-instrument/rw_set.h

@@ -87,7 +87,7 @@ public:
   void output(std::ostream &out) const;
 
 protected:
-  virtual void track_deref(const entryt &entry, bool read) {}
+  virtual void track_deref(const entryt &, bool read) {}
   virtual void set_track_deref() {}
   virtual void reset_track_deref() {}
 

src/goto-instrument/wmm/event_graph.h

@@ -267,7 +267,7 @@ protected:
     std::map<unsigned, unsigned char> events_per_thread;
 
     /* for thread and filtering in backtrack */
-    virtual inline bool filtering(event_idt u)
+    virtual inline bool filtering(event_idt)
     {
       return false;
     }

src/goto-instrument/wmm/instrumenter_strategies.cpp

@@ -159,14 +159,14 @@ void inline instrumentert::instrument_one_event_per_cycle_inserter(
 }
 
 void inline instrumentert::instrument_one_read_per_cycle_inserter(
-  const std::set<event_grapht::critical_cyclet> &set_of_cycles)
+  const std::set<event_grapht::critical_cyclet> &)
 {
   /* TODO */
   throw "read first strategy not implemented yet";
 }
 
 void inline instrumentert::instrument_one_write_per_cycle_inserter(
-  const std::set<event_grapht::critical_cyclet> &set_of_cycles)
+  const std::set<event_grapht::critical_cyclet> &)
 {
   /* TODO */
   throw "write first strategy not implemented yet";

src/goto-programs/cfg.h

@@ -245,10 +245,10 @@ void cfg_baset<T, P, I>::compute_edges_catch(
 
 template<class T, typename P, typename I>
 void cfg_baset<T, P, I>::compute_edges_throw(
-  const goto_programt &goto_program,
-  const goto_programt::instructiont &instruction,
-  goto_programt::const_targett next_PC,
-  entryt &entry)
+  const goto_programt &,
+  const goto_programt::instructiont &,
+  goto_programt::const_targett,
+  entryt &)
 {
   // no (trivial) successors
 }
@@ -256,7 +256,7 @@ void cfg_baset<T, P, I>::compute_edges_throw(
 template<class T, typename P, typename I>
 void cfg_baset<T, P, I>::compute_edges_start_thread(
   const goto_programt &goto_program,
-  const goto_programt::instructiont &instruction,
+  const goto_programt::instructiont &,
   goto_programt::const_targett next_PC,
   entryt &entry)
 {
@@ -333,7 +333,7 @@ void cfg_baset<T, P, I>::compute_edges_function_call(
 
 template<class T, typename P, typename I>
 void procedure_local_cfg_baset<T, P, I>::compute_edges_function_call(
-  const goto_functionst &goto_functions,
+  const goto_functionst &,
   const goto_programt &goto_program,
   const goto_programt::instructiont &instruction,
   goto_programt::const_targett next_PC,

src/goto-programs/goto_convert.cpp

@@ -352,8 +352,8 @@ void goto_convertt::convert_label(
 }
 
 void goto_convertt::convert_gcc_local_label(
-  const codet &code,
-  goto_programt &dest)
+  const codet &,
+  goto_programt &)
 {
   // ignore for now
 }
@@ -712,8 +712,8 @@ void goto_convertt::convert_decl(
 }
 
 void goto_convertt::convert_decl_type(
-  const codet &code,
-  goto_programt &dest)
+  const codet &,
+  goto_programt &)
 {
   // we remove these
 }

src/goto-programs/goto_convert_class.h

@@ -193,7 +193,7 @@ protected:
     const exprt::operandst &arguments,
     goto_programt &dest);
 
-  virtual void do_function_call_symbol(const symbolt &symbol)
+  virtual void do_function_call_symbol(const symbolt &)
   {
   }
 

src/goto-programs/goto_trace.cpp

@@ -33,7 +33,7 @@ void goto_tracet::output(
 }
 
 void goto_trace_stept::output(
-  const namespacet &ns,
+  const namespacet &,
   std::ostream &out) const
 {
   out << "*** ";

src/goto-programs/string_instrumentation.cpp

@@ -635,9 +635,9 @@ void string_instrumentationt::do_format_string_write(
 }
 
 void string_instrumentationt::do_strncmp(
-  goto_programt &dest,
-  goto_programt::targett target,
-  code_function_callt &call)
+  goto_programt &,
+  goto_programt::targett,
+  code_function_callt &)
 {
 }
 

src/goto-programs/wp.cpp

@@ -218,7 +218,7 @@ exprt wp_assign(
 exprt wp_assume(
   const code_assumet &code,
   const exprt &post,
-  const namespacet &ns)
+  const namespacet &)
 {
   return implies_exprt(code.assumption(), post);
 }

src/goto-symex/goto_symex.h

@@ -338,7 +338,7 @@ protected:
   void pop_frame(statet &);
   void return_assignment(statet &);
 
-  virtual void no_body(const irep_idt &identifier)
+  virtual void no_body(const irep_idt &)
   {
   }
 

src/goto-symex/slice.cpp

@@ -26,7 +26,7 @@ void symex_slicet::get_symbols(const exprt &expr)
     depends.insert(to_symbol_expr(expr).get_identifier());
 }
 
-void symex_slicet::get_symbols(const typet &type)
+void symex_slicet::get_symbols(const typet &)
 {
   // TODO
 }

src/goto-symex/symex_builtin_functions.cpp

@@ -453,8 +453,8 @@ void goto_symext::symex_cpp_new(
 }
 
 void goto_symext::symex_cpp_delete(
-  statet &state,
-  const codet &code)
+  statet &,
+  const codet &)
 {
   // TODO
   #if 0
@@ -502,9 +502,10 @@ void goto_symext::symex_trace(
 }
 
 void goto_symext::symex_fkt(
-  statet &state,
-  const code_function_callt &code)
+  statet &,
+  const code_function_callt &)
 {
+  UNREACHABLE;
   #if 0
   exprt new_fc(ID_function, fc.type());
 
@@ -525,7 +526,7 @@ void goto_symext::symex_fkt(
 }
 
 void goto_symext::symex_macro(
-  statet &state,
+  statet &,
   const code_function_callt &code)
 {
   const irep_idt &identifier=code.op0().get(ID_identifier);

src/goto-symex/symex_catch.cpp

@@ -11,8 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
-void goto_symext::symex_catch(statet &state)
+void goto_symext::symex_catch(statet &)
 {
+  UNREACHABLE;
   // there are two variants: 'push' and 'pop'
 
   #if 0

src/goto-symex/symex_dereference_state.cpp

@@ -14,9 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/symbol_table.h>
 
 void symex_dereference_statet::dereference_failure(
-  const std::string &property,
-  const std::string &msg,
-  const guardt &guard)
+  const std::string &,
+  const std::string &,
+  const guardt &)
 {
 }
 

src/goto-symex/symex_function_call.cpp

@@ -18,9 +18,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/invariant.h>
 
 bool goto_symext::get_unwind_recursion(
-  const irep_idt &identifier,
-  const unsigned thread_nr,
-  unsigned unwind)
+  const irep_idt &,
+  const unsigned,
+  unsigned)
 {
   return false;
 }

src/goto-symex/symex_goto.cpp

@@ -539,9 +539,9 @@ void goto_symext::loop_bound_exceeded(
 }
 
 bool goto_symext::get_unwind(
-  const symex_targett::sourcet &source,
-  const goto_symex_statet::call_stackt &context,
-  unsigned unwind)
+  const symex_targett::sourcet &,
+  const goto_symex_statet::call_stackt &,
+  unsigned)
 {
   // by default, we keep going
   return false;

src/goto-symex/symex_target_equation.cpp

@@ -184,9 +184,9 @@ void symex_target_equationt::decl(
 
 /// declare a fresh variable
 void symex_target_equationt::dead(
-  const exprt &guard,
-  const ssa_exprt &ssa_lhs,
-  const sourcet &source)
+  const exprt &,
+  const ssa_exprt &,
+  const sourcet &)
 {
   // we currently don't record these
 }

src/jsil/jsil_language.cpp

@@ -42,9 +42,9 @@ bool jsil_languaget::interfaces(symbol_tablet &symbol_table)
 }
 
 bool jsil_languaget::preprocess(
-  std::istream &instream,
-  const std::string &path,
-  std::ostream &outstream)
+  std::istream &,
+  const std::string &,
+  std::ostream &)
 {
   // there is no preprocessing!
   return true;
@@ -78,7 +78,7 @@ bool jsil_languaget::parse(
 /// Converting from parse tree and type checking.
 bool jsil_languaget::typecheck(
   symbol_tablet &symbol_table,
-  const std::string &module)
+  const std::string &)
 {
   if(jsil_typecheck(symbol_table, get_message_handler()))
     return true;
@@ -124,7 +124,7 @@ bool jsil_languaget::from_type(
 
 bool jsil_languaget::to_expr(
   const std::string &code,
-  const std::string &module,
+  const std::string &,
   exprt &expr,
   const namespacet &ns)
 {

src/jsil/jsil_typecheck.cpp

@@ -922,7 +922,7 @@ bool jsil_typecheck(
 bool jsil_typecheck(
   exprt &expr,
   message_handlert &message_handler,
-  const namespacet &ns)
+  const namespacet &)
 {
   const unsigned errors_before=
     message_handler.get_message_count(messaget::M_ERROR);

src/jsil/jsil_typecheck.h

@@ -56,7 +56,7 @@ protected:
 
   void update_expr_type(exprt &expr, const typet &type);
   void make_type_compatible(exprt &expr, const typet &type, bool must);
-  void typecheck_type_symbol(symbolt &symbol) {}
+  void typecheck_type_symbol(symbolt &) {}
   void typecheck_non_type_symbol(symbolt &symbol);
   void typecheck_symbol_expr(symbol_exprt &symbol_expr);
   void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr);

src/langapi/language.cpp

@@ -18,26 +18,26 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/cprover_prefix.h>
 #include <util/std_types.h>
 
-bool languaget::final(symbol_table_baset &symbol_table)
+bool languaget::final(symbol_table_baset &)
 {
   return false;
 }
 
-bool languaget::interfaces(symbol_tablet &symbol_table)
+bool languaget::interfaces(symbol_tablet &)
 {
   return false;
 }
 
 void languaget::dependencies(
-  const std::string &module,
-  std::set<std::string> &modules)
+  const std::string &,
+  std::set<std::string> &)
 {
 }
 
 bool languaget::from_expr(
   const exprt &expr,
   std::string &code,
-  const namespacet &ns)
+  const namespacet &)
 {
   code=expr.pretty();
   return false;
@@ -46,7 +46,7 @@ bool languaget::from_expr(
 bool languaget::from_type(
   const typet &type,
   std::string &code,
-  const namespacet &ns)
+  const namespacet &)
 {
   code=type.pretty();
   return false;
@@ -55,7 +55,7 @@ bool languaget::from_type(
 bool languaget::type_to_name(
   const typet &type,
   std::string &name,
-  const namespacet &ns)
+  const namespacet &)
 {
   // probably ansi-c/type2name could be used as better fallback if moved to
   // util/

src/langapi/language_ui.cpp

@@ -140,7 +140,7 @@ void language_uit::show_symbol_table(bool brief)
   }
 }
 
-void language_uit::show_symbol_table_xml_ui(bool brief)
+void language_uit::show_symbol_table_xml_ui(bool)
 {
   error() << "cannot show symbol table in this format" << eom;
 }

src/pointer-analysis/value_set.h

@@ -533,7 +533,7 @@ protected:
   /// originated in a particular place, vs. those that have been copied.
   virtual void adjust_assign_rhs_values(
     const exprt &rhs,
-    const namespacet &ns,
+    const namespacet &,
     object_mapt &rhs_values) const
   {
   }
@@ -545,7 +545,7 @@ protected:
   virtual void apply_assign_side_effects(
     const exprt &lhs,
     const exprt &rhs,
-    const namespacet &ns)
+    const namespacet &)
   {
   }
 };

src/pointer-analysis/value_set_domain.h

@@ -25,7 +25,7 @@ public:
 
   // overloading
 
-  bool merge(const value_set_domain_templatet<VST> &other, locationt to)
+  bool merge(const value_set_domain_templatet<VST> &other, locationt)
   {
     return value_set.make_union(other.value_set);
   }
@@ -38,7 +38,7 @@ public:
   }
 
   virtual void initialize(
-    const namespacet &ns,
+    const namespacet &,
     locationt l)
   {
     value_set.clear();

src/pointer-analysis/value_set_domain_fi.h

@@ -36,8 +36,7 @@ public:
     value_set.output(ns, out);
   }
 
-  virtual void initialize(
-    const namespacet &ns)
+  virtual void initialize(const namespacet &)
   {
     value_set.clear();
   }

src/pointer-analysis/value_set_domain_fivr.h

@@ -32,7 +32,7 @@ public:
   }
 
   virtual void initialize(
-    const namespacet &ns)
+    const namespacet &)
   {
     value_set.clear();
   }

src/pointer-analysis/value_set_domain_fivrns.h

@@ -33,7 +33,7 @@ public:
   }
 
   virtual void initialize(
-    const namespacet &ns)
+    const namespacet &)
   {
     value_set.clear();
   }

src/solvers/flattening/arrays.cpp

@@ -573,8 +573,8 @@ void arrayst::add_array_constraints_with(
 }
 
 void arrayst::add_array_constraints_update(
-  const index_sett &index_set,
-  const update_exprt &expr)
+  const index_sett &,
+  const update_exprt &)
 {
   // we got x=UPDATE(y, [i], v)
   // add constaint x[i]=v

src/solvers/floatbv/float_utils.cpp

@@ -1305,14 +1305,14 @@ bvt float_utilst::sticky_right_shift(
 
 bvt float_utilst::debug1(
   const bvt &src1,
-  const bvt &src2)
+  const bvt &)
 {
   return src1;
 }
 
 bvt float_utilst::debug2(
   const bvt &op0,
-  const bvt &op1)
+  const bvt &)
 {
   return op0;
 }

src/solvers/prop/prop.h

@@ -82,12 +82,12 @@ public:
   virtual bool cnf_handled_well() const { return true; }
 
   // assumptions
-  virtual void set_assumptions(const bvt &_assumptions) { }
+  virtual void set_assumptions(const bvt &) { }
   virtual bool has_set_assumptions() const { return false; }
 
   // variables
   virtual literalt new_variable()=0;
-  virtual void set_variable_name(literalt a, const irep_idt &name) { }
+  virtual void set_variable_name(literalt, const irep_idt &) { }
   virtual size_t no_variables() const=0;
   bvt new_variables(std::size_t width);
 
@@ -108,10 +108,10 @@ public:
   virtual bool has_is_in_conflict() const { return false; }
 
   // an incremental solver may remove any variables that aren't frozen
-  virtual void set_frozen(literalt a) { }
+  virtual void set_frozen(literalt) { }
 
   // Resource limits:
-  virtual void set_time_limit_seconds(uint32_t lim)
+  virtual void set_time_limit_seconds(uint32_t)
   {
     warning() << "CPU limit ignored (not implemented)" << eom;
   }

src/solvers/prop/prop_conv.cpp

@@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <algorithm>
 
 /// determine whether a variable is in the final conflict
-bool prop_convt::is_in_conflict(literalt l) const
+bool prop_convt::is_in_conflict(literalt) const
 {
   UNREACHABLE;
   return false;

src/solvers/qbf/qbf_quantor.cpp

@@ -20,7 +20,7 @@ qbf_quantort::~qbf_quantort()
 {
 }
 
-tvt qbf_quantort::l_get(literalt a) const
+tvt qbf_quantort::l_get(literalt) const
 {
   assert(false);
   return tvt::unknown();

src/solvers/qbf/qbf_qube.cpp

@@ -22,7 +22,7 @@ qbf_qubet::~qbf_qubet()
 {
 }
 
-tvt qbf_qubet::l_get(literalt a) const
+tvt qbf_qubet::l_get(literalt) const
 {
   assert(false);
   return tvt(false);

src/solvers/qbf/qbf_qube_core.cpp

@@ -129,12 +129,12 @@ propt::resultt qbf_qube_coret::prop_solve()
   }
 }
 
-bool qbf_qube_coret::is_in_core(literalt l) const
+bool qbf_qube_coret::is_in_core(literalt) const
 {
   throw "not supported";
 }
 
-qdimacs_coret::modeltypet qbf_qube_coret::m_get(literalt a) const
+qdimacs_coret::modeltypet qbf_qube_coret::m_get(literalt) const
 {
   throw "not supported";
 }

src/solvers/qbf/qbf_qube_core.h

@@ -49,7 +49,7 @@ public:
 
   virtual modeltypet m_get(literalt a) const;
 
-  virtual const exprt f_get(literalt l)
+  virtual const exprt f_get(literalt)
   {
     throw "qube does not support full certificates.";
   }

src/solvers/qbf/qbf_skizzo.cpp

@@ -22,7 +22,7 @@ qbf_skizzot::~qbf_skizzot()
 {
 }
 
-tvt qbf_skizzot::l_get(literalt a) const
+tvt qbf_skizzot::l_get(literalt) const
 {
   assert(false);
   return tvt(false);

src/solvers/refinement/string_builtin_function.h

@@ -470,7 +470,7 @@ public:
   }
 
   optionalt<exprt>
-  eval(const std::function<exprt(const exprt &)> &get_value) const override
+  eval(const std::function<exprt(const exprt &)> &) const override
   {
     return {};
   }

src/solvers/sat/cnf_clause_list.h

@@ -31,7 +31,7 @@ public:
   virtual const std::string solver_text()
   { return "CNF clause list"; }
 
-  virtual tvt l_get(literalt literal) const
+  virtual tvt l_get(literalt) const
   {
     return tvt::unknown();
   }

src/solvers/sat/dimacs_cnf.cpp

@@ -19,12 +19,12 @@ dimacs_cnft::dimacs_cnft():break_lines(false)
 {
 }
 
-void dimacs_cnft::set_assignment(literalt a, bool value)
+void dimacs_cnft::set_assignment(literalt, bool)
 {
   UNIMPLEMENTED;
 }
 
-bool dimacs_cnft::is_in_conflict(literalt l) const
+bool dimacs_cnft::is_in_conflict(literalt) const
 {
   UNREACHABLE;
   return false;

src/solvers/smt2/smt2_conv.cpp

@@ -4069,7 +4069,7 @@ void smt2_convt::unflatten(
   }
 }
 
-void smt2_convt::convert_overflow(const exprt &expr)
+void smt2_convt::convert_overflow(const exprt &)
 {
   UNREACHABLE;
 }

src/solvers/smt2/smt2_conv.h

@@ -108,7 +108,7 @@ public:
 
   // overloading interfaces
   virtual literalt convert(const exprt &expr);
-  virtual void set_frozen(literalt a) { /* not needed */ }
+  virtual void set_frozen(literalt) { /* not needed */ }
   virtual void set_to(const exprt &expr, bool value);
   virtual exprt get(const exprt &expr) const;
   virtual std::string decision_procedure_text() const { return "SMT2"; }

src/solvers/smt2/smt2_parser.cpp

@@ -280,8 +280,8 @@ exprt smt2_parsert::quantifier_expression(irep_idt id)
 }
 
 exprt smt2_parsert::function_application(
-  const irep_idt &identifier,
-  const exprt::operandst &op)
+  const irep_idt &,
+  const exprt::operandst &)
 {
   #if 0
   const auto &f = id_map[identifier];

src/util/bv_arithmetic.cpp

@@ -52,7 +52,7 @@ void bv_arithmetict::print(std::ostream &out) const
   out << to_ansi_c_string();
 }
 
-std::string bv_arithmetict::format(const format_spect &format_spec) const
+std::string bv_arithmetict::format(const format_spect &) const
 {
   std::string result;
 

src/util/cout_message.cpp

@@ -100,7 +100,7 @@ void console_message_handlert::flush(unsigned level)
 void gcc_message_handlert::print(
   unsigned level,
   const std::string &message,
-  int sequence_number,
+  int,
   const source_locationt &location)
 {
   const irep_idt file=location.get_file();

src/util/expr.h

@@ -162,14 +162,14 @@ class expr_visitort
 {
 public:
   virtual ~expr_visitort() { }
-  virtual void operator()(exprt &expr) { }
+  virtual void operator()(exprt &) { }
 };
 
 class const_expr_visitort
 {
 public:
   virtual ~const_expr_visitort() { }
-  virtual void operator()(const exprt &expr) { }
+  virtual void operator()(const exprt &) { }
 };
 
 #endif // CPROVER_UTIL_EXPR_H

src/util/message.cpp

@@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 void message_handlert::print(
   unsigned level,
   const std::string &message,
-  int sequence_number,
+  int,
   const source_locationt &location)
 {
   std::string dest;
@@ -58,7 +58,7 @@ void message_handlert::print(
 
 void message_handlert::print(
   unsigned level,
-  const std::string &message)
+  const std::string &)
 {
   if(level>=message_count.size())
     message_count.resize(level+1, 0);

src/util/message.h

@@ -89,8 +89,8 @@ public:
   virtual void print(
     unsigned level,
     const std::string &message,
-    int sequence_number,
-    const source_locationt &location)
+    int,
+    const source_locationt &)
   {
     print(level, message);
   }

src/util/parser.cpp

@@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "parser.h"
 
 #ifdef _WIN32
-int isatty(int f)
+int isatty(int)
 {
   return 0;
 }

src/util/simplify_expr.cpp

@@ -1251,7 +1251,7 @@ bool simplify_exprt::get_values(
   return true;
 }
 
-bool simplify_exprt::simplify_lambda(exprt &expr)
+bool simplify_exprt::simplify_lambda(exprt &)
 {
   bool result=true;
 

src/util/ui_message.cpp

@@ -264,7 +264,7 @@ void ui_message_handlert::ui_msg(
 void ui_message_handlert::xml_ui_msg(
   const std::string &type,
   const std::string &msg1,
-  const std::string &msg2,
+  const std::string &,
   const source_locationt &location)
 {
   xmlt result;
@@ -287,7 +287,7 @@ void ui_message_handlert::xml_ui_msg(
 void ui_message_handlert::json_ui_msg(
   const std::string &type,
   const std::string &msg1,
-  const std::string &msg2,
+  const std::string &,
   const source_locationt &location)
 {
   INVARIANT(json_stream, "JSON stream must be initialized before use");