Following coding guidelines in string preprocessing

I run the cpplint script on the string solver file, and improved the
coding style according to its suggestions. I also added more
explenations in string_constraint_generator.
ALl the errors signaled by cpplint have been dealt with except a few
that conserns indentation in the comments and one concerning an array
of non-constant size.

Author: romainbrenguier

src/goto-programs/string_refine_preprocess.cpp

@@ -9,8 +9,8 @@ Date:   September 2016
 
 \*******************************************************************/
 
-#ifndef CPROVER_STRING_REFINE_PREPROCESS_H
-#define CPROVER_STRING_REFINE_PREPROCESS_H
+#ifndef CPROVER_GOTO_PROGRAMS_STRING_REFINE_PREPROCESS_H
+#define CPROVER_GOTO_PROGRAMS_STRING_REFINE_PREPROCESS_H
 
 #include <goto-programs/goto_model.h>
 #include <util/ui_message.h>
@@ -31,16 +31,16 @@ class string_refine_preprocesst:public messaget
   std::map<irep_idt, irep_idt> side_effect_char_array_functions;
 
  public:
-  string_refine_preprocesst(symbol_tablet &, goto_functionst &, message_handlert &);
+  string_refine_preprocesst
+    (symbol_tablet &, goto_functionst &, message_handlert &);
 
  private:
-
   // add a temporary symbol to the symbol table
   symbol_exprt new_tmp_symbol(const std::string &name, const typet &type);
 
   void declare_function(irep_idt function_name, const typet &type);
 
-  exprt replace_string_literals(const exprt & );
+  exprt replace_string_literals(const exprt &);
 
   // replace "lhs=s.some_function(x,...)" by "lhs=function_name(s,x,...)"
   void make_string_function
@@ -74,15 +74,15 @@ class string_refine_preprocesst:public messaget
   void make_char_array_function_call
     (goto_programt::instructionst::iterator & i_it, irep_idt function_name);
 
-  // replace "r = s.some_function(i,arr,...)" by "s=function_name(s,i,arr.length,arr.data)"
+  // replace `r = s.some_function(i,arr,...)` by
+  // `s=function_name(s,i,arr.length,arr.data)`
   // and add a correspondance from r to s in the string_builders map
   void make_char_array_side_effect
     (goto_programt::instructionst::iterator & i_it, irep_idt function_name);
 
   bool has_java_string_type(const exprt &expr);
 
   void replace_string_calls(goto_functionst::function_mapt::iterator f_it);
-
 };
 
-#endif 
+#endif

src/goto-programs/string_refine_preprocess.h

@@ -10,72 +10,83 @@ Author: Romain Brenguier, [email protected]
 #include <solvers/refinement/refined_string_type.h>
 #include <ansi-c/string_constant.h>
 
-refined_string_typet::refined_string_typet(unsignedbv_typet char_type) : struct_typet() {
+refined_string_typet::refined_string_typet(unsignedbv_typet char_type)
+  :struct_typet()
+{
   components().resize(2);
   components()[0].set_name("length");
   components()[0].set_pretty_name("length");
   components()[0].type()=refined_string_typet::index_type();
 
-  array_typet char_array(char_type,infinity_exprt(refined_string_typet::index_type()));
+  infinity_exprt infinite_index(refined_string_typet::index_type());
+  array_typet char_array(char_type, infinite_index);
   components()[1].set_name("content");
   components()[1].set_pretty_name("content");
   components()[1].type()=char_array;
 }
 
 bool refined_string_typet::is_c_string_type(const typet &type)
 {
-  if (type.id() == ID_struct) {
-    irep_idt tag = to_struct_type(type).get_tag();
-    return (tag == irep_idt("__CPROVER_string"));
-  } else return false;
+  if(type.id()==ID_struct)
+  {
+    irep_idt tag=to_struct_type(type).get_tag();
+    return (tag==irep_idt("__CPROVER_string"));
+  }
+  return false;
 }
 
 bool refined_string_typet::is_java_string_type(const typet &type)
 {
-  if(type.id() == ID_pointer) {
-    pointer_typet pt = to_pointer_type(type);
-    typet subtype = pt.subtype();
+  if(type.id()==ID_pointer)
+  {
+    pointer_typet pt=to_pointer_type(type);
+    typet subtype=pt.subtype();
     return is_java_deref_string_type(subtype);
-  } else return false;
+  }
+  return false;
 }
 
 bool refined_string_typet::is_java_deref_string_type(const typet &type)
 {
-  if(type.id() == ID_symbol)
+  if(type.id()==ID_symbol)
   {
-    irep_idt tag = to_symbol_type(type).get_identifier();
-    return (tag == irep_idt("java::java.lang.String"));
+    irep_idt tag=to_symbol_type(type).get_identifier();
+    return (tag==irep_idt("java::java.lang.String"));
   }
-  else if(type.id() == ID_struct)
+  else if(type.id()==ID_struct)
   {
-    irep_idt tag = to_struct_type(type).get_tag();
-    return (tag == irep_idt("java.lang.String"));
+    irep_idt tag=to_struct_type(type).get_tag();
+    return (tag==irep_idt("java.lang.String"));
   }
-  else return false;
+  return false;
 }
 
 bool refined_string_typet::is_java_string_builder_type(const typet &type)
 {
-  if(type.id() == ID_pointer) {
-    pointer_typet pt = to_pointer_type(type);
-    typet subtype = pt.subtype();
-    if(subtype.id() == ID_struct) {
-      irep_idt tag = to_struct_type(subtype).get_tag();
-      return (tag == irep_idt("java.lang.StringBuilder"));
+  if(type.id()==ID_pointer)
+  {
+    pointer_typet pt=to_pointer_type(type);
+    typet subtype=pt.subtype();
+    if(subtype.id()==ID_struct)
+    {
+      irep_idt tag=to_struct_type(subtype).get_tag();
+      return (tag==irep_idt("java.lang.StringBuilder"));
     }
-    else return false;
-  } else return false;
+  }
+  return false;
 }
 
 bool refined_string_typet::is_java_char_sequence_type(const typet &type)
 {
-  if(type.id() == ID_pointer) {
-    pointer_typet pt = to_pointer_type(type);
-    typet subtype = pt.subtype();
-    if(subtype.id() == ID_struct) {
-      irep_idt tag = to_struct_type(subtype).get_tag();
-      return (tag == irep_idt("java.lang.CharSequence"));
+  if(type.id()==ID_pointer)
+  {
+    pointer_typet pt=to_pointer_type(type);
+    typet subtype=pt.subtype();
+    if(subtype.id()==ID_struct)
+    {
+      irep_idt tag=to_struct_type(subtype).get_tag();
+      return (tag==irep_idt("java.lang.CharSequence"));
     }
-    else return false;
-  } else return false;
+  }
+  return false;
 }

src/solvers/refinement/refined_string_type.cpp

@@ -7,8 +7,8 @@ Author: Romain Brenguier, [email protected]
 
 \*******************************************************************/
 
-#ifndef CPROVER_SOLVER_REFINED_STRING_TYPE_H
-#define CPROVER_SOLVER_REFINED_STRING_TYPE_H
+#ifndef CPROVER_SOLVERS_REFINEMENT_REFINED_STRING_TYPE_H
+#define CPROVER_SOLVERS_REFINEMENT_REFINED_STRING_TYPE_H
 
 #include <util/std_types.h>
 #include <util/std_expr.h>
@@ -19,22 +19,30 @@ Author: Romain Brenguier, [email protected]
 #define STRING_SOLVER_JAVA_CHAR_WIDTH 16
 
 // Internal type used for string refinement
-class refined_string_typet : public struct_typet {
+class refined_string_typet: public struct_typet
+{
 public:
-  refined_string_typet(unsignedbv_typet char_type);
+  explicit refined_string_typet(unsignedbv_typet char_type);
 
   // Type for the content (list of characters) of a string
   inline array_typet get_content_type()
   { return to_array_type((to_struct_type(*this)).components()[1].type());}
 
   // Types used in this refinement
-  static inline unsignedbv_typet char_type() { return unsignedbv_typet(STRING_SOLVER_C_CHAR_WIDTH);}
+  static inline unsignedbv_typet char_type()
+  { return unsignedbv_typet(STRING_SOLVER_C_CHAR_WIDTH); }
 
-  static inline unsignedbv_typet java_char_type() { return unsignedbv_typet(STRING_SOLVER_JAVA_CHAR_WIDTH);}
+  static inline unsignedbv_typet java_char_type()
+  { return unsignedbv_typet(STRING_SOLVER_JAVA_CHAR_WIDTH);}
 
-  static inline signedbv_typet index_type() { return signedbv_typet(STRING_SOLVER_INDEX_WIDTH);}
+  static inline signedbv_typet index_type()
+  { return signedbv_typet(STRING_SOLVER_INDEX_WIDTH);}
 
-  static inline exprt index_zero() { return constant_exprt(integer2binary(0, STRING_SOLVER_INDEX_WIDTH), index_type());}
+  static inline exprt index_zero()
+  {
+    return constant_exprt(integer2binary(0, STRING_SOLVER_INDEX_WIDTH),
+                          index_type());
+  }
 
   // For C the unrefined string type is __CPROVER_string, for java it is a
   // pointer to a strict with tag java.lang.String
@@ -49,24 +57,27 @@ class refined_string_typet : public struct_typet {
 
   static bool is_java_char_sequence_type(const typet & type);
 
-  static inline unsignedbv_typet get_char_type(const exprt & expr) {
-    if(is_c_string_type(expr.type())) return char_type();
-    else return java_char_type();
+  static inline unsignedbv_typet get_char_type(const exprt & expr)
+  {
+    if(is_c_string_type(expr.type()))
+      return char_type();
+    else
+      return java_char_type();
   }
 
   static inline bool is_unrefined_string_type(const typet & type)
-  {  return (is_c_string_type(type)
-          || is_java_string_type(type)
-          || is_java_string_builder_type(type)
-          || is_java_char_sequence_type(type)
-	     ); }
+  {
+    return (is_c_string_type(type)
+            || is_java_string_type(type)
+            || is_java_string_builder_type(type)
+            || is_java_char_sequence_type(type));
+  }
 
   static inline bool is_unrefined_string(const exprt & expr)
-  {  return (is_unrefined_string_type(expr.type())); }
+  { return (is_unrefined_string_type(expr.type())); }
 
   static inline constant_exprt index_of_int(int i)
-  { return from_integer(i,index_type()); }
-
+  { return from_integer(i, index_type()); }
 };