001package daikon.derive.unary;
002
003import daikon.ProglangType;
004import daikon.ValueTuple;
005import daikon.VarInfo;
006import daikon.derive.Derivation;
007import daikon.derive.ValueAndModified;
008import org.checkerframework.dataflow.qual.Pure;
009import org.checkerframework.dataflow.qual.SideEffectFree;
010import org.plumelib.util.Intern;
011
012/** Length of String variables. */
013public final class StringLength extends UnaryDerivation {
014  static final long serialVersionUID = 20061016L;
015
016  /** Boolean. True iff StringLength derived variables should be generated. */
017  public static boolean dkconfig_enabled = false;
018
019  public StringLength(VarInfo vi) {
020    super(vi);
021  }
022
023  public static boolean applicable(VarInfo vi) {
024    assert vi.rep_type.isString();
025    return true;
026  }
027
028  @Override
029  public ValueAndModified computeValueAndModifiedImpl(ValueTuple vt) {
030    int source_mod = base.getModified(vt);
031    if (source_mod == ValueTuple.MISSING_NONSENSICAL) {
032      return ValueAndModified.MISSING_NONSENSICAL;
033    }
034    Object val = base.getValue(vt);
035    if (val == null) {
036      return ValueAndModified.MISSING_NONSENSICAL;
037    }
038
039    int len = ((String) val).length();
040    return new ValueAndModified(Intern.internedLong(len), source_mod);
041  }
042
043  @Override
044  protected VarInfo makeVarInfo() {
045    return VarInfo.make_scalar_str_func("length", ProglangType.INT, base);
046  }
047
048  @Pure
049  @Override
050  public boolean isSameFormula(Derivation other) {
051    return (other instanceof StringLength);
052  }
053
054  @Override
055  @SideEffectFree
056  public String csharp_name(String index) {
057    return String.format("%s.Length", base.csharp_name());
058  }
059
060  @Override
061  @SideEffectFree
062  public String esc_name(String index) {
063    return String.format("%s.length()", base.esc_name());
064  }
065
066  @Override
067  public String jml_name(String index) {
068    return String.format("%s.length()", base.jml_name());
069  }
070
071  @Override
072  @SideEffectFree
073  public String simplify_name() {
074    return String.format("(stringLength %s)", base.simplify_name());
075  }
076}