001// ***** This file is automatically generated from SequenceInitialFactory.java.jpp 002 003package daikon.derive.unary; 004 005import org.checkerframework.checker.nullness.qual.Nullable; 006import daikon.*; 007import java.util.logging.Logger; 008 009public final class SequenceInitialFactory extends UnaryDerivationFactory { 010 011 public static final Logger debug = 012 Logger.getLogger("daikon.derive.binary.SequenceInitialFactory"); 013 014 @Override 015 public UnaryDerivation @Nullable [] instantiate(VarInfo vi) { 016 // System.out.println("SequenceInitialFactory.instantiate(" + vi + ")"); 017 // return (UnaryDerivation)new SequenceFirst(vi); 018 019 if (!SequenceInitial.dkconfig_enabled) { 020 return null; 021 } 022 023 if (vi.rep_type != ProglangType.INT_ARRAY) { 024 return null; 025 } 026 027 // System.out.println("SequenceInitial.applicable(" + vi.name + ") = " 028 // + SequenceInitial.applicable(vi)); 029 030 if (!SequenceInitial.applicable(vi)) { 031 Global.tautological_suppressed_derived_variables += 4; 032 return null; 033 } 034 035 // by default, we use the indices 0, 1, -1, -2. 036 int lowerbound = -2; 037 int upperbound = 1; 038 039 boolean suppress_zero = false; 040 // We know that var.~ll~[0] == var and var.~ll~.field[0] == var.field. 041 if (vi.isClosure()) { 042 suppress_zero = true; 043 if ((lowerbound == 0) && (upperbound == 0)) { 044 Global.tautological_suppressed_derived_variables += 4; 045 } 046 return null; 047 } 048 049 int num_invs = upperbound - lowerbound + 1 - (suppress_zero ? 1 : 0); 050 assert num_invs > 0 051 : "No SequenceInitial invariants to instantiate; lowerbound=" 052 + lowerbound 053 + ", upperbound=" 054 + upperbound 055 + ", suppress_zero=" 056 + suppress_zero; 057 UnaryDerivation[] result = new UnaryDerivation[num_invs]; 058 int j = 0; 059 for (int i = lowerbound; i <= upperbound; i++) { 060 if (!((i == 0) && suppress_zero)) { 061 result[j] = new SequenceInitial(vi, i); 062 j++; 063 } 064 } 065 // No longer needed (I hope!). 066 // assert j == num_invs 067 // : "SequenceInitial(" + vi.name + "): " 068 // + "j=" + j + ", num_invs=" + num_invs 069 // + ",lowerbound=" + lowerbound 070 // + ", upperbound=" + upperbound 071 // + ", suppress_zero=" + suppress_zero; 072 073 Global.tautological_suppressed_derived_variables += 4 - num_invs; 074 075 return result; 076 } 077}