Emit YAML violation witnesses (format 2.3)

README.md

@@ -1,7 +1,33 @@
 # WitnessCreator
 
-WitnessCreator creates SV-COMP GraphML violation witnesses from SWAT witness
-markers.
+WitnessCreator creates SV-COMP violation witnesses from SWAT witness markers:
+
+- `witness.yml` in the [YAML witness format 2.3](https://gitlab.com/sosy-lab/benchmarking/sv-witnesses)
+  for Java (one `violation_sequence` with a `function_return` waypoint per
+  `Verifier.nondet*()` value and a final `target` waypoint at the violating statement),
+- `witness.graphml` in the legacy GraphML format, for validators that still consume it.
+
+## Usage
+
+```sh
+java -jar build/libs/WitnessCreator.jar <markers> [<dir>] \
+    [--input <path>]... [--property <file.prp>] [--out <dir>] [--producer-version <version>]
+```
+
+- `<markers>`: base64 of the SWAT output lines carrying `[WITNESS]` (one per nondet value:
+  `value@@@line@@@class@@@method@@@callIndex@@@typeDesc@@@sourceFile`) and `[WITNESS_TARGET]`
+  (the uncaught throwable with its stack trace) markers. An empty string yields the default
+  violation witness without waypoints.
+- `--input`: the task's input files or directories exactly as given to the verifier. They are
+  searched for the sources (`.java`) and listed, with their SHA-256 hashes, in the witness.
+- `--property`: the property file, its content becomes the witness' `specification`.
+- `--out`: the output directory (default: `<dir>`, the legacy positional source directory).
+- `--producer-version`: written to `metadata.producer.version`.
+
+Columns are derived from the sources: a `function_return` waypoint points to the closing
+parenthesis of the `callIndex`-th nondet call on its line, the `target` waypoint to the start of
+the violating statement (`assert`, `throw`, or the first token of the innermost statement in the
+task sources that appears in the stack trace).
 
 ## Build
 

build.gradle

@@ -14,6 +14,8 @@ repositories {
 
 dependencies {
     implementation 'org.antlr:ST4:4.3.4'
+    testImplementation 'org.junit.jupiter:junit-jupiter:5.10.2'
+    testRuntimeOnly 'org.junit.platform:junit-platform-launcher'
 }
 
 java {
@@ -22,6 +24,10 @@ java {
     }
 }
 
+tasks.named('test') {
+    useJUnitPlatform()
+}
+
 application {
     mainClass = 'App'
 }