Unit test improve convert exprt to string exprt

Structure using GIVEN WHEN THEN

Author: romainbrenguier

unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp

@@ -17,7 +17,7 @@
 #include <util/namespace.h>
 #include <langapi/mode.h>
 
-exprt convert_exprt_to_string_exprt_unit_test(
+refined_string_exprt convert_exprt_to_string_exprt_unit_test(
   java_string_library_preprocesst &preprocess,
   const exprt &deref,
   const source_locationt &loc,
@@ -30,30 +30,57 @@ exprt convert_exprt_to_string_exprt_unit_test(
 
 TEST_CASE("Convert exprt to string exprt")
 {
-  source_locationt loc;
-  symbol_tablet symbol_table;
-  namespacet ns(symbol_table);
-  code_blockt code;
-  java_string_library_preprocesst preprocess;
-  preprocess.add_string_type("java.lang.String", symbol_table);
-  symbol_typet java_string_type("java::java.lang.String");
-  symbol_exprt expr("a", pointer_type(java_string_type));
-  convert_exprt_to_string_exprt_unit_test(
-    preprocess, expr, loc, symbol_table, code);
-  register_language(new_java_bytecode_language);
-
-  std::vector<std::string> code_string;
-  for(auto op : code.operands())
-    code_string.push_back(from_expr(ns, "", op));
-
-  REQUIRE(code_string.size()==7);
-  REQUIRE(code_string[0]=="int cprover_string_length$1;");
-  REQUIRE(code_string[1]=="char cprover_string_array$2[INFINITY()];");
-  REQUIRE(code_string[2]=="cprover_string_length$1 = a->length;");
-  REQUIRE(code_string[3]=="__CPROVER_assume(!(a->data == null));");
-  REQUIRE(code_string[4]=="cprover_string_array$2 = *a->data;");
-  REQUIRE(code_string[5]=="struct __CPROVER_refined_string_type { int length; "
-    "char content[INFINITY()]; } cprover_string$3;");
-  REQUIRE(code_string[6]=="cprover_string$3 = { .=cprover_string_length$1, "
-    ".=cprover_string_array$2 };");
+  GIVEN("A location, a string expression, and a symbol table")
+  {
+    source_locationt loc;
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+    code_blockt code;
+    java_string_library_preprocesst preprocess;
+    preprocess.add_string_type("java.lang.String", symbol_table);
+    symbol_typet java_string_type("java::java.lang.String");
+    symbol_exprt expr("a", pointer_type(java_string_type));
+
+    WHEN("String expression is converted to refined string expression")
+    {
+      refined_string_exprt string_expr =
+        convert_exprt_to_string_exprt_unit_test(
+          preprocess, expr, loc, symbol_table, code);
+
+      THEN("The type of the returd expression is that of refined strings")
+      {
+        REQUIRE(string_expr.id() == ID_struct);
+        REQUIRE(is_refined_string_type(string_expr.type()));
+      }
+
+      THEN("Code is produced")
+      {
+        register_language(new_java_bytecode_language);
+
+        std::vector<std::string> code_string;
+        const std::regex spaces("\\s+");
+        const std::regex numbers("\\$[0-9]*");
+        for(auto op : code.operands())
+        {
+          const std::string line = from_expr(ns, "", op);
+          code_string.push_back(
+            std::regex_replace(
+              std::regex_replace(line, spaces, " "), numbers, ""));
+        }
+
+        const std::vector<std::string> reference_code = {
+          "char *cprover_string_content;",
+          "int cprover_string_length;",
+          "cprover_string_length = a->length;",
+          "cprover_string_content = a->data;"};
+
+        for(std::size_t i = 0;
+            i < code_string.size() && i < reference_code.size();
+            ++i)
+          REQUIRE(code_string[i] == reference_code[i]);
+
+        REQUIRE(code_string.size() == reference_code.size());
+      }
+    }
+  }
 }