b) Interface construct
@Begin
- @Interface: ...
+ @Interface_decl: ...
@Commit_point_set:
IDENTIFIER | IDENTIFIER ...
@Condition: ... (Optional)
@Begin
@Interface_define: <Interface_Name>
@End
+
+ g) Interface declare & define construct
+ @Begin
+ @Interface_decl_define: <Interface_Name>
+ @Commit_point_set:
+ IDENTIFIER | IDENTIFIER ...
+ @Condition: ... (Optional)
+ @HB_Condition:
+ IDENTIFIER :: <C_CPP_Condition>
+ @HB_Condition: ...
+ @ID: ... (Optional, use default ID)
+ @Check: (Optional)
+ ...
+ @Action: (Optional)
+ ...
+ @Post_action: (Optional)
+ @Post_check: (Optional)
+ @End
+
*/
FunctionHeader FuncDecl() :
{
+ ArrayList<VariableDeclaration> templateList;
String ret;
QualifiedName funcName;
ArrayList<VariableDeclaration> args;
}
{
+aa
(<STATIC> | <INLINE>)*
ret = Type()
funcName = ParseQualifiedName()
}
}
-ArrayList<String> TemplateParamList() :
+ArrayList<VariableDeclaration> TemplateParamList() :
{
- ArrayList<String> params;
- String str;
+ ArrayList<VariableDeclaration> params;
+ String type;
+ String name;
}
{
{
- params = new ArrayList<String>();
+ params = new ArrayList<VariableDeclaration>();
}
<TEMPLATE>
"<"
- (str = <IDENTIFIER>.image
- str = <IDENTIFIER>.image {params.add(str);})
+ (type = <IDENTIFIER>.image
+ name = <IDENTIFIER>.image
+ {
+ params.add(new VariableDeclaration(type, name));
+ }
+ )
- ("," str = <IDENTIFIER>.image
- str = <IDENTIFIER>.image {params.add(str);})*
+ ("," type = <IDENTIFIER>.image
+ name = <IDENTIFIER>.image
+ {
+ params.add(new VariableDeclaration(type, name));
+ }
+ )*
">"
{
//System.out.println(params);
String interfaceName = construct.name;
// Generate necessary header file (might be redundant but never mind)
newCode.add(INCLUDE(HEADER_STDLIB));
- newCode.add(INCLUDE(HEADER_THREADS));
newCode.add(INCLUDE(HEADER_CDSANNOTATE));
newCode.add(INCLUDE(HEADER_SPECANNOTATION));
newCode.add(INCLUDE(HEADER_SPEC_LIB));
return newCode;
}
+ // Rename the interface depending on if it's declaration or definition
public static void renameInterface(SemanticsChecker semantics,
Construct construct) {
FunctionHeader header = getFunctionHeader(semantics, construct);
public static String HOME_DIRECTORY = System.getProperty("user.dir");
public static String GENERATED_FILE_DIR = HOME_DIRECTORY + "/" + "output";
public static String MODEL_CHECKER_HOME_DIR = System
- .getProperty("user.home") + "/model-checker-priv";
+ .getProperty("user.home") + "/test/model-checker-priv";
public static String MODEL_CHECKER_TEST_DIR = MODEL_CHECKER_HOME_DIR + "/test";
+
+ public static String MS_QUEUE = MODEL_CHECKER_TEST_DIR = MODEL_CHECKER_TEST_DIR + "/ms-queue";
+ public static String LINUXRWLOCKS = MODEL_CHECKER_TEST_DIR = MODEL_CHECKER_TEST_DIR + "/linuxrwlocks";
+ public static String CLIFFC_HASHTABLE = MODEL_CHECKER_TEST_DIR = MODEL_CHECKER_TEST_DIR + "/cliffc-hashtable";
+
}
import java.util.ArrayList;
public class FunctionHeader {
+ public final ArrayList<VariableDeclaration> templateList;
+
public final String returnType;
public final QualifiedName qualifiedName;
public final ArrayList<VariableDeclaration> args;
- public FunctionHeader(String returnType, QualifiedName qualifiedName,
+ public FunctionHeader(ArrayList<VariableDeclaration> templateList, String returnType, QualifiedName qualifiedName,
ArrayList<VariableDeclaration> args) {
+ this.templateList = templateList;
this.returnType = returnType;
this.qualifiedName = qualifiedName;
this.args = args;
public FunctionHeader getRenamedHeader(String prefix) {
String newFullName = qualifiedName.qualifiedName + prefix + "_"
+ qualifiedName.bareName;
- FunctionHeader newHeader = new FunctionHeader(returnType,
+ FunctionHeader newHeader = new FunctionHeader(templateList, returnType,
new QualifiedName(newFullName), args);
return newHeader;
}
public class InterfaceDefineConstruct extends Construct {
public final String name;
- private String funcDecl;
public InterfaceDefineConstruct(File file, int beginLineNum, String name) {
super(file, beginLineNum);