SMACK'D JSON Input Format

Overview

SMACK'D parses command line output from SMACK and treats it as a JSON document that conforms to the schema below.

SMACK output must print (only) "smackd json\n" just before the json output, to indicate that the input is in json format (to facilitate compatibility until json output is implemented in SMACK).

SMACK'D does not currently validate input against this schema, and this schema may change slightly (particularly with regards to required elements).

Implementation Note

J2SE doesn't include JSON handling (it's only available in J2EE). I had to include an external JAR file. I grabbed javax.json-api-1.0.jar from https://jsonp.java.net/. I'm not sure if this is the best way, but I need to get moving. This should be addressed later.

A Sample SMACK'D Input

smackd json
{
  "verifier": "corral",
  "passed?": false,
  "failsAt": { "file": "simple.c", "line": 12, "column": 3, "description": "error PF5001: This assertion can fail" },
  "threadCount": 3,
  "traces": [
    { "threadid": 3, "file": "simple.c", "line": 11, "column": 5, "description": "" },
    { "threadid": 2, "file": "simple.c", "line": 11, "column": 5, "description": "" },
    { "threadid": 3, "file": "simple.c", "line": 12, "column": 3, "description": "error PF5001: This assertion can fail" }
  ]
}

The JSON Schema expected by SMACK'D

{
  "type":"object",
  "$schema": "http://json-schema.org/draft-03/schema",
  "required":false,
  "properties":{
    "verifier": {
      "type":"string",
      "required":false
    },
    "passed?": {
      "type":"boolean",
      "required":false
    },
    "threadCount": {
      "type":"number",
      "required":false
    },
    "failsAt": {
      "type":"object",
      "required":false,
      "properties":{
        "file": {
          "type":"string",
          "required":false
        },
        "line": {
          "type":"number",
          "required":false
        },
        "column": {
          "type":"number",
          "required":false
        },
        "description": {
          "type":"string",
          "required":false
        }
      }
    },
    "traces": {
      "type":"array",
      "required":false,
      "items": {
        "type":"object",
        "required":false,
        "properties":{
          "threadid": {
            "type":"number",
            "required":false
          },
          "file": {
            "type":"string",
            "required":false
          },
          "line": {
            "type":"number",
            "required":false
          },
          "column": {
            "type":"number",
            "required":false
          },
          "description": {
            "type":"string",
            "required":false
          }
        }
      }
    }
  }
}