Improve documentation and omit two unused parameters

No functional changes intended here.

Author: smowton

src/java_bytecode/java_bytecode_instrument.cpp

@@ -29,15 +29,11 @@ class java_bytecode_instrumentt:public messaget
   java_bytecode_instrumentt(
     symbol_tablet &_symbol_table,
     const bool _throw_runtime_exceptions,
-    message_handlert &_message_handler,
-    const size_t _max_array_length,
-    const size_t _max_tree_depth):
+    message_handlert &_message_handler):
     messaget(_message_handler),
     symbol_table(_symbol_table),
     throw_runtime_exceptions(_throw_runtime_exceptions),
-    message_handler(_message_handler),
-    max_array_length(_max_array_length),
-    max_tree_depth(_max_tree_depth)
+    message_handler(_message_handler)
     {
     }
 
@@ -47,8 +43,6 @@ class java_bytecode_instrumentt:public messaget
   symbol_tablet &symbol_table;
   const bool throw_runtime_exceptions;
   message_handlert &message_handler;
-  const size_t max_array_length;
-  const size_t max_tree_depth;
 
   codet throw_exception(
     const exprt &cond,
@@ -570,28 +564,23 @@ void java_bytecode_instrumentt::operator()(exprt &expr)
 /// runtime exceptions or corresponding assertions.
 /// Exceptions are thrown when the `throw_runtime_exceptions` flag is set.
 /// Otherwise, assertions are emitted.
-/// \par parameters: `symbol_table`: global symbol table (may gain exception type
-///   stubs and similar)
-/// `symbol`: the symbol to instrument
-/// `throw_runtime_exceptions`: flag determining whether we instrument the code
-/// with runtime exceptions or with assertions. The former applies if this flag
-/// is set to true.
-/// `max_array_length`: maximum array length; the only reason we need this is
-/// in order to be able to call the object factory to create exceptions.
-void java_bytecode_instrument(
+/// \param symbol_table: global symbol table (may gain exception type stubs and
+///   similar)
+/// \param symbol: the symbol to instrument
+/// \param throw_runtime_exceptions: flag determining whether we instrument the
+///   code with runtime exceptions or with assertions. The former applies if
+///   this flag is set to true.
+/// \param message_handler: stream to report status and warnings
+void java_bytecode_instrument_symbol(
   symbol_tablet &symbol_table,
   symbolt &symbol,
   const bool throw_runtime_exceptions,
-  message_handlert &message_handler,
-  const size_t max_array_length,
-  const size_t max_tree_depth)
+  message_handlert &message_handler)
 {
   java_bytecode_instrumentt instrument(
     symbol_table,
     throw_runtime_exceptions,
-    message_handler,
-    max_array_length,
-    max_tree_depth);
+    message_handler);
   INVARIANT(
     symbol.value.id()==ID_code,
     "java_bytecode_instrument expects a code-typed symbol");
@@ -602,25 +591,21 @@ void java_bytecode_instrument(
 /// runtime exceptions or corresponding assertions.
 /// Exceptions are thrown when the `throw_runtime_exceptions` flag is set.
 /// Otherwise, assertions are emitted.
-/// \par parameters: `symbol_table`: the symbol table to instrument
-/// `throw_runtime_exceptions`: flag determining whether we instrument the code
-/// with runtime exceptions or with assertions. The former applies if this flag
-/// is set to true.
-/// `max_array_length`: maximum array length; the only reason we need this is
-/// in order to be able to call the object factory to create exceptions.
+/// \param symbol_table: global symbol table, all of whose code members
+///   will be annotated (may gain exception type stubs and similar)
+/// \param throw_runtime_exceptions: flag determining whether we instrument the
+///   code with runtime exceptions or with assertions. The former applies if
+///   this flag is set to true.
+/// \param message_handler: stream to report status and warnings
 void java_bytecode_instrument(
   symbol_tablet &symbol_table,
   const bool throw_runtime_exceptions,
-  message_handlert &message_handler,
-  const size_t max_array_length,
-  const size_t max_tree_depth)
+  message_handlert &message_handler)
 {
   java_bytecode_instrumentt instrument(
     symbol_table,
     throw_runtime_exceptions,
-    message_handler,
-    max_array_length,
-    max_tree_depth);
+    message_handler);
 
   std::vector<irep_idt> symbols_to_instrument;
   forall_symbols(s_it, symbol_table.symbols)
@@ -632,9 +617,5 @@ void java_bytecode_instrument(
   // instrument(...) can add symbols to the table, so it's
   // not safe to hold a reference to a symbol across a call.
   for(const auto &symbol : symbols_to_instrument)
-  {
-    exprt value=symbol_table.lookup(symbol).value;
-    instrument(value);
-    symbol_table.lookup(symbol).value=value;
-  }
+    instrument(symbol_table.lookup(symbol).value);
 }

src/java_bytecode/java_bytecode_instrument.h

@@ -11,19 +11,15 @@ Date:   June 2017
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H
 
-void java_bytecode_instrument(
+void java_bytecode_instrument_symbol(
   symbol_tablet &symbol_table,
   symbolt &symbol,
   const bool throw_runtime_exceptions,
-  message_handlert &_message_handler,
-  const size_t max_array_length,
-  const size_t max_depth);
+  message_handlert &_message_handler);
 
 void java_bytecode_instrument(
   symbol_tablet &symbol_table,
   const bool throw_runtime_exceptions,
-  message_handlert &_message_handler,
-  const size_t max_array_length,
-  const size_t max_depth);
+  message_handlert &_message_handler);
 
 #endif

src/java_bytecode/java_bytecode_language.cpp

@@ -459,9 +459,7 @@ bool java_bytecode_languaget::typecheck(
   java_bytecode_instrument(
     symbol_table,
     throw_runtime_exceptions,
-    get_message_handler(),
-    max_nondet_array_length,
-    max_nondet_tree_depth);
+    get_message_handler());
 
   // now typecheck all
   if(java_bytecode_typecheck(
@@ -748,13 +746,11 @@ void java_bytecode_languaget::replace_string_methods(
       symbol.value=generated_code;
       // Specifically instrument the new code, since this comes after the
       // blanket instrumentation pass called before typechecking.
-      java_bytecode_instrument(
+      java_bytecode_instrument_symbol(
         context,
         symbol,
         throw_runtime_exceptions,
-        get_message_handler(),
-        max_nondet_array_length,
-        max_nondet_tree_depth);
+        get_message_handler());
     }
   }
 }