Implement parsing of Unicode characters from JSON

Previously, if a JSON file contained a string in hexadecimal Unicode
representation, e.g. "\u0001", the JSON parser would discard the "\u"
part and store the string as "0001". This commit fixes this so the
resulting string is equal to "\u0001".

Author: antlechner

src/json/parser.y

@@ -46,8 +46,15 @@ static std::string convert_TOK_STRING()
       case 'r':  result+='\r'; break;
       case 't':  result+='\t'; break;
       case 'u':
+      {
+        // Character in hexadecimal Unicode representation, in the format
+        // \uABCD, i.e. the following four digits are part of this character.
+        assert(p + 4 < yyjsontext + len - 1);
+        std::string hex(++p, 4);
+        result += std::stoi(hex, nullptr, 16);
+        p += 3;
         break;
-        
+      }
       default:; /* an error */
       }
     }

unit/json/json_parser.cpp

@@ -84,4 +84,31 @@ SCENARIO("Loading JSON files")
       }
     }
   }
+  GIVEN("A JSON file containing a hexadecimal Unicode character")
+  {
+    temporary_filet unicode_json_file("cbmc_unit_json_parser_unicode", ".json");
+    const std::string unicode_json_path = unicode_json_file();
+    {
+      std::ofstream unicode_json_out(unicode_json_path);
+      unicode_json_out << "{\n"
+                       << "  \"special character\": \"\\u0001\"\n"
+                       << "}\n";
+    }
+    WHEN("Loading the JSON file with the special character")
+    {
+      jsont unicode_json;
+      const auto unicode_parse_error =
+        parse_json(unicode_json_path, null_message_handler, unicode_json);
+      THEN("The JSON file should be parsed correctly")
+      {
+        REQUIRE_FALSE(unicode_parse_error);
+        REQUIRE(unicode_json.is_object());
+
+        const json_objectt &json_object = to_json_object(unicode_json);
+        REQUIRE(json_object.find("special character") != json_object.end());
+        REQUIRE(json_object["special character"].value.size() == 1);
+        REQUIRE(json_object["special character"].value == "\u0001");
+      }
+    }
+  }
 }