src/edu/uci/eecs/specExtraction/DefineConstruct.java

   1 package edu.uci.eecs.specExtraction;
   2
   3 import java.io.File;
   4 import java.util.ArrayList;
   5 import java.util.HashMap;
   6 import java.util.regex.Matcher;
   7 import java.util.regex.Pattern;
   8
   9 import edu.uci.eecs.specExtraction.SpecUtils.IntObj;
  10 import edu.uci.eecs.specExtraction.SpecUtils.Primitive;
  11 import edu.uci.eecs.utilParser.ParseException;
  12 import edu.uci.eecs.utilParser.UtilParser;
  13
  14 /**
  15  * <p>
  16  * This class is a subclass of Construct. It represents user-defined code that
  17  * we allow in the header file. Note that the code here basically are the same
  18  * as writing code right in place. We require function declaration/definition to
  19  * be inline. Users should be responsible for the correctness of their code.
  20  * </p>
  21  *
  22  * @author Peizhao Ou
  23  *
  24  */
  25 public class DefineConstruct extends Construct {
  26         public final Code code;
  27
  28         // The ending line number of the specification annotation construct
  29         public final int endLineNum;
  30
  31         public DefineConstruct(File file, int beginLineNum, int endLineNum,
  32                         ArrayList<String> annotations) throws WrongAnnotationException {
  33                 super(file, beginLineNum);
  34                 code = new Code();
  35                 this.endLineNum = endLineNum;
  36                 Primitive define = SpecUtils.extractPrimitive(file, beginLineNum,
  37                                 annotations, new IntObj(0));
  38                 code.addLines(define.contents);
  39         }
  40
  41         public String toString() {
  42                 StringBuilder sb = new StringBuilder();
  43                 sb.append(super.toString() + "\n");
  44                 sb.append("@Define:\n");
  45                 if (!code.isEmpty()) {
  46                         sb.append(code);
  47                         sb.append("\n");
  48                 }
  49                 return sb.toString();
  50         }
  51 }