", AnnotateNullable.class);
String[] inv_files = options.parse(true, args);
- assert inv_files.length == 1;
+ if (help) {
+ options.printUsage();
+ System.exit(0);
+ }
+ if (inv_files.length != 1) {
+ System.err.println("must specify exactly one invariant file");
+ options.printUsage(System.err);
+ System.exit(1);
+ }
// Read the serialized invariant file
File inv_file = new File(inv_files[0]);
diff --git a/java/daikon/Chicory.java b/java/daikon/Chicory.java
index c77e6426b5..eafad6653c 100644
--- a/java/daikon/Chicory.java
+++ b/java/daikon/Chicory.java
@@ -240,7 +240,7 @@ public static void main(String[] args) {
public static void check_args(Options options, String[] target_args) {
if (help) {
options.printUsage();
- System.exit(1);
+ System.exit(0);
}
if (nesting_depth < 0) {
System.out.printf("nesting depth (%d) must not be negative%n", nesting_depth);
diff --git a/java/daikon/Daikon.java b/java/daikon/Daikon.java
index 1e7c1e1b73..aaa2b3f3d6 100644
--- a/java/daikon/Daikon.java
+++ b/java/daikon/Daikon.java
@@ -1022,7 +1022,6 @@ static FileOptions read_options(String[] args, String usage) {
LongOpt[] longopts =
new LongOpt[] {
// Control output
- new LongOpt(help_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
new LongOpt(no_text_output_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
new LongOpt(format_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
new LongOpt(show_progress_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
@@ -1055,7 +1054,7 @@ static FileOptions read_options(String[] args, String usage) {
new LongOpt(disc_reason_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
new LongOpt(mem_stat_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
};
- Getopt g = new Getopt("daikon.Daikon", args, "ho:", longopts);
+ DaikonGetopt g = new DaikonGetopt(args, "o:", longopts, usage);
int c;
while ((c = g.getopt()) != -1) {
@@ -1065,10 +1064,7 @@ static FileOptions read_options(String[] args, String usage) {
String option_name = longopts[g.getLongind()].getName();
// Control output
- if (help_SWITCH.equals(option_name)) {
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- } else if (no_text_output_SWITCH.equals(option_name)) {
+ if (no_text_output_SWITCH.equals(option_name)) {
no_text_output = true;
} else if (format_SWITCH.equals(option_name)) {
String format_name = getOptarg(g);
@@ -1367,12 +1363,9 @@ else if (ppt_regexp_SWITCH.equals(option_name)) {
} else if (mem_stat_SWITCH.equals(option_name)) {
use_mem_monitor = true;
} else {
- throw new Daikon.UserError("Unknown option " + option_name + " on command line");
+ throw new Daikon.BugInDaikon("Unhandled long option " + option_name);
}
break;
- case 'h':
- System.out.println(usage);
- throw new Daikon.NormalTermination();
case 'o':
String inv_filename = getOptarg(g);
@@ -1391,11 +1384,6 @@ else if (ppt_regexp_SWITCH.equals(option_name)) {
}
break;
//
- case '?':
- // break; // getopt() already printed an error
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- //
default:
throw new Daikon.BugInDaikon("getopt() returned " + c);
}
diff --git a/java/daikon/DaikonGetopt.java b/java/daikon/DaikonGetopt.java
new file mode 100644
index 0000000000..0f71e31406
--- /dev/null
+++ b/java/daikon/DaikonGetopt.java
@@ -0,0 +1,279 @@
+package daikon;
+
+import gnu.getopt.Getopt;
+import gnu.getopt.LongOpt;
+import java.util.Arrays;
+import java.util.function.Supplier;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.plumelib.util.ArraysPlume;
+
+/**
+ * A command-line option processor that throws a {@link Daikon.UserError} that describes a bad
+ * command-line option, instead of printing a message and returning {@code '?'} or {@code ':'}.
+ *
+ * If constructed with a usage message, it also handles {@code -h} and {@code --help}: it prints
+ * the usage message and throws {@link Daikon.NormalTermination}.
+ */
+public class DaikonGetopt extends Getopt {
+
+ /**
+ * The name passed to {@link Getopt}, which uses it only in messages that DaikonGetopt suppresses.
+ */
+ private static final String PROGNAME = "DaikonGetopt";
+
+ /**
+ * Computes the usage message printed for {@code -h} and {@code --help}, or null if the caller
+ * handles them.
+ */
+ private final @Nullable Supplier usage;
+
+ /** Text appended to the description of a bad command-line option, or null to append nothing. */
+ private @Nullable String usageHint = "run with -h for usage";
+
+ /**
+ * Creates a command-line option processor that recognizes short and long options.
+ *
+ * @param argv the command-line arguments
+ * @param optstring the short options, in the format of {@link Getopt}
+ * @param longopts the long options
+ */
+ public DaikonGetopt(String[] argv, String optstring, LongOpt[] longopts) {
+ super(PROGNAME, argv, optstring, longopts);
+ this.usage = null;
+ opterr = false;
+ }
+
+ /**
+ * Creates a command-line option processor that recognizes short and long options, plus {@code -h}
+ * and {@code --help}, which print the usage message and throw {@link Daikon.NormalTermination}.
+ *
+ * @param argv the command-line arguments
+ * @param optstring the short options, in the format of {@link Getopt}; must not contain {@code h}
+ * @param longopts the long options; must not contain {@code help}
+ * @param usage the usage message to print for {@code -h} and {@code --help}
+ */
+ public DaikonGetopt(String[] argv, String optstring, LongOpt[] longopts, String usage) {
+ this(argv, optstring, longopts, () -> usage);
+ }
+
+ /**
+ * Creates a command-line option processor that recognizes short and long options, plus {@code -h}
+ * and {@code --help}, which print the usage message and throw {@link Daikon.NormalTermination}.
+ * The usage message is computed only if it is needed.
+ *
+ * @param argv the command-line arguments
+ * @param optstring the short options, in the format of {@link Getopt}; must not contain {@code h}
+ * @param longopts the long options; must not contain {@code help}
+ * @param usage computes the usage message to print for {@code -h} and {@code --help}
+ */
+ public DaikonGetopt(String[] argv, String optstring, LongOpt[] longopts, Supplier usage) {
+ super(PROGNAME, argv, withH(optstring), withHelp(longopts));
+ this.usage = usage;
+ opterr = false;
+ }
+
+ /**
+ * Returns the given short options plus {@code -h}.
+ *
+ * @param optstring short options, in the format of {@link Getopt}; must not contain {@code h}
+ * @return {@code optstring} plus {@code -h}
+ */
+ private static String withH(String optstring) {
+ if (optstring.indexOf('h') != -1) {
+ throw new IllegalArgumentException("optstring already contains h: " + optstring);
+ }
+ return optstring + "h";
+ }
+
+ /**
+ * Returns the given long options plus {@code --help}.
+ *
+ * @param longopts long options; must not contain {@code help}
+ * @return {@code longopts} plus {@code --help}
+ */
+ private static LongOpt[] withHelp(LongOpt[] longopts) {
+ for (LongOpt longopt : longopts) {
+ if (longopt.getName().equals(Daikon.help_SWITCH)) {
+ throw new IllegalArgumentException("longopts already contains " + Daikon.help_SWITCH);
+ }
+ }
+ return ArraysPlume.append(
+ longopts, new LongOpt(Daikon.help_SWITCH, LongOpt.NO_ARGUMENT, null, 'h'));
+ }
+
+ /**
+ * Processes the command-line arguments of a program that takes no options other than {@code -h}
+ * and {@code --help}.
+ *
+ * @param argv the command-line arguments
+ * @param usage the usage message to print for {@code -h} and {@code --help}
+ * @return the arguments that are not options
+ * @throws Daikon.NormalTermination after printing the usage message, if an argument requests it
+ * @throws Daikon.UserError if an argument is any other option
+ */
+ public static String[] nonOptionArgs(String[] argv, String usage) {
+ return argsAfterOptions(argv, "", () -> usage);
+ }
+
+ /**
+ * Processes the leading command-line arguments of a program that takes no options other than
+ * {@code -h} and {@code --help}. Processing stops at the first argument that is not an option, so
+ * later arguments may be options for some other program.
+ *
+ * @param argv the command-line arguments
+ * @param usage the usage message to print for {@code -h} and {@code --help}
+ * @return the arguments from the first one that is not an option onward
+ * @throws Daikon.NormalTermination after printing the usage message, if a leading argument
+ * requests it
+ * @throws Daikon.UserError if a leading argument is any other option
+ */
+ public static String[] argsAfterLeadingOptions(String[] argv, String usage) {
+ return argsAfterLeadingOptions(argv, () -> usage);
+ }
+
+ /**
+ * Like {@link #argsAfterLeadingOptions(String[], String)}, but computes the usage message only if
+ * it is needed.
+ *
+ * @param argv the command-line arguments
+ * @param usage computes the usage message to print for {@code -h} and {@code --help}
+ * @return the arguments from the first one that is not an option onward
+ * @throws Daikon.NormalTermination after printing the usage message, if a leading argument
+ * requests it
+ * @throws Daikon.UserError if a leading argument is any other option
+ */
+ public static String[] argsAfterLeadingOptions(String[] argv, Supplier usage) {
+ // A leading "+" tells Getopt to stop at the first argument that is not an option.
+ return argsAfterOptions(argv, "+", usage);
+ }
+
+ /**
+ * Processes command-line arguments, permitting no options other than {@code -h} and {@code
+ * --help}.
+ *
+ * @param argv the command-line arguments
+ * @param optstring "" to process all the arguments, or "+" to stop at the first non-option
+ * @param usage computes the usage message to print for {@code -h} and {@code --help}
+ * @return the arguments that Getopt did not process as options
+ * @throws Daikon.NormalTermination after printing the usage message, if an argument requests it
+ * @throws Daikon.UserError if an argument is any other option
+ */
+ private static String[] argsAfterOptions(
+ String[] argv, String optstring, Supplier usage) {
+ // Getopt permutes its argument array, so give it a copy to avoid modifying the caller's array.
+ String[] argvCopy = argv.clone();
+ DaikonGetopt g = new DaikonGetopt(argvCopy, optstring, new LongOpt[0], usage);
+ // Every option other than -h and --help is bad, so getopt() returns only -1 or throws.
+ int c = g.getopt();
+ if (c != -1) {
+ throw new Daikon.BugInDaikon("getopt() returned " + c);
+ }
+ return Arrays.copyOfRange(argvCopy, g.getOptind(), argvCopy.length);
+ }
+
+ /**
+ * Sets the text that is appended to the description of a bad command-line option. The default
+ * tells the user to run the program with -h.
+ *
+ * @param usageHint text appended to the description of a bad command-line option, or null to
+ * append nothing
+ */
+ public void setUsageHint(@Nullable String usageHint) {
+ this.usageHint = usageHint;
+ }
+
+ /**
+ * Like {@link Getopt#getopt()}, but never returns {@code '?'} or {@code ':'}. Getopt returns
+ * {@code ':'} for a missing argument if the optstring starts with {@code ':'}. If this was
+ * constructed with a usage message, also never returns {@code 'h'}.
+ *
+ * @return the next option, as described in {@link Getopt#getopt()}
+ * @throws Daikon.UserError if the next option is unrecognized, ambiguous, or malformed
+ * @throws Daikon.NormalTermination after printing the usage message, if the next option is {@code
+ * -h} or {@code --help} and this was constructed with a usage message
+ */
+ @Override
+ public int getopt() {
+ int c = super.getopt();
+ if (c == '?' || c == ':') {
+ throw badOptionError();
+ }
+ if (c == 'h' && usage != null) {
+ System.out.println(usage.get());
+ throw new Daikon.NormalTermination();
+ }
+ return c;
+ }
+
+ /**
+ * Returns an exception that describes the bad command-line option that {@link Getopt#getopt()}
+ * just rejected.
+ *
+ * @return an exception that describes the bad command-line option
+ */
+ private Daikon.UserError badOptionError() {
+ String message = badOptionMessage();
+ if (usageHint != null) {
+ message += "; " + usageHint;
+ }
+ return new Daikon.UserError(message);
+ }
+
+ /**
+ * Returns a description of the bad command-line option that {@link Getopt#getopt()} just
+ * rejected.
+ *
+ * @return a description of the bad command-line option
+ */
+ private String badOptionMessage() {
+ // For every bad long option, Getopt clears nextchar and advances optind past the option. A
+ // bad short option has no such guarantee, because it may be followed by other short options in
+ // the same argument, as in "-xh".
+ if ("".equals(nextchar) && argv[optind - 1].startsWith("--")) {
+ return longOptionMessage(argv[optind - 1]);
+ }
+ char c = (char) optopt;
+ if (c == ':' || optstring.indexOf(c) == -1) {
+ return "Unrecognized command-line option -" + c;
+ } else {
+ return "Command-line option -" + c + " requires an argument";
+ }
+ }
+
+ /**
+ * Returns a description of a bad long command-line option. Uses {@code longind}, which Getopt
+ * sets to the index of the long option that matched the argument, or to -1 if none matched.
+ *
+ * @param arg the bad command-line argument, which starts with "--"
+ * @return a description of the bad command-line option
+ */
+ private String longOptionMessage(String arg) {
+ int equalsPos = arg.indexOf('=');
+ String name = (equalsPos == -1) ? arg.substring(2) : arg.substring(2, equalsPos);
+ LongOpt[] longopts = long_options;
+ // Getopt treats an empty name, as in "--=foo", as a prefix of every long option.
+ if (name.isEmpty()) {
+ return "Unrecognized command-line option " + arg;
+ }
+ if (longopts == null || longind == -1) {
+ return "Unrecognized command-line option --" + name;
+ }
+ LongOpt match = longopts[longind];
+ // For an inexact match, Getopt sets longind to the first long option that has the given
+ // prefix. The match is ambiguous if a later long option also has the prefix.
+ if (!match.getName().equals(name)) {
+ for (int i = longind + 1; i < longopts.length; i++) {
+ if (longopts[i].getName().startsWith(name)) {
+ return "Ambiguous command-line option --" + name;
+ }
+ }
+ }
+ if (equalsPos != -1 && match.getHasArg() == LongOpt.NO_ARGUMENT) {
+ return "Command-line option --" + match.getName() + " does not take an argument";
+ } else if (equalsPos == -1 && match.getHasArg() == LongOpt.REQUIRED_ARGUMENT) {
+ return "Command-line option --" + match.getName() + " requires an argument";
+ } else {
+ return "Bad command-line option " + arg;
+ }
+ }
+}
diff --git a/java/daikon/DynComp.java b/java/daikon/DynComp.java
index d7a4118c0a..3c03de694f 100644
--- a/java/daikon/DynComp.java
+++ b/java/daikon/DynComp.java
@@ -179,7 +179,7 @@ public static void main(String[] args) {
public static void check_args(Options options, String[] targetArgs) {
if (help) {
options.printUsage();
- System.exit(1);
+ System.exit(0);
}
if (nesting_depth < 0) {
System.out.printf("nesting depth (%d) must not be negative%n", nesting_depth);
diff --git a/java/daikon/MergeInvariants.java b/java/daikon/MergeInvariants.java
index bc2009da5d..8a814a80fb 100644
--- a/java/daikon/MergeInvariants.java
+++ b/java/daikon/MergeInvariants.java
@@ -5,7 +5,6 @@
import daikon.split.PptSplitter;
import daikon.suppress.NIS;
-import gnu.getopt.Getopt;
import gnu.getopt.LongOpt;
import java.io.File;
import java.io.FileNotFoundException;
@@ -97,14 +96,13 @@ public static void mainHelper(String[] args)
LongOpt[] longopts =
new LongOpt[] {
- new LongOpt(Daikon.help_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
new LongOpt(Daikon.config_option_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
new LongOpt(Daikon.debugAll_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
new LongOpt(Daikon.debug_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
new LongOpt(Daikon.track_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
};
- Getopt g = new Getopt("daikon.MergeInvariants", args, "ho:", longopts);
+ DaikonGetopt g = new DaikonGetopt(args, "o:", longopts, usage);
int c;
while ((c = g.getopt()) != -1) {
switch (c) {
@@ -112,10 +110,7 @@ public static void mainHelper(String[] args)
// long option
case 0:
String option_name = longopts[g.getLongind()].getName();
- if (Daikon.help_SWITCH.equals(option_name)) {
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- } else if (Daikon.config_option_SWITCH.equals(option_name)) {
+ if (Daikon.config_option_SWITCH.equals(option_name)) {
String item = Daikon.getOptarg(g);
daikon.config.Configuration.getInstance().apply(item);
break;
@@ -133,14 +128,10 @@ public static void mainHelper(String[] args)
"Error parsing track argument '" + Daikon.getOptarg(g) + "' - " + error);
}
} else {
- throw new Daikon.UserError("Unknown long option received: " + option_name);
+ throw new Daikon.BugInDaikon("Unhandled long option " + option_name);
}
break;
- case 'h':
- System.out.println(usage);
- throw new Daikon.NormalTermination();
-
case 'o':
String output_inv_filename = Daikon.getOptarg(g);
@@ -160,12 +151,8 @@ public static void mainHelper(String[] args)
}
break;
- case '?':
- break; // getopt() already printed an error
-
default:
- System.out.println("getopt() returned " + c);
- break;
+ throw new Daikon.BugInDaikon("getopt() returned " + c);
}
}
diff --git a/java/daikon/PrintInvariants.java b/java/daikon/PrintInvariants.java
index f7bc9121c3..57f483661d 100644
--- a/java/daikon/PrintInvariants.java
+++ b/java/daikon/PrintInvariants.java
@@ -24,7 +24,6 @@
import daikon.split.PptSplitter;
import daikon.suppress.NIS;
import daikon.suppress.NISuppressionSet;
-import gnu.getopt.Getopt;
import gnu.getopt.LongOpt;
import java.io.BufferedWriter;
import java.io.File;
@@ -329,7 +328,6 @@ public static void mainHelper(String[] args)
LongOpt[] longopts =
new LongOpt[] {
- new LongOpt(Daikon.help_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
new LongOpt(Daikon.format_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
new LongOpt(Daikon.suppress_redundant_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
new LongOpt(Daikon.output_num_samples_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
@@ -344,17 +342,14 @@ public static void mainHelper(String[] args)
new LongOpt(
PrintInvariants.print_csharp_metadata_SWITCH, LongOpt.OPTIONAL_ARGUMENT, null, 0),
};
- Getopt g = new Getopt("daikon.PrintInvariants", args, "h", longopts);
+ DaikonGetopt g = new DaikonGetopt(args, "", longopts, usage);
int c;
while ((c = g.getopt()) != -1) {
switch (c) {
case 0:
// got a long option
String option_name = longopts[g.getLongind()].getName();
- if (Daikon.help_SWITCH.equals(option_name)) {
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- } else if (Daikon.ppt_regexp_SWITCH.equals(option_name)) {
+ if (Daikon.ppt_regexp_SWITCH.equals(option_name)) {
if (ppt_regexp != null) {
throw new Error(
"multiple --"
@@ -430,17 +425,11 @@ public static void mainHelper(String[] args)
} else if (Daikon.wrap_xml_SWITCH.equals(option_name)) {
wrap_xml = true;
} else {
- throw new RuntimeException("Unknown long option received: " + option_name);
+ throw new Daikon.BugInDaikon("Unhandled long option " + option_name);
}
break;
- case 'h':
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- case '?':
- break; // getopt() already printed an error
default:
- System.out.println("getopt() returned " + c);
- break;
+ throw new Daikon.BugInDaikon("getopt() returned " + c);
}
}
diff --git a/java/daikon/SplitDtrace.java b/java/daikon/SplitDtrace.java
index d13b4b81cb..aff7705ba9 100644
--- a/java/daikon/SplitDtrace.java
+++ b/java/daikon/SplitDtrace.java
@@ -29,6 +29,9 @@
*/
public final class SplitDtrace {
+ /** The usage message for this program. */
+ private static final String usage = "Usage: java daikon.SplitDtrace file.dtrace[.gz]";
+
/** Do not instantiate. */
private SplitDtrace() {
throw new UnsupportedOperationException("Do not instantiate");
@@ -40,14 +43,29 @@ private SplitDtrace() {
* @param args one argument, the name of the .dtrace or .dtrace.gz file
*/
public static void main(String[] args) throws IOException {
- if (args.length != 1) {
- throw new RuntimeException(
- "You must supply one argument which is the filename of the dtrace file");
+ try {
+ mainHelper(args);
+ } catch (Daikon.DaikonTerminationException e) {
+ Daikon.handleDaikonTerminationException(e);
+ }
+ }
+
+ /**
+ * This does the work of {@link #main(String[])}, but it never calls System.exit, so it is
+ * appropriate to be called programmatically.
+ *
+ * @param args command-line arguments, like those of {@link #main}
+ * @throws IOException if there is a problem reading or writing a file
+ */
+ public static void mainHelper(String[] args) throws IOException {
+ String[] files = DaikonGetopt.nonOptionArgs(args, usage);
+ if (files.length != 1) {
+ throw new Daikon.UserError(usage);
}
- String filename = args[0].trim();
+ String filename = files[0].trim();
boolean isGz = filename.endsWith(".dtrace.gz");
if (!filename.endsWith(".dtrace") && !isGz) {
- throw new RuntimeException(
+ throw new Daikon.UserError(
"Filename must end with .dtrace or .dtrace.gz: filename=" + filename);
}
int declNum = 1;
diff --git a/java/daikon/UnionInvariants.java b/java/daikon/UnionInvariants.java
index ea34b0f075..c07e19d7ce 100644
--- a/java/daikon/UnionInvariants.java
+++ b/java/daikon/UnionInvariants.java
@@ -1,6 +1,5 @@
package daikon;
-import gnu.getopt.Getopt;
import gnu.getopt.LongOpt;
import java.io.File;
import org.plumelib.util.FilesPlume;
@@ -52,25 +51,19 @@ public static void mainHelper(String[] args) throws Exception {
new LongOpt[] {
new LongOpt(Daikon.suppress_redundant_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
};
- Getopt g = new Getopt("daikon.UnionInvariants", args, "ho:", longopts);
+ DaikonGetopt g = new DaikonGetopt(args, "o:", longopts, usage);
int c;
while ((c = g.getopt()) != -1) {
switch (c) {
case 0:
// got a long option
String option_name = longopts[g.getLongind()].getName();
- if (Daikon.help_SWITCH.equals(option_name)) {
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- } else if (Daikon.suppress_redundant_SWITCH.equals(option_name)) {
+ if (Daikon.suppress_redundant_SWITCH.equals(option_name)) {
Daikon.suppress_redundant_invariants_with_simplify = true;
} else {
- throw new Daikon.UserError("Unknown option received: " + option_name);
+ throw new Daikon.BugInDaikon("Unhandled long option " + option_name);
}
break;
- case 'h':
- System.out.println(usage);
- throw new Daikon.NormalTermination();
case 'o':
String inv_filename = Daikon.getOptarg(g);
@@ -90,11 +83,8 @@ public static void mainHelper(String[] args) throws Exception {
}
break;
//
- case '?':
- break; // getopt() already printed an error
default:
- System.out.println("getopt() returned " + c);
- break;
+ throw new Daikon.BugInDaikon("getopt() returned " + c);
}
}
diff --git a/java/daikon/dcomp/BuildJDK.java b/java/daikon/dcomp/BuildJDK.java
index 7f1cae05f3..35cf4b0583 100644
--- a/java/daikon/dcomp/BuildJDK.java
+++ b/java/daikon/dcomp/BuildJDK.java
@@ -122,6 +122,10 @@ public static void main(String[] args) throws IOException {
DynComp.class,
DCInstrument.class);
String[] cl_args = options.parse(true, args);
+ if (DynComp.help) {
+ options.printUsage();
+ System.exit(0);
+ }
if (cl_args.length < 1) {
System.err.println("must specify destination dir");
options.printUsage();
diff --git a/java/daikon/dcomp/BuildJDK24.java b/java/daikon/dcomp/BuildJDK24.java
index 74c83abacf..13fb445108 100644
--- a/java/daikon/dcomp/BuildJDK24.java
+++ b/java/daikon/dcomp/BuildJDK24.java
@@ -132,6 +132,10 @@ public static void main(String[] args) throws IOException {
DynComp.class,
DCInstrument24.class);
String[] cl_args = options.parse(true, args);
+ if (DynComp.help) {
+ options.printUsage();
+ System.exit(0);
+ }
if (cl_args.length < 1) {
System.err.println("must specify destination dir");
options.printUsage();
diff --git a/java/daikon/diff/Diff.java b/java/daikon/diff/Diff.java
index 0019d1e935..6355ef0892 100644
--- a/java/daikon/diff/Diff.java
+++ b/java/daikon/diff/Diff.java
@@ -4,13 +4,13 @@
import static java.util.logging.Level.INFO;
import daikon.Daikon;
+import daikon.DaikonGetopt;
import daikon.FileIO;
import daikon.Ppt;
import daikon.PptConditional;
import daikon.PptMap;
import daikon.PptTopLevel;
import daikon.inv.Invariant;
-import gnu.getopt.Getopt;
import gnu.getopt.LongOpt;
import java.io.File;
import java.io.FileNotFoundException;
@@ -68,13 +68,19 @@ public final class Diff {
" For a list of flags, see the Daikon manual, which appears in the ",
" Daikon distribution and also at http://plse.cs.washington.edu/daikon/.");
- /** The long command line options. */
- private static final String HELP_SWITCH = "help";
-
+ /** The long command-line option that specifies the comparator to sort the first set of invs. */
private static final String INV_SORT_COMPARATOR1_SWITCH = "invSortComparator1";
+
+ /** The long command-line option that specifies the comparator to sort the second set of invs. */
private static final String INV_SORT_COMPARATOR2_SWITCH = "invSortComparator2";
+
+ /** The long command-line option that specifies the comparator to pair up invs. */
private static final String INV_PAIR_COMPARATOR_SWITCH = "invPairComparator";
+
+ /** The long command-line option that is a synonym for -y. */
private static final String IGNORE_UNJUSTIFIED_SWITCH = "ignore_unjustified";
+
+ /** The long command-line option that ignores numbered exit points. */
private static final String IGNORE_NUMBERED_EXITS_SWITCH = "ignore_exitNN";
/** Determine which ppts should be paired together in the tree. */
@@ -193,7 +199,6 @@ public static void mainHelper(final String[] args)
LongOpt[] longOpts =
new LongOpt[] {
- new LongOpt(HELP_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
new LongOpt(INV_SORT_COMPARATOR1_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
new LongOpt(INV_SORT_COMPARATOR2_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
new LongOpt(INV_PAIR_COMPARATOR_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
@@ -201,20 +206,14 @@ public static void mainHelper(final String[] args)
new LongOpt(IGNORE_NUMBERED_EXITS_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
};
- Getopt g =
- new Getopt(
- "daikon.diff.Diff", args,
- "Hhyduastmxno:jzpevl", longOpts);
+ DaikonGetopt g = new DaikonGetopt(args, "Hydastmxno:jpevl", longOpts, usage);
int c;
while ((c = g.getopt()) != -1) {
switch (c) {
case 0:
// got a long option
String optionName = longOpts[g.getLongind()].getName();
- if (Daikon.help_SWITCH.equals(optionName)) {
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- } else if (INV_SORT_COMPARATOR1_SWITCH.equals(optionName)) {
+ if (INV_SORT_COMPARATOR1_SWITCH.equals(optionName)) {
if (invSortComparator1Classname != null) {
throw new Error(
"multiple --"
@@ -252,12 +251,9 @@ public static void mainHelper(final String[] args)
ignoreNumberedExits = true;
break;
} else {
- throw new RuntimeException("Unknown long option received: " + optionName);
+ throw new Daikon.BugInDaikon("Unhandled long option " + optionName);
}
break;
- case 'h':
- System.out.println(usage);
- throw new Daikon.NormalTermination();
case 'H':
PrintAllVisitor.HUMAN_OUTPUT = true;
break;
@@ -318,13 +314,8 @@ public static void mainHelper(final String[] args)
case 'l':
logging = true;
break;
- case '?':
- // getopt() already printed an error
- System.out.println(usage);
- throw new Daikon.UserError("Bad argument");
default:
- System.out.println("getopt() returned " + c);
- break;
+ throw new Daikon.BugInDaikon("getopt() returned " + c);
}
}
@@ -422,8 +413,7 @@ public static void mainHelper(final String[] args)
v1.printAll();
return;
} else {
- System.out.println(usage);
- throw new Daikon.NormalTermination();
+ throw new Daikon.UserError("No invariant files specified" + Daikon.lineSep + usage);
}
if (logging) {
diff --git a/java/daikon/test/AllTestsSuite.java b/java/daikon/test/AllTestsSuite.java
index 7d74e7e7ac..9a817b266f 100644
--- a/java/daikon/test/AllTestsSuite.java
+++ b/java/daikon/test/AllTestsSuite.java
@@ -7,6 +7,7 @@
@RunWith(Suite.class)
@Suite.SuiteClasses({
daikon.chicory.RuntimeTest.class,
+ daikon.test.BadOptionTest.class,
daikon.test.TestClassOrInterfaceTypeDecorateVisitor.class,
daikon.test.TestAst.class,
daikon.test.config.ConfigurationTest.class,
diff --git a/java/daikon/test/BadOptionTest.java b/java/daikon/test/BadOptionTest.java
new file mode 100644
index 0000000000..67d118e64f
--- /dev/null
+++ b/java/daikon/test/BadOptionTest.java
@@ -0,0 +1,204 @@
+package daikon.test;
+
+import static java.nio.charset.StandardCharsets.UTF_8;
+import static org.junit.Assert.assertArrayEquals;
+import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertNotEquals;
+import static org.junit.Assert.assertThrows;
+
+import daikon.Daikon;
+import daikon.DaikonGetopt;
+import daikon.PrintInvariants;
+import daikon.SplitDtrace;
+import daikon.UnionInvariants;
+import daikon.tools.DtraceDiff;
+import daikon.tools.TraceSelect;
+import gnu.getopt.LongOpt;
+import java.io.ByteArrayOutputStream;
+import java.io.PrintStream;
+import org.junit.Test;
+import org.junit.function.ThrowingRunnable;
+
+/**
+ * Tests that Daikon tools reject bad command-line options with a UserError.
+ *
+ * These tests do not call {@code Daikon.mainHelper}, because it resets Daikon's global state,
+ * which other tests in the same JVM depend on.
+ */
+public class BadOptionTest {
+
+ /** The long options used by {@link #parse}. */
+ private static final LongOpt[] longopts =
+ new LongOpt[] {
+ new LongOpt("help", LongOpt.NO_ARGUMENT, null, 0),
+ new LongOpt("config", LongOpt.REQUIRED_ARGUMENT, null, 0),
+ new LongOpt("config_option", LongOpt.REQUIRED_ARGUMENT, null, 0),
+ new LongOpt("debug", LongOpt.REQUIRED_ARGUMENT, null, 'd'),
+ new LongOpt("verbose", LongOpt.NO_ARGUMENT, null, 'v'),
+ };
+
+ /**
+ * Parses the given command-line arguments, which must contain a bad option, and returns the
+ * resulting error message.
+ *
+ * @param args command-line arguments
+ * @return the message of the UserError for the bad option
+ */
+ private static String parse(String... args) {
+ DaikonGetopt g = new DaikonGetopt(args, "ho:", longopts);
+ Daikon.UserError e = assertThrows(Daikon.UserError.class, () -> consumeAll(g));
+ return String.valueOf(e.getMessage());
+ }
+
+ /**
+ * Calls {@code getopt()} until all command-line arguments have been processed.
+ *
+ * @param g the command-line parser
+ */
+ private static void consumeAll(DaikonGetopt g) {
+ while (g.getopt() != -1) {}
+ }
+
+ /**
+ * Returns the expected message for a bad option.
+ *
+ * @param description a description of the bad option
+ * @return the expected message for a bad option
+ */
+ private static String expected(String description) {
+ return description + "; run with -h for usage";
+ }
+
+ /** Tests an unrecognized long option. */
+ @Test
+ public void testUnrecognizedLongOption() {
+ assertEquals(expected("Unrecognized command-line option --bogus"), parse("--bogus"));
+ assertEquals(expected("Unrecognized command-line option --bogus"), parse("--bogus=3"));
+ assertEquals(expected("Unrecognized command-line option --=3"), parse("--=3"));
+ assertEquals(
+ expected("Unrecognized command-line option --bogus"), parse("-h", "--bogus", "file"));
+ }
+
+ /** Tests an unrecognized short option, alone and combined with a valid one. */
+ @Test
+ public void testUnrecognizedShortOption() {
+ assertEquals(expected("Unrecognized command-line option -x"), parse("-x"));
+ assertEquals(expected("Unrecognized command-line option -x"), parse("-xh"));
+ assertEquals(expected("Unrecognized command-line option -x"), parse("-hx"));
+ assertEquals(expected("Unrecognized command-line option -:"), parse("-:"));
+ }
+
+ /** Tests an ambiguous abbreviation of a long option. */
+ @Test
+ public void testAmbiguousLongOption() {
+ assertEquals(expected("Ambiguous command-line option --conf"), parse("--conf=x"));
+ assertEquals(expected("Ambiguous command-line option --conf"), parse("--conf"));
+ }
+
+ /** Tests that a usage hint of null appends nothing to the description of a bad option. */
+ @Test
+ public void testNoUsageHint() {
+ DaikonGetopt g = new DaikonGetopt(new String[] {"--bogus"}, "h", longopts);
+ g.setUsageHint(null);
+ Daikon.UserError e = assertThrows(Daikon.UserError.class, g::getopt);
+ assertEquals("Unrecognized command-line option --bogus", String.valueOf(e.getMessage()));
+ }
+
+ /** Tests options that are missing their required argument. */
+ @Test
+ public void testMissingArgument() {
+ assertEquals(expected("Command-line option --config requires an argument"), parse("--config"));
+ assertEquals(expected("Command-line option --debug requires an argument"), parse("--deb"));
+ assertEquals(expected("Command-line option -o requires an argument"), parse("-o"));
+ assertEquals(expected("Command-line option -o requires an argument"), parse("-ho"));
+ }
+
+ /** Tests options that are missing their required argument, when the optstring starts with ':'. */
+ @Test
+ public void testMissingArgumentLeadingColon() {
+ DaikonGetopt g = new DaikonGetopt(new String[] {"-o"}, ":ho:", longopts);
+ Daikon.UserError e = assertThrows(Daikon.UserError.class, g::getopt);
+ assertEquals(
+ expected("Command-line option -o requires an argument"), String.valueOf(e.getMessage()));
+ g = new DaikonGetopt(new String[] {"--config"}, ":ho:", longopts);
+ e = assertThrows(Daikon.UserError.class, g::getopt);
+ assertEquals(
+ expected("Command-line option --config requires an argument"),
+ String.valueOf(e.getMessage()));
+ }
+
+ /** Tests long options that are given an argument they do not take. */
+ @Test
+ public void testUnexpectedArgument() {
+ assertEquals(
+ expected("Command-line option --help does not take an argument"), parse("--help=x"));
+ assertEquals(
+ expected("Command-line option --verbose does not take an argument"), parse("--verb=x"));
+ }
+
+ /**
+ * Asserts that running {@code mainCall} throws a UserError with the given message.
+ *
+ * @param description a description of the bad option
+ * @param mainCall a call to a tool's {@code mainHelper} method
+ */
+ private static void assertBadOption(String description, ThrowingRunnable mainCall) {
+ Daikon.UserError e = assertThrows(Daikon.UserError.class, mainCall);
+ assertEquals(expected(description), String.valueOf(e.getMessage()));
+ }
+
+ /** Tests an unrecognized long option in a tool. */
+ @Test
+ public void testPrintInvariantsUnrecognizedOption() {
+ assertBadOption(
+ "Unrecognized command-line option --bogus",
+ () -> PrintInvariants.mainHelper(new String[] {"--bogus", "foo.inv.gz"}));
+ }
+
+ /** Tests that tools accept the {@code --help} option that their usage messages document. */
+ @Test
+ public void testHelpOption() {
+ assertPrintsUsage(() -> DtraceDiff.mainHelper(new String[] {"--help"}));
+ assertPrintsUsage(() -> UnionInvariants.mainHelper(new String[] {"--help"}));
+ assertPrintsUsage(() -> SplitDtrace.mainHelper(new String[] {"-h", "x"}));
+ assertPrintsUsage(() -> TraceSelect.mainHelper(new String[] {"--help"}));
+ assertPrintsUsage(() -> TraceSelect.mainHelper(new String[] {"20", "10", "-h", "x.dtrace"}));
+ }
+
+ /**
+ * Asserts that the given code prints a usage message to standard output and throws {@link
+ * Daikon.NormalTermination}. Captures the usage message so that it does not clutter the test
+ * output.
+ *
+ * @param code the code to run
+ */
+ private static void assertPrintsUsage(ThrowingRunnable code) {
+ PrintStream oldOut = System.out;
+ ByteArrayOutputStream bytes = new ByteArrayOutputStream();
+ System.setOut(new PrintStream(bytes, true, UTF_8));
+ try {
+ assertThrows(Daikon.NormalTermination.class, code);
+ } finally {
+ System.setOut(oldOut);
+ }
+ assertNotEquals("", bytes.toString(UTF_8).trim());
+ }
+
+ /** Tests {@link DaikonGetopt#nonOptionArgs}. */
+ @Test
+ public void testNonOptionArgs() {
+ assertArrayEquals(
+ new String[] {"a.dtrace", "b.dtrace"},
+ DaikonGetopt.nonOptionArgs(new String[] {"a.dtrace", "b.dtrace"}, "u"));
+ assertArrayEquals(
+ new String[] {"-a.dtrace"},
+ DaikonGetopt.nonOptionArgs(new String[] {"--", "-a.dtrace"}, "u"));
+ assertBadOption(
+ "Unrecognized command-line option --bogus",
+ () -> DaikonGetopt.nonOptionArgs(new String[] {"x", "--bogus"}, "u"));
+ assertBadOption(
+ "Unrecognized command-line option -x",
+ () -> DaikonGetopt.nonOptionArgs(new String[] {"-x"}, "u"));
+ assertPrintsUsage(() -> DaikonGetopt.nonOptionArgs(new String[] {"x", "--help"}, "u"));
+ }
+}
diff --git a/java/daikon/test/SampleTester.java b/java/daikon/test/SampleTester.java
index 40919edb6b..b984841454 100644
--- a/java/daikon/test/SampleTester.java
+++ b/java/daikon/test/SampleTester.java
@@ -8,6 +8,7 @@
import static org.junit.Assert.fail;
import daikon.Daikon;
+import daikon.DaikonGetopt;
import daikon.Debug;
import daikon.FileIO;
import daikon.Global;
@@ -18,7 +19,6 @@
import daikon.ValueTuple;
import daikon.VarInfo;
import daikon.inv.Invariant;
-import gnu.getopt.Getopt;
import gnu.getopt.LongOpt;
import java.io.File;
import java.io.IOException;
@@ -67,7 +67,7 @@ public class SampleTester {
/** The usage message for this program. */
private static String usage =
StringsPlume.joinLines(
- "Usage: java daikon.PrintInvariants [OPTION]... FILE",
+ "Usage: java daikon.test.SampleTester [OPTION]...",
" -h, --" + Daikon.help_SWITCH,
" Display this usage message",
" --" + Daikon.config_option_SWITCH,
@@ -78,8 +78,29 @@ public class SampleTester {
" Specify a class, varinfos, and ppt to debug track.",
" Format is class@ppt");
- @SuppressWarnings("JUnitMethodInvoked") // main() runs the tests without JUnit
+ /**
+ * Runs the tests without JUnit.
+ *
+ * @param args command-line arguments, like those of {@link #mainHelper}
+ * @throws IOException if there is a problem reading a test file
+ */
public static void main(String[] args) throws IOException {
+ try {
+ mainHelper(args);
+ } catch (Daikon.DaikonTerminationException e) {
+ Daikon.handleDaikonTerminationException(e);
+ }
+ }
+
+ /**
+ * This does the work of {@link #main(String[])}, but it never calls System.exit, so it is
+ * appropriate to be called programmatically.
+ *
+ * @param args command-line arguments, like those of {@link #main}
+ * @throws IOException if there is a problem reading a test file
+ */
+ @SuppressWarnings("JUnitMethodInvoked") // mainHelper() runs the tests without JUnit
+ public static void mainHelper(String[] args) throws IOException {
LongOpt[] longopts =
new LongOpt[] {
@@ -89,7 +110,7 @@ public static void main(String[] args) throws IOException {
new LongOpt(Daikon.track_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
};
- Getopt g = new Getopt("daikon.test.SampleTester", args, "h:", longopts);
+ DaikonGetopt g = new DaikonGetopt(args, "", longopts, usage);
int c;
while ((c = g.getopt()) != -1) {
switch (c) {
@@ -97,11 +118,7 @@ public static void main(String[] args) throws IOException {
// long option
case 0:
String option_name = longopts[g.getLongind()].getName();
- if (Daikon.help_SWITCH.equals(option_name)) {
- System.out.println(usage);
- throw new Daikon.NormalTermination();
-
- } else if (Daikon.config_option_SWITCH.equals(option_name)) {
+ if (Daikon.config_option_SWITCH.equals(option_name)) {
String item = Daikon.getOptarg(g);
daikon.config.Configuration.getInstance().apply(item);
break;
@@ -119,20 +136,12 @@ public static void main(String[] args) throws IOException {
"Error parsing track argument '" + Daikon.getOptarg(g) + "' - " + error);
}
} else {
- throw new RuntimeException("Unknown long option received: " + option_name);
+ throw new Daikon.BugInDaikon("Unhandled long option " + option_name);
}
break;
- case 'h':
- System.out.println(usage);
- throw new Daikon.NormalTermination();
-
- case '?':
- break; // getopt() already printed an error
-
default:
- System.out.println("getopt() returned " + c);
- break;
+ throw new Daikon.BugInDaikon("getopt() returned " + c);
}
}
diff --git a/java/daikon/test/split/SplitterFactoryTestUpdater.java b/java/daikon/test/split/SplitterFactoryTestUpdater.java
index 0c806f6071..c5be608fc7 100644
--- a/java/daikon/test/split/SplitterFactoryTestUpdater.java
+++ b/java/daikon/test/split/SplitterFactoryTestUpdater.java
@@ -195,7 +195,11 @@ private static String getTestClassText() {
ps.println("import java.io.*;");
ps.println("import java.util.*;");
ps.println("import junit.framework.*;");
+ ps.println("import org.junit.BeforeClass;");
ps.println("import org.junit.Test;");
+ ps.println("import org.junit.runner.JUnitCore;");
+ ps.println("import org.junit.runner.Result;");
+ ps.println("import org.junit.runner.notification.Failure;");
ps.println("import org.plumelib.util.FilesPlume;");
ps.println("import org.plumelib.util.StringsPlume;");
ps.println("import org.plumelib.util.UtilPlume;");
@@ -229,11 +233,6 @@ private static String getTestClassText() {
ps.println(" // java files it produces, changing the order that the setUpTests");
ps.println(" // commands are run will cause the tests to fail.");
ps.println();
- ps.println(" /** Do not instantiate. */");
- ps.println(" private SplitterFactoryTest() {");
- ps.println(" throw new Error(\"Do not instantiate\");");
- ps.println(" }");
- ps.println();
ps.println(" private static String targetDir = \"" + targetDir + "\";");
ps.println();
ps.println(" private static @Nullable String tempDir = null;");
@@ -242,31 +241,41 @@ private static String getTestClassText() {
ps.println();
ps.println(" private static String usage =");
ps.println(" StringsPlume.joinLines(");
- ps.println(" \"Usage: java daikon.tools.CreateSpinfo FILE.java ...\",");
+ ps.println(" \"Usage: java daikon.test.split.SplitterFactoryTest [OPTION]...\",");
ps.println(
- " \" -s Save (do not delete) the splitter java files in the temp directory\",");
- ps.println(" \" -h Display this usage message\");");
+ " \" -s Save (do not delete) the splitter java files in the temp"
+ + " directory\",");
+ ps.println(" \" -h, --help Display this usage message\");");
ps.println();
ps.println(" public static void main(String[] args) {");
- ps.println(
- " Getopt g = new Getopt(\"daikon.test.split.SplitterFactoryTest\", args, \"hs\");");
+ ps.println(" try {");
+ ps.println(" mainHelper(args);");
+ ps.println(" } catch (Daikon.DaikonTerminationException e) {");
+ ps.println(" Daikon.handleDaikonTerminationException(e);");
+ ps.println(" }");
+ ps.println(" }");
+ ps.println();
+ ps.println(" public static void mainHelper(String[] args) {");
+ ps.println(" DaikonGetopt g = new DaikonGetopt(args, \"s\", new LongOpt[0], usage);");
ps.println(" int c;");
ps.println(" while ((c = g.getopt()) != -1) {");
ps.println(" switch (c) {");
ps.println(" case 's':");
ps.println(" saveFiles = true;");
ps.println(" break;");
- ps.println(" case 'h':");
- ps.println(" System.out.println(usage);");
- ps.println(" System.exit(1);");
- ps.println(" break;");
- ps.println(" case '?':");
- ps.println(" break;");
ps.println(" default:");
- ps.println(" System.out.println(\"getopt() returned \" + c);");
- ps.println(" break;");
+ ps.println(" throw new Daikon.BugInDaikon(\"getopt() returned \" + c);");
ps.println(" }");
ps.println(" }");
+ ps.println(" Result result = JUnitCore.runClasses(SplitterFactoryTest.class);");
+ ps.println(" for (Failure failure : result.getFailures()) {");
+ ps.println(" System.out.println(failure.getTrace());");
+ ps.println(" }");
+ ps.println(" if (!result.wasSuccessful()) {");
+ ps.println(
+ " throw new Daikon.UserError(StringsPlume.nPlural(result.getFailureCount(), \"test\")"
+ + " + \" failed\");");
+ ps.println(" }");
ps.println(" }");
ps.println();
@@ -320,7 +329,8 @@ private static String getTestClassText() {
* SplitterFactoryTest to set up the needed files to run the tests on.
*/
public static void appendSetUpTest(PrintStream ps) {
- ps.println(" private static void setUpTests() {");
+ ps.println(" @BeforeClass");
+ ps.println(" public static void setUpTests() {");
ps.println(" List spinfoFiles;");
ps.println(" List declsFiles;");
for (int i = 0; i < spinfoFileLists.size(); i++) {
@@ -350,7 +360,7 @@ private static void appendTests(PrintStream ps) {
ps.println();
for (String className : classNames) {
ps.println(" @Test");
- ps.println(" public static void test" + className + "() {");
+ ps.println(" public void test" + className + "() {");
ps.println(" assertEqualFiles(\"" + className + ".java\");");
ps.println(" }");
ps.println();
diff --git a/java/daikon/tools/DtraceDiff.java b/java/daikon/tools/DtraceDiff.java
index 7d158ccc29..0fe001621e 100644
--- a/java/daikon/tools/DtraceDiff.java
+++ b/java/daikon/tools/DtraceDiff.java
@@ -6,6 +6,7 @@
import static daikon.tools.nullness.NullnessUtil.*;
import daikon.Daikon;
+import daikon.DaikonGetopt;
import daikon.FileIO;
import daikon.Global;
import daikon.PptMap;
@@ -124,7 +125,7 @@ public static void mainHelper(final String[] args) {
new LongOpt(Daikon.config_option_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
};
- Getopt g = new Getopt("daikon.tools.DtraceDiff", args, "h:", longopts);
+ DaikonGetopt g = new DaikonGetopt(args, "", longopts, usage);
int c;
while ((c = g.getopt()) != -1) {
switch (c) {
@@ -132,10 +133,7 @@ public static void mainHelper(final String[] args) {
// long option
case 0:
String option_name = longopts[g.getLongind()].getName();
- if (Daikon.help_SWITCH.equals(option_name)) {
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- } else if (Daikon.ppt_regexp_SWITCH.equals(option_name)) {
+ if (Daikon.ppt_regexp_SWITCH.equals(option_name)) {
if (Daikon.ppt_regexp != null) {
throw new Error(
"multiple --"
@@ -224,20 +222,11 @@ public static void mainHelper(final String[] args) {
Configuration.getInstance().apply(item);
break;
} else {
- throw new RuntimeException("Unknown long option received: " + option_name);
+ throw new Daikon.BugInDaikon("Unhandled long option " + option_name);
}
- // short options
- case 'h':
- System.out.println(usage);
- throw new Daikon.NormalTermination();
-
- case '?':
- break; // getopt() already printed an error
-
default:
- System.out.println("getopt() returned " + c);
- break;
+ throw new Daikon.BugInDaikon("getopt() returned " + c);
}
}
diff --git a/java/daikon/tools/DtraceNonceFixer.java b/java/daikon/tools/DtraceNonceFixer.java
index 942ed31dca..273e0de541 100644
--- a/java/daikon/tools/DtraceNonceFixer.java
+++ b/java/daikon/tools/DtraceNonceFixer.java
@@ -2,6 +2,7 @@
package daikon.tools;
+import daikon.DaikonGetopt;
import java.io.BufferedReader;
import java.io.IOException;
import java.io.PrintWriter;
@@ -53,14 +54,15 @@ public static void main(String[] args) {
* @param args command-line arguments, like those of {@link #main}
*/
public static void mainHelper(final String[] args) {
- if (args.length != 1) {
+ String[] files = DaikonGetopt.nonOptionArgs(args, usage);
+ if (files.length != 1) {
throw new daikon.Daikon.UserError(usage);
}
String outputFilename =
- args[0].endsWith(".gz") ? (args[0] + "_fixed.gz") : (args[0] + "_fixed");
+ files[0].endsWith(".gz") ? (files[0] + "_fixed.gz") : (files[0] + "_fixed");
- try (BufferedReader br1 = FilesPlume.newBufferedFileReader(args[0]);
+ try (BufferedReader br1 = FilesPlume.newBufferedFileReader(files[0]);
PrintWriter out1 = new PrintWriter(FilesPlume.newBufferedFileWriter(outputFilename))) {
// maxNonce - the biggest nonce ever found in the file
@@ -93,7 +95,7 @@ public static void mainHelper(final String[] args) {
// now go back and add the OBJECT and CLASS invocations
String allFixedFilename =
- outputFilename.endsWith(".gz") ? (args[0] + "_all_fixed.gz") : (args[0] + "_all_fixed");
+ outputFilename.endsWith(".gz") ? (files[0] + "_all_fixed.gz") : (files[0] + "_all_fixed");
try (BufferedReader br2 = FilesPlume.newBufferedFileReader(outputFilename);
PrintWriter out2 = new PrintWriter(FilesPlume.newBufferedFileWriter(allFixedFilename))) {
diff --git a/java/daikon/tools/ExtractConsequent.java b/java/daikon/tools/ExtractConsequent.java
index f2ecf3caf3..d4f94d9f49 100644
--- a/java/daikon/tools/ExtractConsequent.java
+++ b/java/daikon/tools/ExtractConsequent.java
@@ -5,6 +5,7 @@
import static java.util.logging.Level.INFO;
import daikon.Daikon;
+import daikon.DaikonGetopt;
import daikon.FileIO;
import daikon.Global;
import daikon.Ppt;
@@ -118,17 +119,14 @@ public static void mainHelper(final String[] args) throws IOException {
new LongOpt(Daikon.debugAll_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
new LongOpt(Daikon.debug_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
};
- Getopt g = new Getopt("daikon.ExtractConsequent", args, "h", longopts);
+ DaikonGetopt g = new DaikonGetopt(args, "", longopts, usage);
int c;
while ((c = g.getopt()) != -1) {
switch (c) {
case 0:
// got a long option
String option_name = longopts[g.getLongind()].getName();
- if (Daikon.help_SWITCH.equals(option_name)) {
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- } else if (Daikon.suppress_redundant_SWITCH.equals(option_name)) {
+ if (Daikon.suppress_redundant_SWITCH.equals(option_name)) {
Daikon.suppress_redundant_invariants_with_simplify = true;
} else if (Daikon.config_option_SWITCH.equals(option_name)) {
String item = Daikon.getOptarg(g);
@@ -139,17 +137,11 @@ public static void mainHelper(final String[] args) throws IOException {
} else if (Daikon.debug_SWITCH.equals(option_name)) {
daikon.LogHelper.setLevel(Daikon.getOptarg(g), FINE);
} else {
- throw new RuntimeException("Unknown long option received: " + option_name);
+ throw new Daikon.BugInDaikon("Unhandled long option " + option_name);
}
break;
- case 'h':
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- case '?':
- break; // getopt() already printed an error
default:
- System.out.println("getopt() returned " + c);
- break;
+ throw new Daikon.BugInDaikon("getopt() returned " + c);
}
}
// The index of the first non-option argument -- the name of the file
diff --git a/java/daikon/tools/InvariantChecker.java b/java/daikon/tools/InvariantChecker.java
index 70a3c804d1..3f8c7c56b7 100644
--- a/java/daikon/tools/InvariantChecker.java
+++ b/java/daikon/tools/InvariantChecker.java
@@ -4,6 +4,7 @@
import static java.util.logging.Level.INFO;
import daikon.Daikon;
+import daikon.DaikonGetopt;
import daikon.Debug;
import daikon.FileIO;
import daikon.Global;
@@ -135,20 +136,16 @@ public static void mainHelper(final String[] args)
new LongOpt(verbose_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
new LongOpt(Daikon.debugAll_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
new LongOpt(Daikon.debug_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
- new LongOpt(Daikon.ppt_regexp_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
new LongOpt(Daikon.track_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
};
- Getopt g = new Getopt("daikon.tools.InvariantChecker", args, "h", longopts);
+ DaikonGetopt g = new DaikonGetopt(args, "", longopts, usage);
int c;
while ((c = g.getopt()) != -1) {
switch (c) {
case 0:
// got a long option
String option_name = longopts[g.getLongind()].getName();
- if (Daikon.help_SWITCH.equals(option_name)) {
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- } else if (conf_SWITCH.equals(option_name)) {
+ if (conf_SWITCH.equals(option_name)) {
doConf = true;
} else if (filter_SWITCH.equals(option_name)) {
doFilter = true;
@@ -179,17 +176,11 @@ public static void mainHelper(final String[] args)
"Error parsing track argument '" + Daikon.getOptarg(g) + "' - " + error);
}
} else {
- throw new RuntimeException("Unknown long option received: " + option_name);
+ throw new Daikon.BugInDaikon("Unhandled long option " + option_name);
}
break;
- case 'h':
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- case '?':
- break; // getopt() already printed an error
default:
- System.out.println("getopt() returned " + c);
- break;
+ throw new Daikon.BugInDaikon("getopt() returned " + c);
}
}
diff --git a/java/daikon/tools/ReadTrace.java b/java/daikon/tools/ReadTrace.java
index b47369d795..944e3b3609 100644
--- a/java/daikon/tools/ReadTrace.java
+++ b/java/daikon/tools/ReadTrace.java
@@ -1,5 +1,7 @@
package daikon.tools;
+import daikon.Daikon;
+import daikon.DaikonGetopt;
import daikon.FileIO;
import daikon.PptMap;
import daikon.PptTopLevel;
@@ -32,6 +34,9 @@
*/
public class ReadTrace {
+ /** The usage message for this program. */
+ private static final String usage = "Usage: java daikon.tools.ReadTrace file1 file2 ...";
+
/** Do not instantiate. */
private ReadTrace() {
throw new UnsupportedOperationException("Do not instantiate");
@@ -43,11 +48,30 @@ private ReadTrace() {
* @param args data trace file names, read from the command line
*/
public static void main(String[] args) {
+ try {
+ mainHelper(args);
+ } catch (Daikon.DaikonTerminationException e) {
+ Daikon.handleDaikonTerminationException(e);
+ }
+ }
+
+ /**
+ * This does the work of {@link #main(String[])}, but it never calls System.exit, so it is
+ * appropriate to be called programmatically.
+ *
+ * @param args command-line arguments, like those of {@link #main}
+ */
+ public static void mainHelper(String[] args) {
+ String[] traceFiles = DaikonGetopt.nonOptionArgs(args, usage);
+ if (traceFiles.length == 0) {
+ throw new Daikon.UserError("No trace files specified" + Daikon.lineSep + usage);
+ }
CollectDataProcessor processor = new CollectDataProcessor();
PptMap ppts = new PptMap();
try {
// `read_data_trace_files()` requires the list of files to be modifiable.
- FileIO.read_data_trace_files(new ArrayList<>(Arrays.asList(args)), ppts, processor, false);
+ FileIO.read_data_trace_files(
+ new ArrayList<>(Arrays.asList(traceFiles)), ppts, processor, false);
} catch (Exception e) {
throw new Error(e);
}
diff --git a/java/daikon/tools/TraceSelect.java b/java/daikon/tools/TraceSelect.java
index 22f181956b..7bf9c29bd3 100644
--- a/java/daikon/tools/TraceSelect.java
+++ b/java/daikon/tools/TraceSelect.java
@@ -1,6 +1,7 @@
// TraceSelect.java
package daikon.tools;
+import daikon.DaikonGetopt;
import java.io.File;
import java.io.IOException;
import java.io.PrintWriter;
@@ -15,7 +16,6 @@
import java.util.Random;
import java.util.StringTokenizer;
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
-import org.checkerframework.checker.nullness.qual.RequiresNonNull;
import org.checkerframework.dataflow.qual.Pure;
import org.plumelib.util.FilesPlume;
import org.plumelib.util.MultiRandSelector;
@@ -40,10 +40,6 @@ private TraceSelect() {
private static @MonotonicNonNull String fileName = null;
- // Just a quick command line cache
- // ... but I think it would it be better to pass args to invokeDaikon
- // rather than introducing this variable.
- private static String @MonotonicNonNull [] argles;
// // stores the invocations in Strings
// private static ArrayList invokeBuffer;
@@ -52,7 +48,8 @@ private TraceSelect() {
// always set to non-null by mainHelper
private static @MonotonicNonNull Random randObj;
- private static int daikonArgStart = 0;
+ /** The arguments to pass to Daikon, other than the .dtrace file. */
+ private static List daikonArgs = new ArrayList<>();
// This allows us to simply call MultiDiff
// with the same files we just created.
@@ -63,7 +60,9 @@ private TraceSelect() {
private static final String usage =
StringsPlume.joinLines(
"USAGE: TraceSelect num_reps sample_size [options] [Daikon-args]...",
- "Example: java TraceSelect 20 10 -NOCLEAN -INCLUDE_UNRETURNED-SEED 1000 foo.dtrace"
+ "The options are -SEED n, -NOCLEAN, -INCLUDE_UNRETURNED, and -DO_DIFFS.",
+ "The Daikon-args start with the first argument that is not one of those options.",
+ "Example: java TraceSelect 20 10 -NOCLEAN -INCLUDE_UNRETURNED -SEED 1000 foo.dtrace"
+ " foo2.dtrace foo.decls RatPoly.decls foo3.dtrace");
/**
@@ -85,14 +84,28 @@ public static void main(String[] args) {
*
* @param args command-line arguments, like those of {@link #main}
*/
- public static void mainHelper(final String[] args) {
- argles = args;
- if (args.length == 0) {
- throw new daikon.Daikon.UserError("No arguments found." + daikon.Daikon.lineSep + usage);
+ public static void mainHelper(String[] args) {
+ // Handles -h and --help before num_reps.
+ args = DaikonGetopt.argsAfterLeadingOptions(args, usage);
+ // Reset the state from any previous call.
+ CLEAN = true;
+ INCLUDE_UNRETURNED = false;
+ DO_DIFFS = false;
+ daikonArgs = new ArrayList<>();
+ String inputFile = null;
+ Random rand = null;
+
+ if (args.length < 2) {
+ throw new daikon.Daikon.UserError("Too few arguments." + daikon.Daikon.lineSep + usage);
}
- num_reps = Integer.parseInt(args[0]);
- numPerSample = Integer.parseInt(args[1]);
+ try {
+ num_reps = Integer.parseInt(args[0]);
+ numPerSample = Integer.parseInt(args[1]);
+ } catch (NumberFormatException e) {
+ throw new daikon.Daikon.UserError(
+ "num_reps and sample_size must be integers." + daikon.Daikon.lineSep + usage);
+ }
// process optional switches
// also deduce index of arg for Daikon
@@ -101,17 +114,20 @@ public static void mainHelper(final String[] args) {
// allows seed setting
if (args[i].toUpperCase(Locale.ENGLISH).equals("-SEED")) {
if (i + 1 >= args.length) {
- throw new daikon.Daikon.UserError("-SEED options requires argument");
+ throw new daikon.Daikon.UserError("-SEED requires an argument");
+ }
+ String seed = args[++i];
+ try {
+ rand = new Random(Long.parseLong(seed));
+ } catch (NumberFormatException e) {
+ throw new daikon.Daikon.UserError("-SEED requires an integer argument, not " + seed);
}
- randObj = new Random(Long.parseLong(args[++i]));
- daikonArgStart = i + 1;
}
// NOCLEAN argument will leave the trace samples even after
// the invariants from these samples have been generated
else if (args[i].toUpperCase(Locale.ENGLISH).equals("-NOCLEAN")) {
CLEAN = false;
- daikonArgStart = i + 1;
}
// INCLUDE_UNRETURNED option will allow selecting method invocations
@@ -119,7 +135,6 @@ else if (args[i].toUpperCase(Locale.ENGLISH).equals("-NOCLEAN")) {
// either from a thrown Exception or abnormal termination.
else if (args[i].toUpperCase(Locale.ENGLISH).equals("-INCLUDE_UNRETURNED")) {
INCLUDE_UNRETURNED = true;
- daikonArgStart = i + 1;
}
// DO_DIFFS will create a spinfo file for generating
@@ -129,48 +144,45 @@ else if (args[i].toUpperCase(Locale.ENGLISH).equals("-INCLUDE_UNRETURNED")) {
// samples.
else if (args[i].toUpperCase(Locale.ENGLISH).equals("-DO_DIFFS")) {
DO_DIFFS = true;
- daikonArgStart = i + 1;
}
- // TODO: The current implementation assumes that a decls
- // or dtrace file will be the first of the Daikon arguments,
- // marking the end of the TraceSelect arguments. That is
- // not necessarily true, especially in cases when someone
- // uses a Daikon argument such as "--nohierarchy" or "--format java"
- // and the manual examples place the arguments before any dtrace
- // or decls arguments.
+ // The Daikon arguments start with the first argument that is not a TraceSelect switch,
+ // such as a .dtrace or .decls file, or "--nohierarchy" or "--format java".
+
+ // -h and --help before the Daikon arguments print the usage message.
+ else if (!knowArgStart
+ && (args[i].equals("-h") || args[i].equals("--" + daikon.Daikon.help_SWITCH))) {
+ System.out.println(usage);
+ throw new daikon.Daikon.NormalTermination();
+ }
// For now, only the first dtrace file will be sampled
else if (args[i].endsWith(".dtrace")) {
- if (fileName == null) {
- fileName = args[i];
+ if (inputFile == null) {
+ inputFile = args[i];
} else {
throw new daikon.Daikon.UserError("Only 1 dtrace file for input allowed");
}
- if (!knowArgStart) {
- daikonArgStart = i;
- knowArgStart = true;
- }
- } else if (args[i].endsWith(".decls")) {
- if (!knowArgStart) {
- daikonArgStart = i;
- knowArgStart = true;
- }
+ knowArgStart = true;
+ } else {
+ knowArgStart = true;
+ daikonArgs.add(args[i]);
}
}
// if no seed provided, use default Random() constructor
- if (randObj == null) {
- randObj = new Random();
- }
+ randObj = (rand != null) ? rand : new Random();
sampleNames = new String[num_reps + 1];
sampleNames[0] = "-p";
- if (fileName == null) {
- throw new daikon.Daikon.UserError("No .dtrace file name specified");
+ if (inputFile == null) {
+ throw new daikon.Daikon.UserError(
+ "No .dtrace file name specified (the trace file must be uncompressed and its name must"
+ + " end with \".dtrace\")");
}
+ fileName = inputFile;
try {
@@ -267,7 +279,6 @@ private static void deleteQuietly(String fileName) {
}
}
- @RequiresNonNull("argles")
private static void invokeDaikon(String dtraceName) throws IOException {
System.out.println("Created file: " + dtraceName);
@@ -278,14 +289,8 @@ private static void invokeDaikon(String dtraceName) throws IOException {
daikonArgsList.add("-o");
daikonArgsList.add(dtraceName + ".inv");
- // find all the Daikon args except for the original
- // single dtrace file.
- for (int i = daikonArgStart; i < argles.length; i++) {
- if (argles[i].endsWith(".dtrace")) {
- continue;
- }
- daikonArgsList.add(argles[i]);
- }
+ // all the Daikon args except for the original single dtrace file
+ daikonArgsList.addAll(daikonArgs);
// create an array to store the Strings in daikonArgsList
String[] daikonArgs = daikonArgsList.toArray(new String[0]);
diff --git a/java/daikon/tools/compare/LogicalCompare.java b/java/daikon/tools/compare/LogicalCompare.java
index bbbc6df993..371d26ea25 100644
--- a/java/daikon/tools/compare/LogicalCompare.java
+++ b/java/daikon/tools/compare/LogicalCompare.java
@@ -5,6 +5,7 @@
import static java.util.logging.Level.INFO;
import daikon.Daikon;
+import daikon.DaikonGetopt;
import daikon.FileIO;
import daikon.Global;
import daikon.PptMap;
@@ -658,7 +659,6 @@ public static void mainHelper(final String[] args)
new LongOpt(Daikon.debugAll_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
new LongOpt(Daikon.debug_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
new LongOpt("filters", LongOpt.REQUIRED_ARGUMENT, null, 0),
- new LongOpt("help", LongOpt.NO_ARGUMENT, null, 0),
new LongOpt("minimize-classes", LongOpt.NO_ARGUMENT, null, 0),
new LongOpt("no-post-after-pre-failure", LongOpt.NO_ARGUMENT, null, 0),
new LongOpt("post-after-pre-failure", LongOpt.NO_ARGUMENT, null, 0),
@@ -675,7 +675,7 @@ public static void mainHelper(final String[] args)
extra_assumptions = new LinkedHashMap<>();
- Getopt g = new Getopt("daikon.tools.compare.LogicalCompare", args, "h", longopts);
+ DaikonGetopt g = new DaikonGetopt(args, "", longopts, usage);
int c;
boolean user_filters = false;
while ((c = g.getopt()) != -1) {
@@ -683,10 +683,7 @@ public static void mainHelper(final String[] args)
case 0:
// got a long option
String option_name = longopts[g.getLongind()].getName();
- if (Daikon.help_SWITCH.equals(option_name)) {
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- } else if (option_name.equals("config-file")) {
+ if (option_name.equals("config-file")) {
String config_file = Daikon.getOptarg(g);
try (InputStream stream = new FileInputStream(config_file)) {
Configuration.getInstance().apply(stream);
@@ -727,15 +724,11 @@ public static void mainHelper(final String[] args)
} else if (option_name.equals("minimize-classes")) {
opt_minimize_classes = true;
} else {
- throw new Error();
+ throw new Daikon.BugInDaikon("Unhandled long option " + option_name);
}
break;
- case 'h':
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- case '?':
- // getopt() already printed an error
- throw new Daikon.UserError("Bad argument");
+ default:
+ throw new Daikon.BugInDaikon("getopt() returned " + c);
}
}
diff --git a/java/daikon/tools/jtb/Annotate.java b/java/daikon/tools/jtb/Annotate.java
index 9635cc5912..cee7292928 100644
--- a/java/daikon/tools/jtb/Annotate.java
+++ b/java/daikon/tools/jtb/Annotate.java
@@ -24,8 +24,7 @@
*
* The first argument is a Daikon {@code .inv} file -- a serialized file of Invariant objects.
* All subsequent arguments are {@code Foo.java} files that are rewritten into {@code
- * Foo.java-jmlannotated} versions; alternately, use the {@code -r} flag to process every {@code
- * .java} file under the current directory.
+ * Foo.java-jmlannotated} versions.
*/
public class Annotate {
@@ -88,10 +87,9 @@ private Annotate() {
private static String usage =
StringsPlume.joinLines(
"Usage: java daikon.tools.Annotate FILE.inv FILE.java ...",
- " -h Display this usage message",
+ " -h, --help Display this usage message",
" -i Insert invariants not supported by ESC with \"!\" instead of \"@\";",
" by default these \"inexpressible\" invariants are simply omitted",
- " -r Use all .java files under the current directory as arguments",
" -s Use // comments rather than /* comments",
" --format name Insert specifications in the given format: DBC, ESC, JML, Java",
" --wrap_xml Wrap each annotation and auxiliary information in XML tags",
@@ -132,7 +130,6 @@ public static void mainHelper(final String[] args) throws Exception {
Daikon.output_format = OutputFormat.ESCJAVA;
LongOpt[] longopts =
new LongOpt[] {
- new LongOpt(Daikon.help_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
new LongOpt(Daikon.debugAll_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
new LongOpt(Daikon.debug_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
new LongOpt(Daikon.format_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
@@ -140,7 +137,7 @@ public static void mainHelper(final String[] args) throws Exception {
new LongOpt(max_invariants_pp_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
new LongOpt(no_reflection_SWITCH, LongOpt.NO_ARGUMENT, null, 0)
};
- Getopt g = new Getopt("daikon.tools.jtb.Annotate", args, "hs", longopts);
+ DaikonGetopt g = new DaikonGetopt(args, "is", longopts, usage);
int c;
while ((c = g.getopt()) != -1) {
switch (c) {
@@ -148,10 +145,7 @@ public static void mainHelper(final String[] args) throws Exception {
// got a long option
String option_name = longopts[g.getLongind()].getName();
- if (Daikon.help_SWITCH.equals(option_name)) {
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- } else if (no_reflection_SWITCH.equals(option_name)) {
+ if (no_reflection_SWITCH.equals(option_name)) {
useReflection = false;
} else if (max_invariants_pp_SWITCH.equals(option_name)) {
try {
@@ -181,12 +175,9 @@ public static void mainHelper(final String[] args) throws Exception {
setLightweight = true;
}
} else {
- throw new Daikon.UserError("Unknown long option received: " + option_name);
+ throw new Daikon.BugInDaikon("Unhandled long option " + option_name);
}
break;
- case 'h':
- System.out.println(usage);
- throw new Daikon.NormalTermination();
case 'i':
insert_inexpressible = true;
break;
@@ -200,11 +191,8 @@ public static void mainHelper(final String[] args) throws Exception {
case 's':
slashslash = true;
break;
- case '?':
- break; // getopt() already printed an error
default:
- System.out.println("getopt() returned " + c);
- break;
+ throw new Daikon.BugInDaikon("getopt() returned " + c);
}
}
diff --git a/java/daikon/tools/jtb/CreateSpinfo.java b/java/daikon/tools/jtb/CreateSpinfo.java
index 56f1b154e2..76d4b23b05 100644
--- a/java/daikon/tools/jtb/CreateSpinfo.java
+++ b/java/daikon/tools/jtb/CreateSpinfo.java
@@ -83,40 +83,30 @@ public static void mainHelper(final String[] args) throws IOException {
daikon.LogHelper.setupLogs(INFO);
LongOpt[] longopts =
new LongOpt[] {
- new LongOpt(Daikon.help_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
new LongOpt(Daikon.debugAll_SWITCH, LongOpt.NO_ARGUMENT, null, 0),
new LongOpt(Daikon.debug_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
};
- Getopt g = new Getopt("daikon.tools.jtb.CreateSpinfo", args, "ho:", longopts);
+ DaikonGetopt g = new DaikonGetopt(args, "o:", longopts, usage);
int c;
while ((c = g.getopt()) != -1) {
switch (c) {
case 0:
// got a long option
String option_name = longopts[g.getLongind()].getName();
- if (Daikon.help_SWITCH.equals(option_name)) {
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- } else if (Daikon.debugAll_SWITCH.equals(option_name)) {
+ if (Daikon.debugAll_SWITCH.equals(option_name)) {
Global.debugAll = true;
} else if (Daikon.debug_SWITCH.equals(option_name)) {
daikon.LogHelper.setLevel(Daikon.getOptarg(g), FINE);
} else {
- throw new RuntimeException("Unknown long option received: " + option_name);
+ throw new Daikon.BugInDaikon("Unhandled long option " + option_name);
}
break;
case 'o':
outputfilename = Daikon.getOptarg(g);
break;
- case 'h':
- System.out.println(usage);
- throw new Daikon.NormalTermination();
- case '?':
- break; // getopt() already printed an error
default:
- System.out.println("getopt() returned " + c);
- break;
+ throw new Daikon.BugInDaikon("getopt() returned " + c);
}
}
diff --git a/java/daikon/tools/jtb/CreateSpinfoC.java b/java/daikon/tools/jtb/CreateSpinfoC.java
index 8cb338947b..391ae18ffd 100644
--- a/java/daikon/tools/jtb/CreateSpinfoC.java
+++ b/java/daikon/tools/jtb/CreateSpinfoC.java
@@ -2,6 +2,8 @@
import static java.nio.charset.StandardCharsets.UTF_8;
+import daikon.Daikon;
+import daikon.DaikonGetopt;
import java.io.File;
import java.io.FileInputStream;
import java.io.IOException;
@@ -21,21 +23,49 @@ private CreateSpinfoC() {
throw new UnsupportedOperationException("Do not instantiate");
}
+ /** The usage message for this program. */
+ private static final String usage =
+ "C Parser Version 0.1Alpha: Usage: java daikon.tools.jtb.CreateSpinfoC inputfile";
+
+ /**
+ * The entry point for CreateSpinfoC.
+ *
+ * @param args one argument, the name of the C file
+ */
public static void main(String[] args) {
- if (args.length == 1) {
- System.out.println("Create spinfo file from file " + args[0] + " . . .");
- } else {
- System.out.println("C Parser Version 0.1Alpha: Usage is one of:");
- System.out.println(" java CreateSpinfoC < inputfile");
- System.out.println("OR");
- System.out.println(" java CreateSpinfoC inputfile");
- return;
+ try {
+ mainHelper(args);
+ } catch (Daikon.DaikonTerminationException e) {
+ Daikon.handleDaikonTerminationException(e);
+ }
+ }
+
+ /**
+ * This does the work of {@link #main(String[])}, but it never calls System.exit, so it is
+ * appropriate to be called programmatically.
+ *
+ * @param args command-line arguments, like those of {@link #main}
+ */
+ public static void mainHelper(String[] args) {
+ String[] files = DaikonGetopt.nonOptionArgs(args, usage);
+ if (files.length != 1) {
+ throw new Daikon.UserError(usage);
}
+ String inputFile = files[0];
+ int dotPos = inputFile.lastIndexOf('.');
+ // On Windows, both '/' and '\\' are separators.
+ int separatorPos =
+ Math.max(inputFile.lastIndexOf('/'), inputFile.lastIndexOf(File.separatorChar));
+ if (dotPos <= separatorPos) {
+ throw new Daikon.UserError(
+ "File name has no extension: " + inputFile + Daikon.lineSep + usage);
+ }
+ String fileName = inputFile.substring(0, dotPos);
+ System.out.println("Create spinfo file from file " + inputFile + " . . .");
+ File temp = new File(fileName + ".temp");
try {
- String fileName = args[0].substring(0, args[0].lastIndexOf('.'));
- File temp = new File(fileName + ".temp");
// filter out the '\f' characters in the file
- try (Reader reader = Files.newBufferedReader(Paths.get(args[0]), UTF_8);
+ try (Reader reader = Files.newBufferedReader(Paths.get(inputFile), UTF_8);
Writer writer = Files.newBufferedWriter(temp.toPath(), UTF_8)) {
int c;
while ((c = reader.read()) != -1) {
@@ -44,39 +74,35 @@ public static void main(String[] args) {
}
}
} catch (IOException e) {
- System.out.println(e.getMessage());
- if (temp != null) {
- temp.delete();
- }
- System.exit(1);
- throw new Error("unreachable");
+ throw new Daikon.UserError(e, "Problem copying " + inputFile + " to " + temp);
}
+ TranslationUnit root;
try (FileInputStream fis = new FileInputStream(temp)) {
@SuppressWarnings("UnusedVariable") // sets static variables for TranslationUnit()
CParser parser = new CParser(fis);
+ // The parser reads lazily, so the stream must be open while it parses.
+ root = CParser.TranslationUnit();
} catch (IOException e) {
throw new UncheckedIOException("problem reading " + temp, e);
+ } catch (ParseException e) {
+ throw new Daikon.UserError(e, "CreateSpinfoC encountered errors during parse");
}
- TranslationUnit root = CParser.TranslationUnit();
StringFinder finder = new StringFinder();
- temp.delete();
root.accept(finder);
- ConditionPrinter printer;
+ String spinfoFile = fileName + ".spinfo";
try {
- printer = new ConditionPrinter(fileName + ".spinfo");
+ ConditionPrinter printer = new ConditionPrinter(spinfoFile);
printer.setActualStrings(finder.functionStringMapping);
printer.setStringArrays(finder.stringMatrices);
root.accept(printer);
printer.close();
} catch (IOException e) {
- System.out.println("File IO Error");
- System.out.println(e.getMessage());
+ throw new Daikon.UserError(e, "Problem writing " + spinfoFile);
}
System.out.println("CreateSpinfoC: C program parsed successfully.");
- } catch (ParseException e) {
- System.out.println("CreateSpinfoC encountered errors during parse.");
- System.out.println(e.getMessage());
+ } finally {
+ temp.delete();
}
}
}
diff --git a/java/daikon/tools/runtimechecker/CommandHandler.java b/java/daikon/tools/runtimechecker/CommandHandler.java
index 7097f6ac9d..f54877aa81 100644
--- a/java/daikon/tools/runtimechecker/CommandHandler.java
+++ b/java/daikon/tools/runtimechecker/CommandHandler.java
@@ -2,10 +2,13 @@
import static java.nio.charset.StandardCharsets.UTF_8;
+import daikon.Daikon;
import java.io.BufferedReader;
+import java.io.ByteArrayOutputStream;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
+import java.io.PrintStream;
import java.io.UncheckedIOException;
/**
@@ -22,20 +25,41 @@ public boolean handle(String[] args) {
throw new UnsupportedOperationException();
}
+ /** Prints the usage message to standard error. */
public void usageMessage() {
+ usageMessage(System.err);
+ }
+
+ /**
+ * Returns the usage message.
+ *
+ * @return the usage message
+ */
+ public String usageMessageString() {
+ ByteArrayOutputStream bytes = new ByteArrayOutputStream();
+ usageMessage(new PrintStream(bytes, true, UTF_8));
+ return bytes.toString(UTF_8).stripTrailing();
+ }
+
+ /**
+ * Prints the usage message.
+ *
+ * @param out where to print the usage message
+ * @throws Daikon.BugInDaikon if the documentation file is missing
+ */
+ public void usageMessage(PrintStream out) {
String[] classnameArray = getClass().getName().split("\\.");
String simpleClassname = classnameArray[classnameArray.length - 1];
String docFile = simpleClassname + ".doc";
InputStream in = getClass().getResourceAsStream(docFile);
if (in == null) {
- System.err.println("Didn't find documentation for " + getClass());
- return;
+ throw new Daikon.BugInDaikon("Didn't find documentation " + docFile + " for " + getClass());
}
try (BufferedReader reader = new BufferedReader(new InputStreamReader(in, UTF_8))) {
String line;
while ((line = reader.readLine()) != null) {
- System.err.println(line);
+ out.println(line);
}
} catch (IOException e) {
throw new UncheckedIOException("problem reading " + docFile, e);
diff --git a/java/daikon/tools/runtimechecker/InstrumentHandler.doc b/java/daikon/tools/runtimechecker/InstrumentHandler.doc
index 84ddec8845..b4d7089ab5 100644
--- a/java/daikon/tools/runtimechecker/InstrumentHandler.doc
+++ b/java/daikon/tools/runtimechecker/InstrumentHandler.doc
@@ -7,6 +7,7 @@ instrument [OPTIONS] INV_FILE JAVA_FILES
INV_FILE is an invariant file (suffix .inv or .inv.gz) created by Daikon.
JAVA_FILES is one or more Java files that will be instrumented.
OPTIONS:
+ -h, --help Display this usage message.
--make_all_fields_public Make all declared fields public.
--directory=DIRNAME Output directory; default: instrumented-classes
--output_only_high_conf_invariants
diff --git a/java/daikon/tools/runtimechecker/InstrumentHandler.java b/java/daikon/tools/runtimechecker/InstrumentHandler.java
index ffd4e77a48..39f5a375a9 100644
--- a/java/daikon/tools/runtimechecker/InstrumentHandler.java
+++ b/java/daikon/tools/runtimechecker/InstrumentHandler.java
@@ -5,17 +5,18 @@
import static java.util.logging.Level.INFO;
import daikon.Daikon;
+import daikon.DaikonGetopt;
import daikon.FileIO;
import daikon.Global;
import daikon.PptMap;
import daikon.tools.jtb.ParseResults;
-import gnu.getopt.Getopt;
import gnu.getopt.LongOpt;
import java.io.File;
import java.io.IOException;
import java.io.Writer;
import java.nio.file.Files;
import java.util.ArrayList;
+import java.util.Arrays;
import java.util.List;
import java.util.logging.Logger;
import jtb.syntaxtree.*;
@@ -81,11 +82,17 @@ public boolean handle(String[] args) {
return false;
}
- String[] realArgs = new String[args.length - 1];
- for (int i = 0; i < realArgs.length; i++) {
- realArgs[i] = args[i + 1];
+ String[] realArgs = Arrays.copyOfRange(args, 1, args.length);
+ Arguments arguments;
+ try {
+ arguments = readArguments(realArgs);
+ } catch (Daikon.NormalTermination e) {
+ // The user requested the usage message, which has been printed.
+ return true;
+ } catch (Daikon.UserError e) {
+ System.err.println(e.getMessage());
+ return false;
}
- Arguments arguments = readArguments(realArgs);
if (arguments == errorWhileReadingArguments) {
return false;
}
@@ -213,7 +220,9 @@ private Arguments readArguments(String[] args) {
new LongOpt(directory_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0),
new LongOpt(checkers_directory_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0)
};
- Getopt g = new Getopt("daikon.tools.runtimechecker.InstrumentHandler", args, "hs", longopts);
+ DaikonGetopt g = new DaikonGetopt(args, "", longopts, this::usageMessageString);
+ // The caller prints the usage message when this command fails.
+ g.setUsageHint(null);
int c;
while ((c = g.getopt()) != -1) {
switch (c) {
@@ -236,12 +245,11 @@ private Arguments readArguments(String[] args) {
} else if (Daikon.debug_SWITCH.equals(option_name)) {
daikon.LogHelper.setLevel(Daikon.getOptarg(g), FINE);
} else {
- System.err.println("Unknown long option received: " + option_name);
+ throw new Daikon.BugInDaikon("Unhandled long option " + option_name);
}
break;
default:
- System.out.println("unrecognized option" + c);
- return errorWhileReadingArguments;
+ throw new Daikon.BugInDaikon("getopt() returned " + c);
}
}
// The index of the first non-option argument -- the name of the
diff --git a/java/daikon/tools/runtimechecker/Main.java b/java/daikon/tools/runtimechecker/Main.java
index 9259e07f45..188b747947 100644
--- a/java/daikon/tools/runtimechecker/Main.java
+++ b/java/daikon/tools/runtimechecker/Main.java
@@ -1,8 +1,11 @@
package daikon.tools.runtimechecker;
+import daikon.Daikon;
+import daikon.DaikonGetopt;
import java.util.Collections;
import java.util.List;
import java.util.Locale;
+import java.util.StringJoiner;
/**
* Main entrypoint for the instrumenter. Passes control to whichever handler can handle the
@@ -10,10 +13,19 @@
*/
public class Main extends CommandHandler {
- protected void usageMessage(List handlers) {
+ /**
+ * Returns the usage message of this and of each handler.
+ *
+ * @param handlers the handlers whose usage messages to include
+ * @return the usage message of this and of each handler
+ */
+ private String usageMessage(List handlers) {
+ StringJoiner result = new StringJoiner(Daikon.lineSep);
+ result.add(usageMessageString());
for (CommandHandler h : handlers) {
- h.usageMessage();
+ result.add(h.usageMessageString());
}
+ return result.toString();
}
/**
@@ -27,19 +39,26 @@ public void nonStaticMain(String[] args) {
List handlers =
Collections.singletonList((CommandHandler) new InstrumentHandler());
- if (args.length < 1) {
+ String[] commandAndArgs;
+ try {
+ commandAndArgs = DaikonGetopt.argsAfterLeadingOptions(args, () -> usageMessage(handlers));
+ } catch (Daikon.DaikonTerminationException e) {
+ Daikon.handleDaikonTerminationException(e);
+ return;
+ }
+ if (commandAndArgs.length < 1) {
System.err.println("ERROR: No command given.");
System.err.println(
"For more help, invoke the instrumenter with \"help\" as its sole argument.");
System.exit(1);
}
- if (args[0].toUpperCase(Locale.ENGLISH).equals("HELP") || args[0].equals("?")) {
- usageMessage();
- usageMessage(handlers);
+ if (commandAndArgs[0].toUpperCase(Locale.ENGLISH).equals("HELP")
+ || commandAndArgs[0].equals("?")) {
+ System.out.println(usageMessage(handlers));
System.exit(0);
}
- String command = args[0];
+ String command = commandAndArgs[0];
boolean success = false;
@@ -49,7 +68,7 @@ public void nonStaticMain(String[] args) {
for (CommandHandler handler : handlers) {
if (handler.handles(command)) {
h = handler;
- success = h.handle(args);
+ success = h.handle(commandAndArgs);
if (!success) {
System.err.println("The command you issued returned a failing status flag.");
}
@@ -69,7 +88,12 @@ public void nonStaticMain(String[] args) {
System.err.println(
"For more help, invoke the instrumenter with \"help\" as its sole argument.");
} else {
- h.usageMessage();
+ // Don't let a problem printing the usage message prevent the exit below.
+ try {
+ h.usageMessage();
+ } catch (RuntimeException e) {
+ System.err.println(e.getMessage());
+ }
}
System.exit(1);
} else {
diff --git a/java/daikon/tools/runtimechecker/WriteViolationFile.java b/java/daikon/tools/runtimechecker/WriteViolationFile.java
index dcfb548648..ee16a07420 100644
--- a/java/daikon/tools/runtimechecker/WriteViolationFile.java
+++ b/java/daikon/tools/runtimechecker/WriteViolationFile.java
@@ -2,6 +2,8 @@
import static java.nio.charset.StandardCharsets.UTF_8;
+import daikon.Daikon;
+import daikon.DaikonGetopt;
import java.io.BufferedWriter;
import java.io.IOException;
import java.io.UncheckedIOException;
@@ -11,8 +13,10 @@
import java.nio.file.Files;
import java.nio.file.Path;
import java.nio.file.Paths;
+import java.util.Arrays;
import java.util.List;
import org.checkerframework.checker.signature.qual.BinaryName;
+import org.plumelib.util.StringsPlume;
/**
* This program runs a given program (which is assumed to contain some classes that have been
@@ -26,27 +30,35 @@ private WriteViolationFile() {
throw new UnsupportedOperationException("Do not instantiate");
}
+ /** The usage message for this program. */
+ private static final String usageMessage =
+ StringsPlume.joinLines(
+ "Usage: java WriteViolationFile CLASS ARGS",
+ " CLASS and ARGS are just as they would be when being run directly,",
+ " except that CLASS is written as a binary name, not a fully-qualified name",
+ "Output is written to file \"violations.txt\" in the current directory.");
+
public static void usage() {
- System.out.println("Usage: java WriteViolationFile CLASS ARGS");
- System.out.println(" CLASS and ARGS are just as they would be when being run directly,");
- System.out.println(
- " except that CLASS is written as a binary name, not a fully-qualified name");
- System.out.println("Output is written to file \"violations.txt\" in the current directory.");
+ System.out.println(usageMessage);
}
@SuppressWarnings("Finally")
public static void main(String[] args) {
- if (args.length == 0) {
+ String[] classAndArgs;
+ try {
+ classAndArgs = DaikonGetopt.argsAfterLeadingOptions(args, usageMessage);
+ } catch (Daikon.DaikonTerminationException e) {
+ Daikon.handleDaikonTerminationException(e);
+ return;
+ }
+ if (classAndArgs.length == 0) {
System.out.println("Error: no class specified");
usage();
System.exit(1);
}
@SuppressWarnings("signature") // will be checked immediately below, and exception is caught
- @BinaryName String class_name = args[0];
- String[] main_args = new String[args.length - 1];
- for (int i = 0; i < main_args.length; i++) {
- main_args[i] = args[i + 1];
- }
+ @BinaryName String class_name = classAndArgs[0];
+ String[] main_args = Arrays.copyOfRange(classAndArgs, 1, classAndArgs.length);
Class cls;
try {
cls = Class.forName(class_name);
diff --git a/tests/diff-tests/Makefile.common b/tests/diff-tests/Makefile.common
index 7a22461dfd..014605b8b4 100644
--- a/tests/diff-tests/Makefile.common
+++ b/tests/diff-tests/Makefile.common
@@ -20,10 +20,10 @@ INV_FILES := $(PROGRAM)-1.inv.gz $(PROGRAM)-2.inv.gz
# An output file must satisfy the pattern program%.txt, where the % is
# the options passed to Diff
## Must reinstate -a and -ap and -p in V3 as soon as possible. -MDE 6/10/2003
-# OUTPUT := $(PROGRAM).txt $(PROGRAM)-u.txt $(PROGRAM)-a.txt $(PROGRAM)-p.txt \
+# OUTPUT := $(PROGRAM).txt $(PROGRAM)-a.txt $(PROGRAM)-p.txt \
# $(PROGRAM)-e.txt $(PROGRAM)-ap.txt $(PROGRAM)-t.txt \
# $(PROGRAM)-jt.txt
-OUTPUT := $(PROGRAM).txt $(PROGRAM)-u.txt \
+OUTPUT := $(PROGRAM).txt \
$(PROGRAM)-e.txt $(PROGRAM)-t.txt \
$(PROGRAM)-jt.txt
# Must be handled differently than OUTPUT, because map files are
diff --git a/tests/diff-tests/StackAr/StackAr-u.txt.goal b/tests/diff-tests/StackAr/StackAr-u.txt.goal
deleted file mode 100644
index f3164de375..0000000000
--- a/tests/diff-tests/StackAr/StackAr-u.txt.goal
+++ /dev/null
@@ -1,105 +0,0 @@
-(I)V:::ENTER>
- = 0 {0+}, capacity >= 2 {1-}> (UInt,DJU)
- (U!Int,DUU)
-(I)V:::EXIT>
- (Bin,MJ)
- (Bin,MJ)
- = -1 {0.8136-}, this.topOfStack >= -1 {0.8333-}> (U!Int,SUU)
- (UInt,SJU)
- (U!Int,DUU)
- (U!Int,SUU)
- (UInt,SJU)
- (UInt,MJ)
-
- = -1 {0+}, this.topOfStack >= -1 {0+}> (U!Int,SJJ)
- (U!Int,DJU)
- (U!Int,DUU)
- (UInt,MJ)
-
- = -1 {0+}, this.topOfStack >= -1 {0+}> (U!Int,SJJ)
- (U!Int,DJU)
- (U!Int,DJU)
- (U!Int,DUU)
- (UInt,MJ)
-
- (Bin,MJ)
- = -1 {0+}, this.topOfStack >= -1 {0+}> (U!Int,SJJ)
- (U!Int,DJJ)
- (U!Int,DUU)
-
- (Bin,MJ)
- = -1 {0+}, this.topOfStack >= -1 {0+}> (U!Int,SJJ)
- (UInt,MJ)
- (U!Int,DJJ)
- (U!Int,DJJ)
- (U!Int,DUU)
-
- (Bin,JM)
- = -1 {0+}, this.topOfStack >= 9223372036854775807 {1-}> (U!Int,DJU)
- (U!Int,UM)
- (U!Int,DUU)
- (UInt,JM)
- (UInt,JM)
- (UInt,DJU)
-
- (Bin,JM)
- (Bin,JM)
- (Bin,JM)
- (Bin,JM)
- (Bin,JM)
- = -1 {0+}, null> (U!Int,JM)
- = -1 {0.8205-}, this.topOfStack >= 9223372036854775807 {1-}> (U!Int,DUU)
- (UInt,DJU)
- (U!Int,UM)
- (U!Int,UM)
- (U!Int,UM)
- (U!Int,DUU)
- (UInt,DJU)
- (UInt,JM)
- (UInt,JM)
- (UInt,DJU)
- (UInt,DJU)
-
- = 9223372036854775807 {1-}, this.topOfStack >= 9223372036854775807 {1-}> (U!Int,SUU)
- (U!Int,SUU)
-
- = 9223372036854775807 {1-}, this.topOfStack >= 9223372036854775807 {1-}> (U!Int,SUU)
- (U!Int,SUU)
-
- = -1 {0+}, this.topOfStack >= -1 {0+}> (U!Int,SJJ)
- (U!Int,DJJ)
- (U!Int,DUU)
-
- = -1 {0+}, orig(this.topOfStack) >= -1 {0+}> (U!Int,SJJ)
- (U!Int,DUU)
- (U!Int,DJJ)
- (U!Int,DJJ)
- (U!Int,DUU)
-
- = -1 {0+}, this.topOfStack >= 0 {0+}> (UInt,DJJ)
- (U!Int,DJJ)
- (U!Int,DUU)
-
- (Bin,MJ)
- (Bin,MJ)
- (Bin,MJ)
- (Bin,MJ)
- = -1 {0+}, this.topOfStack >= 0 {0+}> (UInt,DJJ)
- (UInt,MJ)
- (U!Int,DJJ)
- (U!Int,DJJ)
- (U!Int,DUU)
-
- = -1 {0+}, this.topOfStack >= -1 {0+}> (U!Int,SJJ)
- (U!Int,DJU)
- (U!Int,DUU)
-
- (Bin,MJ)
- (Bin,MJ)
- (Bin,MJ)
- = -1 {0+}, orig(this.topOfStack) >= -1 {0+}> (U!Int,SJJ)
- = -1 {0+}, this.topOfStack >= -1 {0+}> (U!Int,SJJ)
- (U!Int,DUU)
- (U!Int,DJU)
- (U!Int,DJU)
- (U!Int,DUU)
diff --git a/tests/diff-tests/schedule2/schedule2-u.txt.goal b/tests/diff-tests/schedule2/schedule2-u.txt.goal
deleted file mode 100644
index ef71a1c0d9..0000000000
--- a/tests/diff-tests/schedule2/schedule2-u.txt.goal
+++ /dev/null
@@ -1,77 +0,0 @@
-getopt() returned 117
-
- <::next_pid >= 0 {0-}, ::next_pid >= 0 {1+}> (Una,SUJ)
-
- <::next_pid >= 0 {0-}, ::next_pid >= 0 {1+}> (Una,SUJ)
-
- = 0 {1+}, prio >= -1 {1+}> (Una,DJJ)
-
- (return is a pointer) {1+}> (Nul,MJ)
- (prio >= -1) {1+}> (Nul,MJ)
- (prio >= 0) {1+}> (Nul,MJ)
- (prio != 0) {0.9999+}> (Nul,MJ)
- = 0 {1+}, prio >= -1 {1+}> (Una,DJJ)
- (Una,DJJ)
-
- <*prio >= -1 {1+}, *prio >= -2 {0-}> (Una,DJU)
- <*command != 0 {1+}, null> (Una,JM)
-
- (*prio >= -1) {1+}> (Nul,MJ)
- (orig(*prio) >= -1) {1+}> (Nul,MJ)
- <(return == 1) ==> (*prio != 0) {1+}, null> (Nul,JM)
- (*command == 0) {1+}> (Bin,MJ)
- <(*prio == 0) ==> (orig(*prio) == 0) {1+}, null> (Bin,JM)
- <*prio >= -1 {1+}, *prio >= -2 {0-}> (Una,DJU)
- <*command != 0 {1+}, null> (Una,JM)
-
- <::next_pid >= 0 {0.4444-}, ::next_pid >= 0 {1+}> (Una,SUJ)
-
- <::next_pid >= 0 {0.4444-}, ::next_pid >= 0 {1+}> (Una,SUJ)
-
- = 0.0 {1+}, ratio >= -1.0 {0.0721-}> (Una,DJU)
-
- = 0.0 {1+}, ratio >= -1.0 {0.0721-}> (Una,DJU)
- (Una,DJJ)
-
- (Una,JM)
-
- = orig(::next_pid) {1+}> (Bin,MJ)
- <::next_pid - orig(::next_pid) - 1 == 0 {1+}, null> (Bin,JM)
- (orig(::next_pid) == 0) {1+}> (Bin,MJ)
- <::next_pid >= 1 {1+}, ::next_pid >= 0 {0.3333-}> (Una,DJU)
- (Una,DUJ)
- (Una,JM)
- (Una,DJJ)
-
- = 0 {1+}, prio >= -1 {1+}> (Una,DJJ)
-
- (return is a pointer) {1+}> (Nul,MJ)
- (prio >= -1) {1+}> (Nul,MJ)
- (prio >= 0) {1+}> (Nul,MJ)
- (prio != 0) {0.9999+}> (Nul,MJ)
- = 0 {1+}, prio >= -1 {1+}> (Una,DJJ)
- (Una,DJJ)
-
- = -1 {1+}, prio >= -2 {0-}> (Una,DJU)
- (Una,JM)
- (Una,JM)
-
- = -1 {1+}, prio >= -2 {0-}> (Una,DJU)
- (Una,JM)
- (Una,JM)
- (Una,JM)
- (Una,JM)
-
- (Una,SUJ)
-
- (Una,SUJ)
- (Una,DJJ)
-
- <::next_pid >= 0 {1+}, ::next_pid >= 0 {0.7779-}> (Una,SJU)
- (Una,SUJ)
- (Una,JM)
-
- <::next_pid >= 0 {1+}, ::next_pid >= 0 {0.7779-}> (Una,SJU)
- (Una,SUJ)
- (Una,JM)
- (Una,DJJ)