From cd54ad72925bfa79a4137e6bbfd5351f3b0270f9 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Wed, 16 May 2018 15:14:29 +0100
Subject: [PATCH] Corrected state persistence in the json parser

The parser needs a call to restart before it can be used again as
otherwise it reports the last calls failure.
Added a simple unit test that exhibits the problem
---
 src/json/json_parser.h    |  2 ++
 unit/json/invalid.json    |  1 +
 unit/json/json_parser.cpp | 69 +++++++++++++++++++++++++++++++++++++++
 unit/json/valid.json      |  3 ++
 4 files changed, 75 insertions(+)
 create mode 100644 unit/json/invalid.json
 create mode 100644 unit/json/json_parser.cpp
 create mode 100644 unit/json/valid.json

diff --git a/src/json/json_parser.h b/src/json/json_parser.h
index d3d28aa6fa2..d3155f9e337 100644
--- a/src/json/json_parser.h
+++ b/src/json/json_parser.h
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/json.h>
 
 int yyjsonparse();
+void yyjsonrestart(FILE *input_file);
 
 class json_parsert:public parsert
 {
@@ -46,6 +47,7 @@ class json_parsert:public parsert
   virtual void clear() override
   {
     stack=stackt();
+    yyjsonrestart(nullptr);
   }
 };
 
diff --git a/unit/json/invalid.json b/unit/json/invalid.json
new file mode 100644
index 00000000000..257cc5642cb
--- /dev/null
+++ b/unit/json/invalid.json
@@ -0,0 +1 @@
+foo
diff --git a/unit/json/json_parser.cpp b/unit/json/json_parser.cpp
new file mode 100644
index 00000000000..0ab1d73bfc4
--- /dev/null
+++ b/unit/json/json_parser.cpp
@@ -0,0 +1,69 @@
+/*******************************************************************\
+
+ Module: Example Catch Tests
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <json/json_parser.h>
+#include <testing-utils/catch.hpp>
+
+SCENARIO("Loading JSON files")
+{
+  null_message_handlert message_handler;
+  GIVEN("A invalid JSON file and a valid JSON file")
+  {
+    const std::string valid_json_path = "./json/valid.json";
+    const std::string invalid_json_path = "./json/invalid.json";
+
+    WHEN("Loading the invalid JSON file")
+    {
+      jsont invalid_json;
+      const auto invalid_parse_error =
+        parse_json(invalid_json_path, message_handler, invalid_json);
+      THEN("An error state should be returned")
+      {
+        REQUIRE(invalid_parse_error);
+        REQUIRE(invalid_json.is_null());
+        AND_WHEN("Loading the valid JSON file")
+        {
+          jsont valid_json;
+          const auto valid_parse_error =
+            parse_json(valid_json_path, message_handler, valid_json);
+          THEN("The JSON file should be parsed correctly")
+          {
+            REQUIRE_FALSE(valid_parse_error);
+            REQUIRE(valid_json.is_object());
+            REQUIRE(valid_json.object.find("hello") != valid_json.object.end());
+            REQUIRE(valid_json.object["hello"].value == "world");
+          }
+        }
+      }
+    }
+    WHEN("Loading the valid JSON file")
+    {
+      jsont valid_json;
+      const auto valid_parse_error =
+        parse_json(valid_json_path, message_handler, valid_json);
+      THEN("The JSON file should be parsed correctly")
+      {
+        REQUIRE_FALSE(valid_parse_error);
+        REQUIRE(valid_json.is_object());
+        REQUIRE(valid_json.object.find("hello") != valid_json.object.end());
+        REQUIRE(valid_json.object["hello"].value == "world");
+        AND_WHEN("Loading the invalid JSON file")
+        {
+          jsont invalid_json;
+          const auto invalid_parse_error =
+            parse_json(invalid_json_path, message_handler, invalid_json);
+          THEN("An error state should be returned")
+          {
+            REQUIRE(invalid_parse_error);
+            REQUIRE(invalid_json.is_null());
+          }
+        }
+      }
+    }
+  }
+}
diff --git a/unit/json/valid.json b/unit/json/valid.json
new file mode 100644
index 00000000000..f2a886f39de
--- /dev/null
+++ b/unit/json/valid.json
@@ -0,0 +1,3 @@
+{
+  "hello": "world"
+}