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}