Peter's comments

Author: mgudemann

src/java_bytecode/expr2java.cpp

@@ -50,7 +50,7 @@ std::string expr2javat::convert_code_function_call(
     unsigned p;
     std::string lhs_str=convert(src.lhs(), p);
 
-    // TODO: ggf. Klammern je nach p
+    // TODO: if necessery add parentheses, dependent on p
     dest+=lhs_str;
     dest+='=';
   }

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -425,14 +425,14 @@ codet java_bytecode_convert_methodt::get_array_bounds_check(
   bounds_checks.operands().back().add_source_location()
     .set_comment("Array index < 0");
   bounds_checks.operands().back().add_source_location()
-    .set_property_class("array-index-oob-low");
+    .set_property_class("array-index-out-of-bounds-low");
   bounds_checks.add(code_assertt(ltlength));
 
   bounds_checks.operands().back().add_source_location()=original_sloc;
   bounds_checks.operands().back().add_source_location()
     .set_comment("Array index >= length");
   bounds_checks.operands().back().add_source_location()
-    .set_property_class("array-index-oob-high");
+    .set_property_class("array-index-out-of-bounds-high");
 
   // TODO make this throw ArrayIndexOutOfBoundsException instead of asserting.
   return bounds_checks;
@@ -795,9 +795,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
       if(i_it->statement=="jsr" ||
          i_it->statement=="jsr_w")
       {
-        instructionst::const_iterator next=i_it;
+        instructionst::const_iterator next=i_it+1;
         assert(
-          ++next!=instructions.end() &&
+          next!=instructions.end() &&
           "jsr without valid return address?");
         targets.insert(next->address);
         jsr_ret_targets.push_back(next->address);
@@ -1750,7 +1750,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       if(!disable_runtime_checks)
       {
         // TODO make this throw NegativeArrayIndexException instead.
-        constant_exprt intzero=as_number(0, java_int_type());
+        constant_exprt intzero=from_integer(0, java_int_type());
         binary_relation_exprt gezero(op[0], ID_ge, intzero);
         code_assertt check(gezero);
         check.add_source_location().set_comment("Array size < 0");
@@ -1761,7 +1761,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
         if(max_array_length!=0)
         {
           constant_exprt size_limit=
-            as_number(max_array_length, java_int_type());
+            from_integer(max_array_length, java_int_type());
           binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
           code_assumet assume_le_max_size(le_max_size);
           checkandcreate.move_to_operands(assume_le_max_size);

src/java_bytecode/java_bytecode_convert_method_class.h

@@ -51,7 +51,7 @@ class java_bytecode_convert_methodt:public messaget
 protected:
   symbol_tablet &symbol_table;
   const bool disable_runtime_checks;
-  size_t max_array_length;
+  const size_t max_array_length;
 
   irep_idt method_id;
   irep_idt current_method;

src/java_bytecode/java_bytecode_parser.cpp

@@ -1455,11 +1455,11 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
       sourcefile_name=pool_entry(sourcefile_index).s;
     else
     {
-      std::string packageName=fqn.substr(0, last_index+1);
-      std::replace(packageName.begin(), packageName.end(), '.', '/');
-      const std::string
-        &fullFileName=(packageName+id2string(pool_entry(sourcefile_index).s));
-      sourcefile_name=fullFileName;
+      std::string package_name=fqn.substr(0, last_index+1);
+      std::replace(package_name.begin(), package_name.end(), '.', '/');
+      const std::string &full_file_name=
+        package_name+id2string(pool_entry(sourcefile_index).s);
+      sourcefile_name=full_file_name;
     }
 
     for(methodst::iterator m_it=parsed_class.methods.begin();

src/java_bytecode/java_entry_point.cpp

@@ -105,12 +105,12 @@ bool java_static_lifetime_init(
   symbolt &initialize_symbol=symbol_table.lookup(INITIALIZE);
   code_blockt &code_block=to_code_block(to_code(initialize_symbol.value));
 
-  // W need to zero out all static variables, or nondet-initialize if they're
+  // We need to zero out all static variables, or nondet-initialize if they're
   // external. Iterate over a copy of the symtab, as its iterators are
   // invalidated by object_factory:
 
   std::list<irep_idt> symnames;
-  for(const auto& entry : symbol_table.symbols)
+  for(const auto &entry : symbol_table.symbols)
     symnames.push_back(entry.first);
 
   for(const auto& symname : symnames)

src/java_bytecode/java_object_factory.cpp

@@ -81,17 +81,30 @@ class java_object_factoryt:public messaget
     const typet &override_type=empty_typet());
 };
 
-// Returns false if we can't figure out the size of allocate_type.
-// allocate_type may differ from target_expr, e.g. for target_expr having
-// type int* and allocate_type being an int[10].
+
+/*******************************************************************\
+
+Function: gen_nondet_array_init
+
+  Inputs: the target expression, desired object type, source location
+          and Boolean whether to create a dynamic object
+
+ Outputs: the allocated object
+
+ Purpose: Returns false if we can't figure out the size of allocate_type.
+          allocate_type may differ from target_expr, e.g. for target_expr
+          having type int* and allocate_type being an int[10].
+
+\*******************************************************************/
+
 exprt java_object_factoryt::allocate_object(
-  const exprt& target_expr,
-  const typet& allocate_type,
+  const exprt &target_expr,
+  const typet &allocate_type,
   const source_locationt &loc,
   bool create_dynamic_objects)
 {
-  const typet& allocate_type_resolved=ns.follow(allocate_type);
-  const typet& target_type=ns.follow(target_expr.type().subtype());
+  const typet &allocate_type_resolved=ns.follow(allocate_type);
+  const typet &target_type=ns.follow(target_expr.type().subtype());
   bool cast_needed=allocate_type_resolved!=target_type;
   if(!create_dynamic_objects)
   {
@@ -197,7 +210,7 @@ void java_object_factoryt::gen_nondet_init(
     if(!assume_non_null)
     {
       auto returns_null_sym=
-          new_tmp_symbol(symbol_table, "opaque_returns_null");
+        new_tmp_symbol(symbol_table, "opaque_returns_null");
       returns_null_sym.type=c_bool_typet(1);
       auto returns_null=returns_null_sym.symbol_expr();
       auto assign_returns_null=
@@ -449,7 +462,6 @@ void java_object_factoryt::gen_nondet_array_init(
   init_code.move_to_operands(init_done_label);
 }
 
-
 /*******************************************************************\
 
 Function: gen_nondet_init
@@ -502,7 +514,7 @@ Function: new_tmp_symbol
 
 symbolt &new_tmp_symbol(symbol_tablet &symbol_table, const std::string& prefix)
 {
-  static size_t temporary_counter=0;
+  static size_t temporary_counter=0; // TODO change this
 
   auxiliary_symbolt new_symbol;
   symbolt *symbol_ptr;

src/java_bytecode/java_pointer_casts.cpp

@@ -44,7 +44,6 @@ Function: find_superclass_with_type
 
 \*******************************************************************/
 
-
 bool find_superclass_with_type(
   exprt &ptr,
   const typet &target_type,

src/util/json_expr.cpp

@@ -265,7 +265,7 @@ json_objectt json(
       if(expr.get(ID_value)==ID_NULL)
         result["data"]=json_stringt("NULL");
     }
-    else if(type.id()==ID_bool || type.id()==ID_c_bool)
+    else if(type.id()==ID_bool)
     {
       result["name"]=json_stringt("boolean");
       result["binary"]=json_stringt(expr.is_true()?"1":"0");