Skip to main content

Symflower run

This page provides an overview of symflower run, a Symflower feature that sends a main function to Symflower for symbolic execution and returns coverage as a result.

Usage​

symflower [OPTIONS] run [run-OPTIONS] [filters...]

The command takes the following arguments:

  • coverage options
    • --coverage-file: The file path where the coverage should be written to.
  • workspace options
    • --language: Analyze with this language. By default all languages are used.
    • --workspace: The root directory of the project to analyze. (default: .)

Example output:

> cat main.go
package main

func main() {
x := int32(2147483647)
x++
}
> symflower run main.go
main.go:5:2: critical: main.main: overflow of addition

Details​

Use this feature to symbolically execute programs to collect coverage data for analysis. The command lets you specify the file path to write the coverage data to.

Tutorial​

Example​

This example stores the sign of the variable x in the variable y and prints it to the console.

public class Main {
    public static void main(String[] args) {
        int x = 5;
        int y;

        if (x > 0) {
            y = 1;
        } else if (x == 0) {
            y = 0;
        } else {
            y = -1;
        }

        System.out.println(y);
    }
}

Execute symflower run​

Run the symflower run command:

symflower run --coverage-file=coverage.json src/main/java/com/symflower/Main.java

View the coverage​

The output is a coverage.json file with coverage data per file range:

[
 {
   "FileRange": "src/java/io/PrintStream.java:52:32-src/java/io/PrintStream.java:54:5",
   "CoverageType": "NodeCoverageTrue",
   "Count": 1
 },
 {
   "FileRange": "src/main/java/com/symflower/Main.java:16:28-src/main/java/com/symflower/Main.java:16:28",
   "CoverageType": "NodeCoverageTrue",
   "Count": 1
 },
 {
   "FileRange": "src/main/java/com/symflower/Main.java:16:9-src/main/java/com/symflower/Main.java:16:18",
   "CoverageType": "NodeCoverageTrue",
   "Count": 1
 },
 {
   "FileRange": "src/main/java/com/symflower/Main.java:16:9-src/main/java/com/symflower/Main.java:16:29",
   "CoverageType": "NodeCoverageTrue",
   "Count": 1
 },
 {
   "FileRange": "src/main/java/com/symflower/Main.java:4:44-src/main/java/com/symflower/Main.java:17:5",
   "CoverageType": "NodeCoverageTrue",
   "Count": 1
 },
 {
   "FileRange": "src/main/java/com/symflower/Main.java:5:17-src/main/java/com/symflower/Main.java:5:17",
   "CoverageType": "NodeCoverageTrue",
   "Count": 1
 },
 {
   "FileRange": "src/main/java/com/symflower/Main.java:5:9-src/main/java/com/symflower/Main.java:5:17",
   "CoverageType": "NodeCoverageTrue",
   "Count": 1
 },
 {
   "FileRange": "src/main/java/com/symflower/Main.java:6:9-src/main/java/com/symflower/Main.java:6:13",
   "CoverageType": "NodeCoverageTrue",
   "Count": 1
 },
 {
   "FileRange": "src/main/java/com/symflower/Main.java:8:13-src/main/java/com/symflower/Main.java:8:13",
   "CoverageType": "NodeCoverageTrue",
   "Count": 1
 },
 {
   "FileRange": "src/main/java/com/symflower/Main.java:8:13-src/main/java/com/symflower/Main.java:8:17",
   "CoverageType": "NodeCoverageTrue",
   "Count": 1
 },
 {
   "FileRange": "src/main/java/com/symflower/Main.java:8:17-src/main/java/com/symflower/Main.java:8:17",
   "CoverageType": "NodeCoverageTrue",
   "Count": 1
 },
 {
   "FileRange": "src/main/java/com/symflower/Main.java:8:20-src/main/java/com/symflower/Main.java:10:9",
   "CoverageType": "NodeCoverageTrue",
   "Count": 1
 },
 {
   "FileRange": "src/main/java/com/symflower/Main.java:8:9-src/main/java/com/symflower/Main.java:14:9",
   "CoverageType": "NodeCoverageTrue",
   "Count": 1
 },
 {
   "FileRange": "src/main/java/com/symflower/Main.java:9:13-src/main/java/com/symflower/Main.java:9:13",
   "CoverageType": "NodeCoverageTrue",
   "Count": 1
 },
 {
   "FileRange": "src/main/java/com/symflower/Main.java:9:13-src/main/java/com/symflower/Main.java:9:17",
   "CoverageType": "NodeCoverageTrue",
   "Count": 1
 },
 {
   "FileRange": "src/main/java/com/symflower/Main.java:9:17-src/main/java/com/symflower/Main.java:9:17",
   "CoverageType": "NodeCoverageTrue",
   "Count": 1
 }
]