diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-11-09 10:32:04 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-11-09 10:32:04 -0800 |
| commit | 69d88c8fc5be24a41a1fb57af945251c3701d1a2 (patch) | |
| tree | 6bccf5aa680a8c57aaa87349b066f8ca02283177 /Source/GPUVerify/CommandLineOptions.cs | |
| parent | c38ad7de79e9a3b351ba9f1a8648f43893ec7ca7 (diff) | |
| parent | 9865334085ec74d1fe931490f72e6970cc88de64 (diff) | |
Merge
Diffstat (limited to 'Source/GPUVerify/CommandLineOptions.cs')
| -rw-r--r-- | Source/GPUVerify/CommandLineOptions.cs | 67 |
1 files changed, 36 insertions, 31 deletions
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index 9e7ba32c..2f08477b 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -14,10 +14,7 @@ namespace GPUVerify 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;
@@ -49,6 +46,12 @@ namespace GPUVerify switch (beforeColon)
{
+ case "-help":
+ case "/help":
+ case "-?":
+ case "/?":
+ return -1;
+
case "-print":
case "/print":
if (!hasColonArgument)
@@ -60,34 +63,6 @@ namespace GPUVerify 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;
@@ -163,5 +138,35 @@ namespace GPUVerify return 0;
}
+ private static bool printedHelp = false;
+
+ public static void Usage()
+ {
+ // Ensure that we only print the help message once
+ if (printedHelp)
+ {
+ return;
+ }
+ printedHelp = true;
+
+ Console.WriteLine(@"GPUVerify: usage: GPUVerify [ option ... ] [ filename ... ]
+ where <option> is one of
+
+ /help : this message
+ /fullAbstraction : apply full state abstraction
+ /onlyDivergence : only check for divergence-freedom, not race-freedom
+ /symmetry : apply symmetry breaking
+ /eager : check races eagerly, rather than waiting for barrier
+ /inference:file : use automatic invariant inference. Optional file can include manually supplied candidates
+ /raceCheckingContract : try to infer race-freedom contracts for procedures
+ /setEncoding : check races using set encoding
+ /divided : check individual pairs of possibly racing statements separately
+ /dividedArray : check races on arrays one at a time
+ /dividedElement : ???
+
+");
+ }
+
+
}
}
|