001    package escjava.vcGeneration.sammy;
002    
003    import java.util.HashMap;
004    import java.io.*;
005    
006    import javafe.ast.Expr;
007    
008    import escjava.translate.GC;
009    import escjava.translate.InitialState;
010    import escjava.vcGeneration.*;
011    
012    public class SammyProver extends ProverType {
013        
014        public String labelRename(String label) {
015            return label;
016        }
017        
018        public TVisitor visitor(Writer out) throws IOException {
019            return null; //FIXME
020        }
021        
022        public void getProof(Writer out, String proofName, TNode term) throws IOException {
023            //FIXME
024        }
025        
026        public/*@ non_null @*/String getVariableInfo(VariableInfo caller) {
027    
028            if (caller.type != TNode._Type) {
029                if (caller.def == null)
030                    sammyRename(caller);
031    
032                return caller.def;
033            } else
034                return getTypeInfo(caller.type);
035        }
036    
037        // fixme, does nothing atm
038        /*! ensures sammy != null; !*/
039        private void sammyRename(VariableInfo caller) {
040            caller.def = caller.old;
041        }
042    
043        public String getTypeInfo(TypeInfo caller) {
044            if (caller.def == null)
045                sammyRename(caller);
046    
047            return caller.def;
048        }
049    
050        // fixme, does nothing atm
051        /*! ensures sammy != null; !*/
052        private void sammyRename(TypeInfo caller) {
053            caller.def = caller.old;
054        }
055    
056        public void init() {
057            // Predefined types
058    
059            TNode._Reference = TNode.addType("%Reference", "?");
060            TNode._Time = TNode.addType("%Time", "?");
061            TNode._Type = TNode.addType("%Type", "?");
062            TNode._boolean = TNode.addType("boolean", "?");
063            TNode._char = TNode.addType("char", "?");
064            TNode._DOUBLETYPE = TNode.addType("DOUBLETYPE", "?"); // fixme, is it JavaNumber or BaseType ?
065            TNode._double = TNode.addType("double", "?"); //fixme
066            TNode._Field = TNode.addType("%Field", "?"); // fixme there's a lot of different fields in the pvs logic, I need to capture that
067            TNode._INTTYPE = TNode.addType("INTTYPE", "?"); //fixme like DOUBLETYPE
068            TNode._integer = TNode.addType("integer", "?"); //fixme
069            TNode._float = TNode.addType("float", "?");
070            TNode._Path = TNode.addType("%Path", "?"); // used to modelize different ways
071            // of terminating a function
072            //_String = addType("String", "?"); fixme, does this type appears in original proof ?
073    
074            // Predefined variables name
075            // variables used by the old proof system and that we still need
076            TNode.addName("ecReturn", "%Path", "ecReturn");
077            TNode.addName("ecThrow", "%Path", "ecThrow");
078            TNode.addName("XRES", "%Reference", "XRES");        
079        }
080        
081        public Expr addTypeInfo(InitialState initState, Expr tree) {
082            tree = GC.implies(initState.getInitialState(), tree);
083            return tree;
084        }
085    
086        public TNode rewrite(TNode tree) {
087            // Intentionally do nothing!
088            return tree;
089        }
090    
091        public void generateDeclarations(/*@ non_null @*/ Writer s, HashMap variablesName) throws IOException {
092            // TODO Auto-generated method stub
093        }
094    }