001 package daikon.inv.unary.string;
002
003 import daikon.*;
004 import daikon.inv.*;
005 import daikon.inv.unary.UnaryInvariant;
006 import utilMDE.*;
007
008 /**
009 * Abstract base class used to evaluate single strings.
010 **/
011
012 public abstract class SingleString
013 extends UnaryInvariant
014 {
015 // We are Serializable, so we specify a version to allow changes to
016 // method signatures without breaking serialization. If you add or
017 // remove fields, you should change this number to the current date.
018 static final long serialVersionUID = 20020122L;
019
020 protected SingleString(/*@Dependent(result=Nullable.class, when=Prototype.class)*/ PptSlice ppt) {
021 super(ppt);
022 // System.out.println("Created SingleString invariant " + this + " at " + ppt);
023 }
024
025 /** Returns whether or not the specified types are valid for unary string **/
026 public final boolean valid_types (VarInfo[] vis) {
027 return ((vis.length == 1) && vis[0].file_rep_type.isString());
028 }
029
030 public VarInfo var() {
031 return ppt.var_infos[0];
032 }
033
034 // Should never be called with modified == ValueTuple.MISSING_NONSENSICAL.
035 // Subclasses need not override this except in special cases;
036 // just implement @link{add_modified(String,int)}.
037 public InvariantStatus add(Object val, int mod_index, int count) {
038 assert ! falsified;
039 assert (mod_index >= 0) && (mod_index < 2);
040 String value = (String) val;
041 if (mod_index == 0) {
042 return add_unmodified(value, count);
043 } else {
044 return add_modified(value, count);
045 }
046 }
047
048 public InvariantStatus check(Object val, int mod_index, int count) {
049 assert ! falsified;
050 assert (mod_index >= 0) && (mod_index < 2);
051 String value = (String) val;
052 if (mod_index == 0) {
053 return check_unmodified(value, count);
054 } else {
055 return check_modified(value, count);
056 }
057 }
058
059
060 /**
061 * This method need not check for falsified;
062 * that is done by the caller.
063 **/
064 public abstract InvariantStatus add_modified(String value, int count);
065
066 /**
067 * By default, do nothing if the value hasn't been seen yet.
068 * Subclasses can override this.
069 **/
070 public InvariantStatus add_unmodified(String value, int count) {
071 return InvariantStatus.NO_CHANGE;
072 }
073
074 public abstract InvariantStatus check_modified(String value, int count);
075
076 public InvariantStatus check_unmodified(String value, int count) {
077 return InvariantStatus.NO_CHANGE;
078 }
079
080
081
082 }