* annotations or the beginning line of the next primitive
* @throws WrongAnnotationException
*/
- public static Primitive extractPrimitive(File file, int beginLineNum, ArrayList<String> annotations, IntObj curIdx)
+ public static Primitive extractPrimitive(File file, int beginLineNum,
+ ArrayList<String> annotations, IntObj curIdx)
throws WrongAnnotationException {
if (curIdx.getVal() == annotations.size()) // The current index points
// to the end
}
// Assert that we must have found one primitive
if (primitive == null) {
- WrongAnnotationException.err(file, curLineNum,
- "Something is wrong! We must have found one primitve here!\n");
+ WrongAnnotationException
+ .err(file, curLineNum,
+ "Something is wrong! We must have found one primitve here!\n");
}
// Process the current "primitive"
primitive.addLine(trimmedCode);
}
} else {
- WrongAnnotationException.err(file, curLineNum,
- "The state annotation should have correct primitive syntax (sub-annotations)");
+ WrongAnnotationException
+ .err(file, curLineNum,
+ "The state annotation should have correct primitive syntax (sub-annotations)");
}
// Deal with other normal line. E.g. y = 1;
if (primitive.contents.size() == 0) { // The content of the primitive is
// empty
- WrongAnnotationException.warning(file, curLineNum, "Primitive " + primitive.name + " is empty.");
+ WrongAnnotationException.warning(file, curLineNum, "Primitive "
+ + primitive.name + " is empty.");
}
return primitive;
}
// FIXME: We only consider the type is either a one-level pointer or a
// struct
String bareType = trimSpace(type.replace('*', ' '));
- return !bareType.equals("int") && !bareType.matches("unsigned\\s+int") && !bareType.equals("unsigned")
- && !bareType.equals("bool") && !bareType.equals("double") && !bareType.equals("float")
+ return !bareType.equals("int") && !bareType.matches("unsigned\\s+int")
+ && !bareType.equals("unsigned") && !bareType.equals("bool")
+ && !bareType.equals("double") && !bareType.equals("float")
&& !bareType.equals("void");
}
String bareType = trimSpace(type.replace('*', ' '));
return bareType;
}
+
+ /**
+ * <p>
+ * This function will automatically generate the printing statements for
+ * supported types when given a type and a name of the declaration.
+ * </p>
+ *
+ * @return The auto-generated state printing statements
+ */
+ public static Code generatePrintStatement(String type, String name) {
+ Code code = new Code();
+ // Primitive types
+ if (type.equals("int") || type.equals("unsigned")
+ || type.equals("unsigned int") || type.equals("int unsigned")
+ || type.equals("double") || type.equals("double")
+ || type.equals("bool")) {
+ // PRINT("\tx=%d\n", x);
+ code.addLine(SpecNaming.PRINT + "(\"\\t" + name + "=%d\\n\", "
+ + name + ");");
+ } else if (type.equals("int *") || type.equals("unsigned *")
+ || type.equals("unsigned int *")
+ || type.equals("int unsigned *") || type.equals("double *")
+ || type.equals("double *") || type.equals("bool *")) {
+ // Supported pointer types for primitive types
+ // PRINT("\t*x=%d\n", *x);
+ code.addLine(SpecNaming.PRINT + "(\"\\t*" + name + "=%d\\n\", *"
+ + name + ");");
+ } else if (type.equals("IntList") || type.equals("IntSet")
+ || type.equals("IntMap")) {
+ // Supported types
+ // PRINT("\tq: ");
+ // printContainer(&q);
+ // model_print("\n");
+ code.addLine(SpecNaming.PRINT + "(\"\\t" + name + ": \");");
+ code.addLine(SpecNaming.PrintContainer + "(&" + name + ");");
+ code.addLine(SpecNaming.PRINT + "(\"\\n\");");
+ } else if (type.equals("IntList *") || type.equals("IntSet *")
+ || type.equals("IntMap *")) {
+ // Supported pointer types
+ // PRINT("\tq: ");
+ // printContainer(q);
+ // model_print("\n");
+ code.addLine(SpecNaming.PRINT + "(\"\\t" + name + ": \");");
+ code.addLine(SpecNaming.PrintContainer + "(" + name + ");");
+ code.addLine(SpecNaming.PRINT + "(\"\\n\");");
+ } else if (type.equals("void")) {
+ // Just do nothing!
+ } else {
+ if (type.endsWith("*")) { // If it's an obvious pointer (with a STAR)
+ // Weak support pointer types (just print out the address)
+ // PRINT("\tmutex=%p\n", mutex);
+ code.addLine(SpecNaming.PRINT + "(\"\\t" + name + "=%p\\n\", "
+ + name + ");");
+ } else {
+ code.addLine("// We do not support auto-gen print-out for type: "
+ + type + ".");
+ }
+
+ }
+
+ return code;
+ }
+
}