001    package escjava.vcGeneration;
002    
003    import java.util.Iterator;
004    import java.util.Set;
005    import java.util.HashMap;
006    
007    import java.util.regex.Pattern;
008    import java.util.regex.Matcher;
009    
010    public class VariableInfo {
011    
012        /**
013         * README :
014         *
015         * This class is used to contain renaming of variables.
016         * For each variable a VariableInfo object is created.
017         *
018         * If you want to change the way variables are renamed, just change 
019         * {@link pvsRename} or {@link sammyRename} or add
020         * a function at the end.
021         */
022    
023        public/*@ non_null @*/String old = null;
024    
025        public TypeInfo type = null;
026    
027        public String def = null;
028    
029        private ProverType prover = null;
030    
031        public boolean typeSure = false;
032    
033        /**
034         * This last field wasn't planned intially. 
035         * But it is necessary when some variables have two types
036         * like for a class like :
037         *
038         * class A {
039    
040         int i1;
041    
042         }
043         *
044         * Then the variable i1 must have as first type "%Field"
045         * and "integer" two.
046         */
047        private TypeInfo secondType = null;
048    
049        /**
050         * When we call this constructor, we know the old type, so we give it.
051         */
052        public VariableInfo(/*@ non_null @*/String old, TypeInfo type) {
053            this.old = old;
054            this.type = type;
055        }
056    
057        /**
058         * Constructor for specifying the renaming of the variable.
059         */
060        public VariableInfo(/*@ non_null @*/String old, TypeInfo type, /*@ non_null @*/String def, /*@ non_null @*/ProverType prover) {
061            this.old = old;
062            this.type = type;
063            this.def = def;
064            this.prover = prover;
065        }
066    
067        public void setSecondType(/*@ non_null @*/TypeInfo type) {
068    
069            /*
070             * do some control
071             */
072            if (secondType != null) {
073                if (secondType != type)
074                    System.err
075                            .println("Inconsistancy, changing type of a field named "
076                                    + old
077                                    + " from "
078                                    + secondType.old
079                                    + " to "
080                                    + type.old);
081            } else
082                secondType = type;
083    
084        }
085    
086        public TypeInfo getSecondType() {
087            return secondType;
088        }
089    
090        public/*@ non_null @*/String getVariableInfo() {
091            return prover.getVariableInfo(this);
092        }
093        
094        public boolean equals(Object o){
095            if(o instanceof VariableInfo) {
096                    VariableInfo vi = (VariableInfo) o;
097                    return old.equals(vi.old);
098            }
099            return false;
100        }
101    }