Merge pull request #6225 from thomasspriggs/tas/unit_test_smt_identifier_conversion

Add unit test of `smt2_convt::convert_identifier`

Author: martin-cs

src/solvers/smt2/smt2_conv.h

@@ -82,6 +82,8 @@ class smt2_convt : public stack_decision_proceduret
 
   std::size_t get_number_of_solver_calls() const override;
 
+  static std::string convert_identifier(const irep_idt &identifier);
+
 protected:
   const namespacet &ns;
   std::ostream &out;
@@ -136,8 +138,6 @@ class smt2_convt : public stack_decision_proceduret
   void convert_with(const with_exprt &expr);
   void convert_update(const exprt &expr);
 
-  std::string convert_identifier(const irep_idt &identifier);
-
   void convert_expr(const exprt &);
   void convert_type(const typet &);
   void convert_literal(const literalt);

unit/Makefile

@@ -84,6 +84,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/sat/external_sat.cpp \
        solvers/sat/satcheck_cadical.cpp \
        solvers/sat/satcheck_minisat2.cpp \
+       solvers/smt2/smt2_conv.cpp \
        solvers/strings/array_pool/array_pool.cpp \
        solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \
        solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \

unit/solvers/smt2/module_dependencies.txt

@@ -0,0 +1,2 @@
+solvers/smt2
+testing-utils

unit/solvers/smt2/smt2_conv.cpp

@@ -0,0 +1,18 @@
+// Author: Diffblue Ltd.
+
+#include <testing-utils/use_catch.h>
+
+#include <solvers/smt2/smt2_conv.h>
+
+TEST_CASE(
+  "smt2_convt::convert_identifier character escaping.",
+  "[core][solvers][smt2]")
+{
+  const auto no_escaping_characters = "abcdefghijklmnopqrstuvwxyz0123456789$";
+  CHECK(
+    smt2_convt::convert_identifier(no_escaping_characters) ==
+    no_escaping_characters);
+  CHECK(smt2_convt::convert_identifier("\\") == "&92;");
+  CHECK(smt2_convt::convert_identifier("|") == "&124;");
+  CHECK(smt2_convt::convert_identifier("&") == "&38;");
+}