take tautschnig's comments into account

Author: mgudemann

src/java_bytecode/expr2java.cpp

@@ -95,7 +95,7 @@ std::string expr2javat::convert_code_function_call(
         first=false;
       else
         dest+=", ";
-      // TODO: ggf. Klammern je nach p
+      // TODO: if necessery add parentheses, dependent on p
       dest+=arg_str;
     }
   }

src/java_bytecode/java_bytecode_language.cpp

@@ -239,15 +239,13 @@ bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
 
   symbolt entry=res.main_function;
 
-  if(java_entry_point(
-       symbol_table,
-       main_class,
-       get_message_handler(),
-       assume_inputs_non_null,
-       max_nondet_array_length))
-    return true;
-
-  return false;
+  return(
+    java_entry_point(
+      symbol_table,
+      main_class,
+      get_message_handler(),
+      assume_inputs_non_null,
+      max_nondet_array_length));
 }
 
 /*******************************************************************\

src/java_bytecode/java_bytecode_typecheck_expr.cpp

@@ -94,8 +94,8 @@ void java_bytecode_typecheckt::typecheck_expr_java_new_array(
 static void escape_non_alnum(std::string& toescape)
 {
   for(auto &ch : toescape)
-  if(!isalnum(ch))
-    ch='_';
+    if(!isalnum(ch))
+      ch='_';
 }
 
 /*******************************************************************\

src/java_bytecode/java_entry_point.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #include <set>
 #include <iostream>
 
+#include <util/arith_tools.h>
 #include <util/prefix.h>
 #include <util/std_types.h>
 #include <util/std_code.h>
@@ -71,18 +72,6 @@ static void create_initialize(symbol_tablet &symbol_table)
 }
 
 
-/*******************************************************************\
-
-Function: java_static_lifetime_init
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
 static bool should_init_symbol(const symbolt& sym)
 {
   if(sym.type.id()!=ID_code &&
@@ -95,6 +84,18 @@ static bool should_init_symbol(const symbolt& sym)
   return has_prefix(id2string(sym.name), "java::java.lang.String.Literal");
 }
 
+/*******************************************************************\
+
+Function: java_static_lifetime_init
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
 bool java_static_lifetime_init(
   symbol_tablet &symbol_table,
   const source_locationt &source_location,
@@ -126,12 +127,11 @@ bool java_static_lifetime_init(
           std::string namestr=id2string(sym.symbol_expr().get_identifier());
           const std::string suffix="@class_model";
           // Static '.class' fields are always non-null.
-          if(namestr.size()>=suffix.size() &&
-             namestr.substr(namestr.size()-suffix.size())==suffix)
+          if(has_suffix(namestr, suffix))
             allow_null=false;
           if(allow_null && has_prefix(
-                             namestr,
-                             "java::java.lang.String.Literal"))
+               namestr,
+               "java::java.lang.String.Literal"))
             allow_null=false;
         }
         auto newsym=object_factory(
@@ -208,7 +208,7 @@ exprt::operandst java_build_arguments(
   {
     bool is_this=(param_number==0) &&
                  parameters[param_number].get_this();
-    bool is_default_entry_point(config.main=="");
+    bool is_default_entry_point(config.main.empty());
     bool is_main=is_default_entry_point;
     if(!is_main)
     {
@@ -244,7 +244,7 @@ exprt::operandst java_build_arguments(
     input.op0()=address_of_exprt(
       index_exprt(
         string_constantt(p_symbol.base_name),
-        gen_zero(index_type())));
+        from_integer(0, index_type())));
     input.op1()=main_arguments[param_number];
     input.add_source_location()=function.location;
 
@@ -293,7 +293,7 @@ void java_record_outputs(
       address_of_exprt(
         index_exprt(
           string_constantt(return_symbol.base_name),
-          gen_zero(index_type())));
+          from_integer(0, index_type())));
     output.op1()=return_symbol.symbol_expr();
     output.add_source_location()=function.location;
 
@@ -316,7 +316,7 @@ void java_record_outputs(
         address_of_exprt(
           index_exprt(
             string_constantt(p_symbol.base_name),
-            gen_zero(index_type())));
+            from_integer(0, index_type())));
       output.op1()=main_arguments[param_number];
       output.add_source_location()=function.location;
 

src/java_bytecode/java_object_factory.cpp

@@ -514,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; // TODO change this
+  static size_t temporary_counter=0; // TODO encapsulate as class variable
 
   auxiliary_symbolt new_symbol;
   symbolt *symbol_ptr;

src/util/json_expr.cpp

@@ -16,6 +16,7 @@ Author: Peter Schrammel
 #include "config.h"
 
 #include "json_expr.h"
+
 /*******************************************************************\
 
 Function: json