Silence warnings about unused parameters

Their names are useful to understand the purpose of the function and/or are part
of Doxygen documentation, and thus cannot be removed.

Author: tautschnig

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;
   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;
   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;
   binary_relation_exprt is_bmp(chr, ID_le, from_integer(0xFFFF, chr.type()));
   return is_bmp;
 }
@@ -423,6 +426,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;
   // The following intervals are undefined in unicode, according to
   // the Unicode Character Database: http://www.unicode.org/Public/UCD/latest/
   exprt::operandst intervals;
@@ -487,6 +491,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;
   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);
@@ -525,6 +530,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;
   return in_interval_expr(chr, 0xD800, 0xDBFF);
 }
 
@@ -549,6 +555,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;
   or_exprt ignorable(
     in_interval_expr(chr, 0x0000, 0x0008),
      or_exprt(
@@ -776,6 +783,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;
   return in_list_expr(chr, {0x28, 0x29, 0x3C, 0x3E, 0x5B, 0x5D, 0x7B, 0x7D});
 }
 
@@ -818,6 +826,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;
   std::list<mp_integer> space_characters=
     {0x20, 0x00A0, 0x1680, 0x202F, 0x205F, 0x3000, 0x2028, 0x2029};
   exprt condition0=in_list_expr(chr, space_characters);
@@ -852,6 +861,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;
   return binary_relation_exprt(chr, ID_gt, from_integer(0xFFFF, chr.type()));
 }
 
@@ -872,6 +882,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;
   return in_interval_expr(chr, 0xD800, 0xDFFF);
 }
 
@@ -908,6 +919,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;
   std::list<mp_integer>title_case_chars=
     {0x01C5, 0x01C8, 0x01CB, 0x01F2, 0x1FBC, 0x1FCC, 0x1FFC};
   exprt::operandst conditions;
@@ -945,6 +957,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;
   // The following set of characters is the general category "Nl" in the
   // Unicode specification.
   exprt cond0=in_interval_expr(chr, 0x16EE, 0x16F0);
@@ -1058,6 +1071,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;
   return binary_relation_exprt(chr, ID_le, from_integer(0x10FFFF, chr.type()));
 }
 
@@ -1082,6 +1096,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;
   exprt::operandst conditions;
   std::list<mp_integer> space_characters=
     {0x20, 0x1680, 0x205F, 0x3000, 0x2028, 0x2029};

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1157,6 +1157,11 @@ bool java_bytecode_languaget::to_expr(
   java_bytecode_parser.clear();
 
   return result;
+  #else
+  (void)code;
+  (void)module;
+  (void)expr;
+  (void)ns;
   #endif
 
   return true; // fail for now

jbmc/src/java_bytecode/java_bytecode_typecheck.cpp

@@ -119,6 +119,10 @@ bool java_bytecode_typecheck(
   }
 
   return java_bytecode_typecheck.get_error_found();
+  #else
+  (void)expr;
+  (void)message_handler;
+  (void)ns;
   #endif
 
   // fail for now

jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp

@@ -35,6 +35,8 @@ tvt java_enum_static_init_unwind_handler(
   unsigned &unwind_max,
   const symbol_tablet &symbol_table)
 {
+  (void)loop_number;
+
   const std::string &function_str = id2string(function_id);
   if(!has_suffix(function_str, ".<clinit>:()V"))
     return tvt::unknown();

jbmc/src/java_bytecode/java_local_variable_table.cpp

@@ -538,6 +538,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;
 #endif
 
   // Nuke the now-subsumed var-table entries:

src/analyses/ai.h

@@ -114,6 +114,7 @@ class ai_domain_baset
     exprt &condition,
     const namespacet &ns) const
   {
+    (void)condition;
     return true;
   }
 

src/analyses/constant_propagator.cpp

@@ -229,6 +229,8 @@ bool constant_propagator_domaint::two_way_propagate_rec(
 {
 #ifdef DEBUG
   std::cout << "two_way_propagate_rec: " << format(expr) << '\n';
+#else
+  (void)expr;
 #endif
 
   bool change=false;
@@ -260,6 +262,8 @@ bool constant_propagator_domaint::two_way_propagate_rec(
        assign_rec(values, rhs, lhs, ns);
     change=values.meet(copy_values);
   }
+#else
+  (void)cp;
 #endif
 
 #ifdef DEBUG

src/analyses/local_may_alias.cpp

@@ -328,6 +328,7 @@ void local_may_aliast::build(const goto_functiont &goto_function)
 
   loc_infos.resize(cfg.nodes.size());
 
+  (void)goto_function;
   #if 0
   // feed in sufficiently bad defaults
   for(code_typet::parameterst::const_iterator

src/analyses/uncaught_exceptions_analysis.cpp

@@ -183,6 +183,7 @@ void uncaught_exceptions_analysist::collect_uncaught_exceptions(
 void uncaught_exceptions_analysist::output(
   const goto_functionst &goto_functions) const
 {
+  (void)goto_functions;
 #ifdef DEBUG
   forall_goto_functions(it, goto_functions)
   {

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -747,6 +747,8 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     // add generic checks
     status() << "Generic Property Instrumentation" << eom;
     goto_check(options, goto_model);
+    #else
+    (void)options;
     #endif
 
     // recalculate numbers, etc.