001package daikon.inv;
002
003import daikon.Global;
004import daikon.VarInfo;
005import org.checkerframework.checker.signature.qual.ClassGetName;
006import org.checkerframework.dataflow.qual.SideEffectFree;
007
008/**
009 * A class used for holding a DiscardCode and a string that contains more detailed information about
010 * why an Invariant was discarded, as well as the classname and what would be returned by the
011 * Invariant's format() method.
012 */
013public final class DiscardInfo {
014
015  /**
016   * The DiscardCode describing this DiscardInfo. It should never be null; if an invariant isn't
017   * being discarded, use null as its DiscardInfo.
018   */
019  private DiscardCode discardCode;
020
021  /** The detailed reason for discard. */
022  private String discardString;
023
024  /**
025   * The String that would have resulted from calling format() on the Invariant being discarded.
026   * This does not have to be maintained if the Invariant isn't discarded.
027   */
028  private String discardFormat;
029
030  /** Invariant for which the DiscardInfo applies. */
031  public Invariant inv;
032
033  // Rarely used, so no need to precompute. -MDE
034  // /**
035  //  * The className of the Invariant being discarded
036  //  */
037  // private String className;
038
039  // public DiscardInfo(String className, String discardFormat, DiscardCode discardCode,
040  //                    String discardString) {
041  //   this.discardCode = discardCode;
042  //   this.discardString = discardString;
043  //   this.discardFormat = discardFormat;
044  //   this.className = className;
045  // }
046
047  public DiscardInfo(Invariant inv, DiscardCode discardCode, String discardString) {
048    assert inv.ppt != null;
049    // this(inv.getClass().getName(), inv.format(), discardCode, discardString);
050    this.discardCode = discardCode;
051    this.discardString = discardString;
052    this.discardFormat = inv.format();
053    // this.className = inv.getClass().getName();
054    this.inv = inv;
055    inv.log("%s", discardString);
056  }
057
058  public String discardFormat() {
059    return this.discardFormat;
060  }
061
062  public DiscardCode discardCode() {
063    return this.discardCode;
064  }
065
066  public String discardString() {
067    return this.discardString;
068  }
069
070  public @ClassGetName String className() {
071    return this.inv.getClass().getName();
072  }
073
074  @SideEffectFree
075  public String format() {
076    return (discardFormat + Global.lineSep + discardCode + Global.lineSep + discardString);
077  }
078
079  /** Adds the specified string as an additional reason. */
080  public void add_implied(String reason) {
081    discardString += " and " + reason;
082  }
083
084  /**
085   * Adds an equality string to the discardString for each variable in in vis which is different
086   * from the leader.
087   */
088  public void add_implied_vis(VarInfo[] vis) {
089    for (int i = 0; i < vis.length; i++) {
090      if (inv.ppt.var_infos[i] != vis[i]) {
091        discardString += " and " + inv.ppt.var_infos[i] + "==" + vis[i];
092      }
093    }
094  }
095}