Documentation for java_bytecode_convert_methodt::variable

Author: cesaro

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -186,6 +186,21 @@ symbol_exprt java_bytecode_convert_methodt::tmp_variable(
   return result;
 }
 
+/// Returns a symbol_exprt indicating a local variable suitable to load/store
+/// from a bytecode at address `address` a value of type `type_char` stored in
+/// the JVM's slot `arg`.
+///
+/// \param arg
+///   The local variable slot
+/// \param type_char
+///   The type of the value stored in the slot pointed by `arg`.
+/// \param address
+///   Bytecode address used to find a variable that the LVT declares to be live
+///   and living in the slot pointed by `arg` for this bytecode.
+/// \param do_cast
+///   Indicates whether we should return the original symbol_exprt or a
+///   typecast_exprt if the type of the symbol_exprt does not equal that
+///   represented by `type_char`.
 const exprt java_bytecode_convert_methodt::variable(
   const exprt &arg,
   char type_char,

src/java_bytecode/java_local_variable_table.cpp

@@ -543,7 +543,7 @@ static void merge_variable_table_entries(
 /// Given a sequence of users of the same local variable slot, this figures out
 /// which ones are related by control flow, and combines them into a single
 /// entry with holes, such that after combination we can create a single
-/// declaration per variable table entry, placed at the live range's start
+/// GOTO variable per variable table entry, placed at the live range's start
 /// address, which may be moved back so that the declaration dominates all uses.
 /// \par parameters: `firstvar`-`varlimit`: sequence of variable table entries,
 ///   all of which should concern the same slot index.