blob: 1d20e48fb5e4680300d40212f46108880eb91fdd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.IO;
using System.Diagnostics;
namespace GPUVerify
{
class CommandLineOptions
{
public static List<string> inputFiles = new List<string>();
public static string outputFile = null;
public static string formulaSkeletonsFile = null;
public static string formulasFile = null;
public static bool NewRaceDetectionMethod = false;
public static bool OnlyDivergence = false;
public static bool FullAbstraction;
public static bool Inference;
public static string invariantsFile = null;
public static int Parse(string[] args)
{
for (int i = 0; i < args.Length; i++)
{
bool hasColonArgument = false;
string beforeColon;
string afterColon = null;
int colonIndex = args[i].IndexOf(':');
if (colonIndex >= 0 && (args[i].StartsWith("-") || args[i].StartsWith("/"))) {
hasColonArgument = true;
beforeColon = args[i].Substring(0, colonIndex);
afterColon = args[i].Substring(colonIndex + 1);
} else {
beforeColon = args[i];
}
switch (beforeColon)
{
case "-print":
case "/print":
if (!hasColonArgument)
{
Console.WriteLine("Error: filename expected after " + beforeColon + " argument");
Environment.Exit(1);
}
Debug.Assert(afterColon != null);
outputFile = afterColon;
break;
case "-generateFormulaSkeletons":
case "/generateFormulaSkeletons":
if (!hasColonArgument)
{
Console.WriteLine("Error: filename expected after " + beforeColon + " argument");
Environment.Exit(1);
}
Debug.Assert(afterColon != null);
formulaSkeletonsFile = afterColon;
break;
case "-formulas":
case "/formulas":
if (!hasColonArgument)
{
Console.WriteLine("Error: filename expected after " + beforeColon + " argument");
Environment.Exit(1);
}
Debug.Assert(afterColon != null);
formulasFile = afterColon;
break;
case "-newRaceDetectionMethod":
case "/newRaceDetectionMethod":
NewRaceDetectionMethod = true;
break;
case "-onlyDivergence":
case "/onlyDivergence":
OnlyDivergence = true;
break;
case "-fullAbstraction":
case "/fullAbstraction":
FullAbstraction = true;
break;
case "-inference":
case "/inference":
Inference = true;
if (hasColonArgument)
{
Debug.Assert(afterColon != null);
invariantsFile = afterColon;
}
break;
default:
inputFiles.Add(args[i]);
break;
}
}
return 0;
}
}
}
|
