Skip to main content

Symflower run

This feature sends a main function to Symflower for symbolic execution and returns coverage as a result:

symflower run $filepath

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

Use this feature to symbolically execute programs to collect coverage data for analysis.

Tutorial: symflower run

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);
}
}

Run the symflower run command:

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

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
}
]