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