Commit 7180a4d1 authored by Etienne Renault's avatar Etienne Renault

go2pins: options can now be combined

* main.go: Here.
parent bc162002
......@@ -492,92 +492,94 @@ func main() {
if *astprint {
tools.PrintAst(flag.Args()[0])
} else if *callgraph {
}
if *callgraph {
tools.PrintCG(tools.CallGraph(flag.Args()[0]))
} else {
relPackagePath := flag.Args()[0]
basePackagePath := path.Base(relPackagePath)
// Check whether the output/ directory already exists.
if _, err := os.Stat(*output); err == nil {
if !*forceOverwrite {
fmt.Fprintln(os.Stderr, *output+" already exists")
os.Exit(1)
}
err = os.RemoveAll(*output)
if err != nil {
fmt.Fprintln(os.Stderr, "couldn't delete "+*output)
os.Exit(1)
}
}
}
// Create the output directory.
if err := os.MkdirAll(*output, 0777); err != nil {
fmt.Fprintln(os.Stderr, err.Error())
relPackagePath := flag.Args()[0]
basePackagePath := path.Base(relPackagePath)
// Check whether the output/ directory already exists.
if _, err := os.Stat(*output); err == nil {
if !*forceOverwrite {
fmt.Fprintln(os.Stderr, *output+" already exists")
os.Exit(1)
}
// Create a file in output/ with the same name as the input package.
f, err := os.Create(path.Join(*output, basePackagePath))
err = os.RemoveAll(*output)
if err != nil {
fmt.Fprintln(os.Stderr, err.Error())
fmt.Fprintln(os.Stderr, "couldn't delete "+*output)
os.Exit(1)
}
defer f.Close()
}
if *ignorefunc != "" {
var unspacify = regexp.MustCompile(` *`)
s := unspacify.ReplaceAllString(*ignorefunc, "")
toIgnore = strings.Split(s, ";")
}
// Create the output directory.
if err := os.MkdirAll(*output, 0777); err != nil {
fmt.Fprintln(os.Stderr, err.Error())
os.Exit(1)
}
tmpFilePath, goroutines := duplicateGoroutines(relPackagePath)
// FIXME: do we want this ?
// defer os.Remove(tmpFilePath)
flag.Args()[0] = tmpFilePath
// Create a file in output/ with the same name as the input package.
f, err := os.Create(path.Join(*output, basePackagePath))
if err != nil {
fmt.Fprintln(os.Stderr, err.Error())
os.Exit(1)
}
defer f.Close()
src, err := ioutil.ReadFile(tmpFilePath)
if err != nil {
fmt.Println(err)
os.Exit(1)
}
if *ignorefunc != "" {
var unspacify = regexp.MustCompile(` *`)
s := unspacify.ReplaceAllString(*ignorefunc, "")
toIgnore = strings.Split(s, ";")
}
// Compile and write the package to the output file.
packageName, err := compileTo(basePackagePath, src, f, goroutines, rers)
if err != nil {
fmt.Fprintln(os.Stderr, err.Error())
os.Exit(1)
}
tmpFilePath, goroutines := duplicateGoroutines(relPackagePath)
// FIXME: do we want this ?
// defer os.Remove(tmpFilePath)
flag.Args()[0] = tmpFilePath
tools.FormatArray(*output+"/"+basePackagePath, "var G2PVariableNames =")
src, err := ioutil.ReadFile(tmpFilePath)
if err != nil {
fmt.Println(err)
os.Exit(1)
}
// Get project root directory to locate boilerplate/ dir
_, currentPath, _, ok := runtime.Caller(0)
if !ok {
fmt.Fprintln(os.Stderr, "can't get path of current file")
os.Exit(1)
}
go2pinsDir := path.Dir(currentPath)
// Compile and write the package to the output file.
packageName, err := compileTo(basePackagePath, src, f, goroutines, rers)
if err != nil {
fmt.Fprintln(os.Stderr, err.Error())
os.Exit(1)
}
boilerplateFiles := []string{
"Makefile",
"go2pins.c",
"go2pins.h",
"main.go",
}
data := packageTemplate{basePackagePath, packageName}
for _, filename := range boilerplateFiles {
from := path.Join(go2pinsDir, "boilerplate/"+filename)
to := path.Join(*output, filename)
copyFile(from, to, data)
}
tools.FormatArray(*output+"/"+basePackagePath, "var G2PVariableNames =")
fmt.Println("Preprocessing done.\n\nTo display the state space of you program, follows the instructions below")
fmt.Println(" cd", *output)
fmt.Println(" make")
fmt.Println(" ./go2pins-mc -display")
fmt.Println("\nDisplay all available options (including LTL verification) with the following instruction:")
fmt.Println(" ./go2pins-mc -help")
// Get project root directory to locate boilerplate/ dir
_, currentPath, _, ok := runtime.Caller(0)
if !ok {
fmt.Fprintln(os.Stderr, "can't get path of current file")
os.Exit(1)
}
go2pinsDir := path.Dir(currentPath)
boilerplateFiles := []string{
"Makefile",
"go2pins.c",
"go2pins.h",
"main.go",
}
data := packageTemplate{basePackagePath, packageName}
for _, filename := range boilerplateFiles {
from := path.Join(go2pinsDir, "boilerplate/"+filename)
to := path.Join(*output, filename)
copyFile(from, to, data)
}
fmt.Println("Preprocessing done.\n\nTo display the state space of you program, follows the instructions below")
fmt.Println(" cd", *output)
fmt.Println(" make")
fmt.Println(" ./go2pins-mc -display")
fmt.Println("\nDisplay all available options (including LTL verification) with the following instruction:")
fmt.Println(" ./go2pins-mc -help")
}
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment