edits
authorPeizhao Ou <peizhaoo@uci.edu>
Fri, 4 Mar 2016 01:41:49 +0000 (17:41 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Fri, 4 Mar 2016 01:41:49 +0000 (17:41 -0800)
src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java

index 4100a0a..fffeae5 100644 (file)
@@ -571,7 +571,11 @@ public class CodeGeneratorUtils {
                                        construct.preCondition.align(1);
                                        code.addLine(TabbedLine(ShortComment("Execute PreCondition")));
                                        code.addLines(construct.preCondition);
-
+                                       
+                                       // By default, we will return true for @PreCondition
+                                       code.addLine(TabbedLine(ShortComment("By default @PreCondition returns true")));
+                                       code.addLine(TabbedLine("return true;"));
+                                       
                                        code.addLine("}");
                                        code.addLine("");
 
@@ -596,6 +600,10 @@ public class CodeGeneratorUtils {
                                        code.addLine(TabbedLine(ShortComment("Execute PostCondition")));
                                        code.addLines(construct.postCondition);
 
+                                       // By default, we will return true for @PostCondition
+                                       code.addLine(TabbedLine(ShortComment("By default @PostCondition returns true")));
+                                       code.addLine(TabbedLine("return true;"));
+                                       
                                        code.addLine("}");
                                        code.addLine("");
                                }