Java Doc for Recoder2KeY.java in  » Testing » KeY » de » uka » ilkd » key » java » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation 1.  6.0 JDK Core 2.  6.0 JDK Modules 3.  6.0 JDK Modules com.sun 4.  6.0 JDK Modules com.sun.java 5.  6.0 JDK Modules sun 6.  6.0 JDK Platform 7.  Ajax 8.  Apache Harmony Java SE 9.  Aspect oriented 10.  Authentication Authorization 11.  Blogger System 12.  Build 13.  Byte Code 14.  Cache 15.  Chart 16.  Chat 17.  Code Analyzer 18.  Collaboration 19.  Content Management System 20.  Database Client 21.  Database DBMS 22.  Database JDBC Connection Pool 23.  Database ORM 24.  Development 25.  EJB Server geronimo 26.  EJB Server GlassFish 27.  EJB Server JBoss 4.2.1 28.  EJB Server resin 3.1.5 29.  ERP CRM Financial 30.  ESB 31.  Forum 32.  GIS 33.  Graphic Library 34.  Groupware 35.  HTML Parser 36.  IDE 37.  IDE Eclipse 38.  IDE Netbeans 39.  Installer 40.  Internationalization Localization 41.  Inversion of Control 42.  Issue Tracking 43.  J2EE 44.  JBoss 45.  JMS 46.  JMX 47.  Library 48.  Mail Clients 49.  Net 50.  Parser 51.  PDF 52.  Portal 53.  Profiler 54.  Project Management 55.  Report 56.  RSS RDF 57.  Rule Engine 58.  Science 59.  Scripting 60.  Search Engine 61.  Security 62.  Sevlet Container 63.  Source Control 64.  Swing Library 65.  Template Engine 66.  Test Coverage 67.  Testing 68.  UML 69.  Web Crawler 70.  Web Framework 71.  Web Mail 72.  Web Server 73.  Web Services 74.  Web Services apache cxf 2.0.1 75.  Web Services AXIS2 76.  Wiki Engine 77.  Workflow Engines 78.  XML 79.  XML UI Java Java Tutorial Java Open Source Jar File Download Java Articles Java Products Java by API Photoshop Tutorials Maya Tutorials Flash Tutorials 3ds-Max Tutorials Illustrator Tutorials GIMP Tutorials C# / C Sharp C# / CSharp Tutorial C# / CSharp Open Source ASP.Net ASP.NET Tutorial JavaScript DHTML JavaScript Tutorial JavaScript Reference HTML / CSS HTML CSS Reference C / ANSI-C C Tutorial C++ C++ Tutorial Ruby PHP Python Python Tutorial Python Open Source SQL Server / T-SQL SQL Server / T-SQL Tutorial Oracle PL / SQL Oracle PL/SQL Tutorial PostgreSQL SQL / MySQL MySQL Tutorial VB.Net VB.Net Tutorial Flash / Flex / ActionScript VBA / Excel / Access / Word XML XML Tutorial Microsoft Office PowerPoint 2007 Tutorial Microsoft Office Excel 2007 Tutorial Microsoft Office Word 2007 Tutorial

Java Source Code / Java Documentation » Testing » KeY » de.uka.ilkd.key.java   Source Cross Reference   Class Diagram   Java Document (Java Doc)   java.lang.Object    de.uka.ilkd.key.java.Recoder2KeY All known Subclasses:   de.uka.ilkd.key.java.SchemaRecoder2KeY, Recoder2KeY public class Recoder2KeY implements JavaReader(Code) Field Summary protected  HashMap fieldSpecificationMapping      Hashmap from recoder.java.declaration.FieldSpecification to ProgramVariable; this is necessary to avoid cycles when converting initializers.  String fileName      static  String javaSrcDir      static  Logger logger      protected  HashMap methodsDeclaring      methodsDeclaring contains the recoder method declarations as keys that have been started to convert but are not yet finished. protected  KeYRecoderMapping rec2key      protected  KeYCrossReferenceServiceConfiguration servConf      protected  Services services      protected  HashMap type2KeYType      protected  TypeConverter typeConverter      Constructor Summary public   Recoder2KeY(KeYCrossReferenceServiceConfiguration servConf, KeYRecoderMapping rec2key, NamespaceSet nss, TypeConverter tc)      public   Recoder2KeY(Services services, NamespaceSet nss)      Method Summary public  void addProgramVariablesToClassContext(recoder.java.declaration.ClassDeclaration classContext, ListOfProgramVariable vars, recoder.service.CrossReferenceSourceInfo csi)      protected  Object callConvert(recoder.java.ProgramElement pe)      protected  ExtList collectChildren(recoder.java.NonTerminalProgramElement pe)      protected  ExtList collectComments(recoder.java.ProgramElement pe)      public  ProgramElement convert(recoder.java.JavaProgramElement pe)      the standard case. public  Instanceof convert(recoder.java.expression.operator.Instanceof rio)      public  PassiveExpression convert(de.uka.ilkd.key.java.recoderext.PassiveExpression pass)      public  ParenthesizedExpression convert(recoder.java.expression.ParenthesizedExpression x)      public  Comment convert(recoder.java.Comment rc)      public  NewArray convert(recoder.java.expression.operator.NewArray newArr)      public  CopyAssignment convert(recoder.java.expression.operator.CopyAssignment ass)      public  PostIncrement convert(recoder.java.expression.operator.PostIncrement postInc)      public  PreIncrement convert(recoder.java.expression.operator.PreIncrement preInc)      public  PostDecrement convert(recoder.java.expression.operator.PostDecrement postDec)      public  PreDecrement convert(recoder.java.expression.operator.PreDecrement preDec)      public  Minus convert(recoder.java.expression.operator.Minus minus)      public  Plus convert(recoder.java.expression.operator.Plus plus)      public  Times convert(recoder.java.expression.operator.Times times)      public  Divide convert(recoder.java.expression.operator.Divide div)      public  PlusAssignment convert(recoder.java.expression.operator.PlusAssignment plus)      public  MinusAssignment convert(recoder.java.expression.operator.MinusAssignment minus)      public  TimesAssignment convert(recoder.java.expression.operator.TimesAssignment times)      public  DivideAssignment convert(recoder.java.expression.operator.DivideAssignment div)      public  LessThan convert(recoder.java.expression.operator.LessThan op)      public  LessOrEquals convert(recoder.java.expression.operator.LessOrEquals op)      public  GreaterThan convert(recoder.java.expression.operator.GreaterThan op)      public  GreaterOrEquals convert(recoder.java.expression.operator.GreaterOrEquals op)      public  Equals convert(recoder.java.expression.operator.Equals op)      public  NotEquals convert(recoder.java.expression.operator.NotEquals op)      public  LogicalNot convert(recoder.java.expression.operator.LogicalNot op)      public  LogicalAnd convert(recoder.java.expression.operator.LogicalAnd op)      public  LogicalOr convert(recoder.java.expression.operator.LogicalOr op)      public  ArrayInitializer convert(recoder.java.expression.ArrayInitializer ai)      public  IntLiteral convert(recoder.java.expression.literal.IntLiteral intLit)      public  BooleanLiteral convert(recoder.java.expression.literal.BooleanLiteral booleanLit)      public  StringLiteral convert(recoder.java.expression.literal.StringLiteral stringLit)      public  DoubleLiteral convert(recoder.java.expression.literal.DoubleLiteral doubleLit)      public  FloatLiteral convert(recoder.java.expression.literal.FloatLiteral floatLit)      public  LongLiteral convert(recoder.java.expression.literal.LongLiteral longLit)      public  CharLiteral convert(recoder.java.expression.literal.CharLiteral charLit)      public  NullLiteral convert(recoder.java.expression.literal.NullLiteral nullLit)      public  EmptyStatement convert(recoder.java.statement.EmptyStatement eStmnt)      public  Throw convert(recoder.java.statement.Throw stmntThrow)      public  If convert(recoder.java.statement.If stmntIf)      public  Then convert(recoder.java.statement.Then stmntThen)      public  Else convert(recoder.java.statement.Else stmntElse)      public  ProgramElementName convert(recoder.java.Identifier id)      public  ProgramElementName convert(ImplicitIdentifier id)      public  StatementBlock convert(recoder.java.StatementBlock block)      public  SynchronizedBlock convert(recoder.java.statement.SynchronizedBlock block)      public  Return convert(recoder.java.statement.Return stmntReturn)      public  Try convert(recoder.java.statement.Try stmntTry)      public  Catch convert(recoder.java.statement.Catch stmntCatch)      public  Finally convert(recoder.java.statement.Finally stmntFinally)      public  MethodFrame convert(de.uka.ilkd.key.java.recoderext.MethodCallStatement rmcs)      public  MethodBodyStatement convert(de.uka.ilkd.key.java.recoderext.MethodBodyStatement rmbs)      public  CatchAllStatement convert(de.uka.ilkd.key.java.recoderext.CatchAllStatement cas)      public  Public convert(recoder.java.declaration.modifier.Public m)      public  Protected convert(recoder.java.declaration.modifier.Protected m)      public  Private convert(recoder.java.declaration.modifier.Private m)      public  Static convert(recoder.java.declaration.modifier.Static m)      public  Abstract convert(recoder.java.declaration.modifier.Abstract m)      public  Final convert(recoder.java.declaration.modifier.Final m)      public  Native convert(recoder.java.declaration.modifier.Native m)      public  Transient convert(recoder.java.declaration.modifier.Transient m)      public  Synchronized convert(recoder.java.declaration.modifier.Synchronized m)      public  CompilationUnit convert(recoder.java.CompilationUnit cu)      public  ClassInitializer convert(recoder.java.declaration.ClassInitializer ci)      public  PackageSpecification convert(recoder.java.PackageSpecification ps)      public  Throws convert(recoder.java.declaration.Throws t)      public  Extends convert(recoder.java.declaration.Extends e)      public  Implements convert(recoder.java.declaration.Implements e)      public  ClassDeclaration convert(recoder.java.declaration.ClassDeclaration td)      public  InterfaceDeclaration convert(recoder.java.declaration.InterfaceDeclaration td)      public  LocalVariableDeclaration convert(recoder.java.declaration.LocalVariableDeclaration lvd)      public  ParameterDeclaration convert(recoder.java.declaration.ParameterDeclaration pd)      public  FieldDeclaration convert(recoder.java.declaration.FieldDeclaration fd)      public  ProgramMethod convert(recoder.java.declaration.ConstructorDeclaration cd)      public  ProgramMethod convert(recoder.abstraction.DefaultConstructor dc)      public  TypeCast convert(recoder.java.expression.operator.TypeCast c)      public  ExecutionContext convert(de.uka.ilkd.key.java.recoderext.ExecutionContext ec)      public  ThisConstructorReference convert(recoder.java.reference.ThisConstructorReference tcr)      converts a recoder this constructor reference. public  SuperConstructorReference convert(recoder.java.reference.SuperConstructorReference scr)      converts a SpecialConstructorReference. public  ThisReference convert(recoder.java.reference.ThisReference tr)      public  SuperReference convert(recoder.java.reference.SuperReference sr)      public  VariableSpecification convert(recoder.java.declaration.VariableSpecification recoderVarSpec)      public  ProgramMethod convert(recoder.java.declaration.MethodDeclaration md)      public  FieldSpecification convert(recoder.java.declaration.FieldSpecification recoderVarSpec)      public  TypeReference convert(recoder.java.reference.TypeReference tr)      public  ProgramElement convert(recoder.java.reference.UncollatedReferenceQualifier urq)      public  ProgramVariable convert(recoder.java.reference.VariableReference vr)      converts a recoder variable reference. public  BinaryAnd convert(recoder.java.expression.operator.BinaryAnd b)      public  BinaryOr convert(recoder.java.expression.operator.BinaryOr b)      public  BinaryXOr convert(recoder.java.expression.operator.BinaryXOr b)      public  BinaryNot convert(recoder.java.expression.operator.BinaryNot b)      public  BinaryAndAssignment convert(recoder.java.expression.operator.BinaryAndAssignment b)      public  BinaryOrAssignment convert(recoder.java.expression.operator.BinaryOrAssignment b)      public  BinaryXOrAssignment convert(recoder.java.expression.operator.BinaryXOrAssignment b)      public  ShiftLeft convert(recoder.java.expression.operator.ShiftLeft b)      public  ShiftRight convert(recoder.java.expression.operator.ShiftRight b)      public  UnsignedShiftRight convert(recoder.java.expression.operator.UnsignedShiftRight b)      public  ShiftLeftAssignment convert(recoder.java.expression.operator.ShiftLeftAssignment b)      public  ShiftRightAssignment convert(recoder.java.expression.operator.ShiftRightAssignment b)      public  UnsignedShiftRightAssignment convert(recoder.java.expression.operator.UnsignedShiftRightAssignment b)      public  Negative convert(recoder.java.expression.operator.Negative b)      public  Positive convert(recoder.java.expression.operator.Positive b)      public  Modulo convert(recoder.java.expression.operator.Modulo b)      public  ModuloAssignment convert(recoder.java.expression.operator.ModuloAssignment b)      public  Conditional convert(recoder.java.expression.operator.Conditional b)      public  FieldReference convert(recoder.java.reference.ArrayLengthReference alr)      public  PackageReference convert(recoder.java.reference.PackageReference pr)      public  Expression convert(recoder.java.reference.FieldReference fr)      converts a recoder field reference. public  MethodReference convert(recoder.java.reference.MethodReference mr)      converts a recoder method reference. public  LabeledStatement convert(recoder.java.statement.LabeledStatement l)      public  For convert(recoder.java.statement.For f)      converts a For. public  While convert(recoder.java.statement.While w)      converts a While. public  Do convert(recoder.java.statement.Do d)      converts a Do. public  ArrayReference convert(recoder.java.reference.ArrayReference ar)      converts an ArrayReference. public  Break convert(recoder.java.statement.Break b)      public  Assert convert(recoder.java.statement.Assert a)      public  Case convert(recoder.java.statement.Case c)      converts a Case. public  New convert(recoder.java.expression.operator.New n)      converts a New. public  Import convert(recoder.java.Import im)      protected  Statement convertBody(recoder.java.statement.LoopStatement ls)      helper for convert(x) with x a LoopStatement. protected  Guard convertGuard(recoder.java.statement.LoopStatement ls)      helper for convert(x) with x a LoopStatement. protected  LoopInit convertLoopInitializers(recoder.java.statement.LoopStatement ls)      helper for convert(x) with x a LoopStatement. protected  ForUpdates convertUpdates(recoder.java.statement.LoopStatement ls)      helper for convert(x) with x a LoopStatement. public  ArrayDeclaration createArrayType(KeYJavaType baseType, KeYJavaType arrayType)      public  Context createContext(ListOfProgramVariable pvs)      public  Context createContext(ListOfProgramVariable vars, recoder.service.CrossReferenceSourceInfo csi)      public  Context createEmptyContext()      protected  recoder.java.declaration.MethodDeclaration embedBlock(recoder.java.StatementBlock block)      protected  recoder.java.declaration.ClassDeclaration embedMethod(recoder.java.declaration.MethodDeclaration mdecl, Context context)      protected  int[] extractPositionInfo(String errorMessage)      protected  ListOfField filterField(FieldDeclaration field)      protected  ProgramVariable find(String name, ListOfField fields)      protected  Class getKeYClass(Class recoderClass)      protected  Constructor getKeYClassConstructor(Class recoderClass)      protected  HashMap getKeYClassConstructorCache()      returns the hashmap of a concrete RecodeR class to the constructor of its corresponding KeY class. protected  String getKeYName(Class recoderClass)      protected  HashMap getMethodCache()      returns the hashmap of a concrete Java AST class to its corresponding convert method. protected  ProgramVariable getProgramVariableForFieldSpecification(recoder.java.declaration.FieldSpecification recoderVarSpec)      protected  recoder.java.declaration.VariableSpecification getRecoderVarSpec(recoder.java.reference.VariableReference vr)      public  KeYCrossReferenceServiceConfiguration getServiceConfiguration()      protected  void insertToMap(recoder.ModelElement r, ModelElement k)      public  void parseSpecialClasses()      protected  PositionInfo positionInfo(recoder.java.SourceElement se)      public  JavaBlock readBlock(String block, Context context)      public  JavaBlock readBlockWithEmptyContext(String block)      public  JavaBlock readBlockWithProgramVariables(Namespace varns, String s)      public  CompilationUnit readCompilationUnit(String cUnitString)      public  CompilationUnit[] readCompilationUnitsAsFiles(String[] cUnitStrings)      public  KeYRecoderMapping rec2key()      protected  recoder.java.StatementBlock recoderBlock(String block, Context context)      parses a given JavaBlock using the context to determine the right references and returns a statement block of recoder. protected  recoder.list.CompilationUnitMutableList recoderCompilationUnits(String[] cUnitStrings)      protected  recoder.list.CompilationUnitMutableList recoderCompilationUnitsAsFiles(String[] cUnitStrings)      protected  void reportError(String message, Throwable e)      protected  void setUpSort(Sort s)      Insert sorts into the namespace, add symbols that may have been defined by a sort to the function namespace (e.g. protected  void transformModel(recoder.list.CompilationUnitMutableList cUnits)      Field Detail fieldSpecificationMapping protected HashMap fieldSpecificationMapping(Code) Hashmap from recoder.java.declaration.FieldSpecification to ProgramVariable; this is necessary to avoid cycles when converting initializers. Access to this map is performed via the method getProgramVariableForFieldSpecification fileName String fileName(Code) javaSrcDir static String javaSrcDir(Code) logger static Logger logger(Code) methodsDeclaring protected HashMap methodsDeclaring(Code) methodsDeclaring contains the recoder method declarations as keys that have been started to convert but are not yet finished. The mapped value is the reference to the later completed ProgramMethod. rec2key protected KeYRecoderMapping rec2key(Code) servConf protected KeYCrossReferenceServiceConfiguration servConf(Code) services protected Services services(Code) type2KeYType protected HashMap type2KeYType(Code) mapping from recoder.abstraction.Type to KeYJavaType typeConverter protected TypeConverter typeConverter(Code) Constructor Detail Recoder2KeY public Recoder2KeY(KeYCrossReferenceServiceConfiguration servConf, KeYRecoderMapping rec2key, NamespaceSet nss, TypeConverter tc)(Code) Recoder2KeY public Recoder2KeY(Services services, NamespaceSet nss)(Code) Method Detail addProgramVariablesToClassContext public void addProgramVariablesToClassContext(recoder.java.declaration.ClassDeclaration classContext, ListOfProgramVariable vars, recoder.service.CrossReferenceSourceInfo csi)(Code) callConvert protected Object callConvert(recoder.java.ProgramElement pe)(Code) determines the right convert method using reflection Parameters:   pe - the recoder.java.JavaProgramElement to be converted the converted element collectChildren protected ExtList collectChildren(recoder.java.NonTerminalProgramElement pe)(Code) collects children and adds their converted KeY-counterpart to the list of childrem Parameters:   pe - the NonTerminalProgramElement that needs itschildren before being converted the list of children after conversion collectComments protected ExtList collectComments(recoder.java.ProgramElement pe)(Code) collects comments and adds their converted KeY-counterpart to the list of childrem Parameters:   pe - the ProgramElement that needs itscomments before being converted the list of comments after conversion convert public ProgramElement convert(recoder.java.JavaProgramElement pe)(Code) the standard case. Parameters:   pe - the recoder.java.ProgramElement to be converted the converted de.uka.ilkd.key.java.JavaProgramElement convert public Instanceof convert(recoder.java.expression.operator.Instanceof rio)(Code) convert public PassiveExpression convert(de.uka.ilkd.key.java.recoderext.PassiveExpression pass)(Code) converts the passive expression of the recoder extensions to the KeYDependance convert public ParenthesizedExpression convert(recoder.java.expression.ParenthesizedExpression x)(Code) converts the parenthesized expression to the KeYDependance convert public Comment convert(recoder.java.Comment rc)(Code) converts the recoder.java.Comment to the KeYDependance convert public NewArray convert(recoder.java.expression.operator.NewArray newArr)(Code) converts the recoder.java.expression.operator.NewArray node to the KeYDependance convert public CopyAssignment convert(recoder.java.expression.operator.CopyAssignment ass)(Code) converts the recoder.java.expression.operator.CopyAssignment node to the KeYDependance convert public PostIncrement convert(recoder.java.expression.operator.PostIncrement postInc)(Code) converts the recoder.java.expression.operator.PostIncrement node to the KeYDependance convert public PreIncrement convert(recoder.java.expression.operator.PreIncrement preInc)(Code) converts the recoder.java.expression.operator.PreIncrement node to the KeYDependance convert public PostDecrement convert(recoder.java.expression.operator.PostDecrement postDec)(Code) converts the recoder.java.expression.operator.PostDecrement node to the KeYDependance convert public PreDecrement convert(recoder.java.expression.operator.PreDecrement preDec)(Code) converts the recoder.java.expression.operator.PreDecrement node to the KeYDependance convert public Minus convert(recoder.java.expression.operator.Minus minus)(Code) converts the recoder.java.expression.operator.Minus node to the KeYDependance convert public Plus convert(recoder.java.expression.operator.Plus plus)(Code) converts the recoder.java.expression.operator.Plus node to the KeYDependance convert public Times convert(recoder.java.expression.operator.Times times)(Code) converts the recoder.java.expression.operator.Times node to the KeYDependance convert public Divide convert(recoder.java.expression.operator.Divide div)(Code) converts the recoder.java.expression.operator.Divide node to the KeYDependance convert public PlusAssignment convert(recoder.java.expression.operator.PlusAssignment plus)(Code) converts the recoder.java.expression.operator.PlusAssignment node to the KeYDependance convert public MinusAssignment convert(recoder.java.expression.operator.MinusAssignment minus)(Code) converts the recoder.java.expression.operator.MinusAssignment node to the KeYDependance convert public TimesAssignment convert(recoder.java.expression.operator.TimesAssignment times)(Code) converts the recoder.java.expression.operator.TimesAssignment node to the KeYDependance convert public DivideAssignment convert(recoder.java.expression.operator.DivideAssignment div)(Code) converts the recoder.java.expression.operator.DivideAssignment node to the KeYDependance convert public LessThan convert(recoder.java.expression.operator.LessThan op)(Code) converts the recoder.java.expression.operator.LessThan node to the KeYDependance convert public LessOrEquals convert(recoder.java.expression.operator.LessOrEquals op)(Code) converts the recoder.java.expression.operator.LessOrEquals node to the KeYDependance convert public GreaterThan convert(recoder.java.expression.operator.GreaterThan op)(Code) converts the recoder.java.expression.operator.GreaterThan node to the KeYDependance convert public GreaterOrEquals convert(recoder.java.expression.operator.GreaterOrEquals op)(Code) converts the recoder.java.expression.operator.GreaterOrEquals node to the KeYDependance convert public Equals convert(recoder.java.expression.operator.Equals op)(Code) converts the recoder.java.expression.operator.Equals node to the KeYDependance convert public NotEquals convert(recoder.java.expression.operator.NotEquals op)(Code) converts the recoder.java.expression.operator.NotEquals node to the KeYDependance convert public LogicalNot convert(recoder.java.expression.operator.LogicalNot op)(Code) converts the recoder.java.expression.operator.LogicalNot node to the KeYDependance convert public LogicalAnd convert(recoder.java.expression.operator.LogicalAnd op)(Code) converts the recoder.java.expression.operator.LogicalAnd node to the KeYDependance convert public LogicalOr convert(recoder.java.expression.operator.LogicalOr op)(Code) converts the recoder.java.expression.operator.LogicalOr node to the KeYDependance convert public ArrayInitializer convert(recoder.java.expression.ArrayInitializer ai)(Code) convert a recoder ArrayInitializer to a KeY array initializer convert public IntLiteral convert(recoder.java.expression.literal.IntLiteral intLit)(Code) convert a recoder IntLiteral to a KeY IntLiteral convert public BooleanLiteral convert(recoder.java.expression.literal.BooleanLiteral booleanLit)(Code) convert a recoder BooleanLiteral to a KeY BooleanLiteral convert public StringLiteral convert(recoder.java.expression.literal.StringLiteral stringLit)(Code) convert a recoder StringLiteral to a KeY StringLiteral convert public DoubleLiteral convert(recoder.java.expression.literal.DoubleLiteral doubleLit)(Code) convert a recoder DoubleLiteral to a KeY DoubleLiteral convert public FloatLiteral convert(recoder.java.expression.literal.FloatLiteral floatLit)(Code) convert a recoder FloatLiteral to a KeY FloatLiteral convert public LongLiteral convert(recoder.java.expression.literal.LongLiteral longLit)(Code) convert a recoder LongLiteral to a KeY LongLiteral convert public CharLiteral convert(recoder.java.expression.literal.CharLiteral charLit)(Code) convert a recoder CharLiteral to a KeY CharLiteral convert public NullLiteral convert(recoder.java.expression.literal.NullLiteral nullLit)(Code) convert a recoder NullLiteral to a KeY NullLiteral convert public EmptyStatement convert(recoder.java.statement.EmptyStatement eStmnt)(Code) convert a recoder EmptyStatement to a KeY EmptyStatement convert public Throw convert(recoder.java.statement.Throw stmntThrow)(Code) converts a recoder throw statement to a KeY throw statement convert public If convert(recoder.java.statement.If stmntIf)(Code) converts a recoder if statement to a KeY if statement convert public Then convert(recoder.java.statement.Then stmntThen)(Code) converts a recoder then statement to a KeY then statement convert public Else convert(recoder.java.statement.Else stmntElse)(Code) converts a recoder else statement to a KeY else statement convert public ProgramElementName convert(recoder.java.Identifier id)(Code) convert a recoder EmptyStatement to a KeY EmptyStatement convert public ProgramElementName convert(ImplicitIdentifier id)(Code) convert a recoder EmptyStatement to a KeY EmptyStatement convert public StatementBlock convert(recoder.java.StatementBlock block)(Code) convert a recoder StamentBlock to a KeY StatementBlock convert public SynchronizedBlock convert(recoder.java.statement.SynchronizedBlock block)(Code) convert a recoder StamentBlock to a KeY StatementBlock convert public Return convert(recoder.java.statement.Return stmntReturn)(Code) convert a recoder return statement to a KeY return statement convert public Try convert(recoder.java.statement.Try stmntTry)(Code) convert a recoder try statement to a KeY try statement convert public Catch convert(recoder.java.statement.Catch stmntCatch)(Code) convert a recoder catch statement to a KeY catch statement convert public Finally convert(recoder.java.statement.Finally stmntFinally)(Code) convert a recoder finally statement to a KeY finally statement convert public MethodFrame convert(de.uka.ilkd.key.java.recoderext.MethodCallStatement rmcs)(Code) convert a recoderext MethodFrameStatement to a KeY MethodFrameStatement convert public MethodBodyStatement convert(de.uka.ilkd.key.java.recoderext.MethodBodyStatement rmbs)(Code) convert a recoderext MethodBodyStatement to a KeY MethodBodyStatement convert public CatchAllStatement convert(de.uka.ilkd.key.java.recoderext.CatchAllStatement cas)(Code) convert public Public convert(recoder.java.declaration.modifier.Public m)(Code) converts the recoder public modifier to the KeY modifier convert public Protected convert(recoder.java.declaration.modifier.Protected m)(Code) converts the recoder protected modifier to the KeY modifier convert public Private convert(recoder.java.declaration.modifier.Private m)(Code) converts the recoder private modifier to the KeY modifier convert public Static convert(recoder.java.declaration.modifier.Static m)(Code) converts the recoder static modifier to the KeY modifier convert public Abstract convert(recoder.java.declaration.modifier.Abstract m)(Code) converts the recoder abstract modifier to the KeY modifier convert public Final convert(recoder.java.declaration.modifier.Final m)(Code) converts the recoder final modifier to the KeY modifier convert public Native convert(recoder.java.declaration.modifier.Native m)(Code) converts the recoder native modifier to the KeY modifier convert public Transient convert(recoder.java.declaration.modifier.Transient m)(Code) converts the recoder transient modifier to the KeY modifier convert public Synchronized convert(recoder.java.declaration.modifier.Synchronized m)(Code) converts the recoder synchronized modifier to the KeY modifier convert public CompilationUnit convert(recoder.java.CompilationUnit cu)(Code) convert public ClassInitializer convert(recoder.java.declaration.ClassInitializer ci)(Code) convert public PackageSpecification convert(recoder.java.PackageSpecification ps)(Code) convert public Throws convert(recoder.java.declaration.Throws t)(Code) convert public Extends convert(recoder.java.declaration.Extends e)(Code) convert public Implements convert(recoder.java.declaration.Implements e)(Code) convert public ClassDeclaration convert(recoder.java.declaration.ClassDeclaration td)(Code) convert public InterfaceDeclaration convert(recoder.java.declaration.InterfaceDeclaration td)(Code) convert public LocalVariableDeclaration convert(recoder.java.declaration.LocalVariableDeclaration lvd)(Code) converts a recoder LocalVariableDeclaration to a KeY LocalVariableDeclaration (especially the declaration type of its parent is determined and handed over) convert public ParameterDeclaration convert(recoder.java.declaration.ParameterDeclaration pd)(Code) converts a recoder ParameterDeclaration to a KeY ParameterDeclaration (especially the declaration type of its parent is determined and handed over) convert public FieldDeclaration convert(recoder.java.declaration.FieldDeclaration fd)(Code) convert a recoder FieldDeclaration to a KeY FieldDeclaration (especially the declaration type of its parent is determined and handed over) convert public ProgramMethod convert(recoder.java.declaration.ConstructorDeclaration cd)(Code) convert a recoder ConstructorDeclaration to a KeY ProgramMethod (especially the declaration type of its parent is determined and handed over) convert public ProgramMethod convert(recoder.abstraction.DefaultConstructor dc)(Code) convert a recoder DefaultConstructor to a KeY ProgramMethod (especially the declaration type of its parent is determined and handed over) convert public TypeCast convert(recoder.java.expression.operator.TypeCast c)(Code) convert public ExecutionContext convert(de.uka.ilkd.key.java.recoderext.ExecutionContext ec)(Code) converts an execution context convert public ThisConstructorReference convert(recoder.java.reference.ThisConstructorReference tcr)(Code) converts a recoder this constructor reference. the this reference in the KeY data structures convert public SuperConstructorReference convert(recoder.java.reference.SuperConstructorReference scr)(Code) converts a SpecialConstructorReference. Special handling because the initializing Expressions and the ReferencePrefix accessPath might not be disjunct. convert public ThisReference convert(recoder.java.reference.ThisReference tr)(Code) convert public SuperReference convert(recoder.java.reference.SuperReference sr)(Code) convert public VariableSpecification convert(recoder.java.declaration.VariableSpecification recoderVarSpec)(Code) convert a recoder VariableSpecification to a KeY VariableSpecification (checks dimension and hands it over and insert in hashmap) convert public ProgramMethod convert(recoder.java.declaration.MethodDeclaration md)(Code) convert a recoder MethodDeclaration to a KeY ProgramMethod (especially the declaration type of its parent is determined and handed over) convert public FieldSpecification convert(recoder.java.declaration.FieldSpecification recoderVarSpec)(Code) convert a recoder FieldSpecification to a KeY FieldSpecification (checks dimension and hands it over and insert in hash map) convert public TypeReference convert(recoder.java.reference.TypeReference tr)(Code) convert a recoder TypeReference to a KeY TypeReference (checks dimension and hands it over) convert public ProgramElement convert(recoder.java.reference.UncollatedReferenceQualifier urq)(Code) if an UncollatedReferenceQualifier appears throw a ConvertExceception because these qualifiers have to be resolved by running the CrossReferencer convert public ProgramVariable convert(recoder.java.reference.VariableReference vr)(Code) converts a recoder variable reference. A ProgramVariable is created replacing the variable reference. Parameters:   vr - the recoder variable reference. convert public BinaryAnd convert(recoder.java.expression.operator.BinaryAnd b)(Code) convert public BinaryOr convert(recoder.java.expression.operator.BinaryOr b)(Code) convert public BinaryXOr convert(recoder.java.expression.operator.BinaryXOr b)(Code) convert public BinaryNot convert(recoder.java.expression.operator.BinaryNot b)(Code) convert public BinaryAndAssignment convert(recoder.java.expression.operator.BinaryAndAssignment b)(Code) convert public BinaryOrAssignment convert(recoder.java.expression.operator.BinaryOrAssignment b)(Code) convert public BinaryXOrAssignment convert(recoder.java.expression.operator.BinaryXOrAssignment b)(Code) convert public ShiftLeft convert(recoder.java.expression.operator.ShiftLeft b)(Code) convert public ShiftRight convert(recoder.java.expression.operator.ShiftRight b)(Code) convert public UnsignedShiftRight convert(recoder.java.expression.operator.UnsignedShiftRight b)(Code) convert public ShiftLeftAssignment convert(recoder.java.expression.operator.ShiftLeftAssignment b)(Code) convert public ShiftRightAssignment convert(recoder.java.expression.operator.ShiftRightAssignment b)(Code) convert public UnsignedShiftRightAssignment convert(recoder.java.expression.operator.UnsignedShiftRightAssignment b)(Code) convert public Negative convert(recoder.java.expression.operator.Negative b)(Code) convert public Positive convert(recoder.java.expression.operator.Positive b)(Code) convert public Modulo convert(recoder.java.expression.operator.Modulo b)(Code) convert public ModuloAssignment convert(recoder.java.expression.operator.ModuloAssignment b)(Code) convert public Conditional convert(recoder.java.expression.operator.Conditional b)(Code) convert public FieldReference convert(recoder.java.reference.ArrayLengthReference alr)(Code) converts a recoder array length reference to a usual KeY field reference convert public PackageReference convert(recoder.java.reference.PackageReference pr)(Code) converts a recoder package reference to the KeY package reference Parameters:   pr - the recoder package reference reference. convert public Expression convert(recoder.java.reference.FieldReference fr)(Code) converts a recoder field reference. A ProgramVariable is created replacing the field reference. Parameters:   fr - the recoder field reference. convert public MethodReference convert(recoder.java.reference.MethodReference mr)(Code) converts a recoder method reference. A de.uka.ilkd.key.logic.op.ProgramMethod is created replacing the method reference. Parameters:   mr - the recoder method reference. the Method the KeY Dependance convert public LabeledStatement convert(recoder.java.statement.LabeledStatement l)(Code) convert public For convert(recoder.java.statement.For f)(Code) converts a For. Parameters:   f - the For of recoder the For of KeY convert public While convert(recoder.java.statement.While w)(Code) converts a While. Parameters:   w - the While of recoder the While of KeY convert public Do convert(recoder.java.statement.Do d)(Code) converts a Do. Parameters:   d - the Do of recoder the Do of KeY convert public ArrayReference convert(recoder.java.reference.ArrayReference ar)(Code) converts an ArrayReference. Special handling because the initializing Expressions and the ReferencePrefix accessPath might not be disjunct. convert public Break convert(recoder.java.statement.Break b)(Code) convert Breaks convert public Assert convert(recoder.java.statement.Assert a)(Code) convert Assert convert public Case convert(recoder.java.statement.Case c)(Code) converts a Case. Special handling because the initializing Expression and Statements might not be disjunct. convert public New convert(recoder.java.expression.operator.New n)(Code) converts a New. Special handling because the ReferencePrefix and the TypeReference might not be disjunct. convert public Import convert(recoder.java.Import im)(Code) convertBody protected Statement convertBody(recoder.java.statement.LoopStatement ls)(Code) helper for convert(x) with x a LoopStatement. Converts the body of x. convertGuard protected Guard convertGuard(recoder.java.statement.LoopStatement ls)(Code) helper for convert(x) with x a LoopStatement. Converts the guard of x. convertLoopInitializers protected LoopInit convertLoopInitializers(recoder.java.statement.LoopStatement ls)(Code) helper for convert(x) with x a LoopStatement. Converts the loop initializers of x. convertUpdates protected ForUpdates convertUpdates(recoder.java.statement.LoopStatement ls)(Code) helper for convert(x) with x a LoopStatement. Converts the updates of x. createArrayType public ArrayDeclaration createArrayType(KeYJavaType baseType, KeYJavaType arrayType)(Code) createContext public Context createContext(ListOfProgramVariable pvs)(Code) createContext public Context createContext(ListOfProgramVariable vars, recoder.service.CrossReferenceSourceInfo csi)(Code) createEmptyContext public Context createEmptyContext()(Code) creates an empty RECODER compilation unit the recoder.java.CompilationUnit embedBlock protected recoder.java.declaration.MethodDeclaration embedBlock(recoder.java.StatementBlock block)(Code) wraps a RECODER StatementBlock in a method Parameters:   block - the recoder.java.StatementBlock to wrap the enclosing recoder.java.MethodDeclaration embedMethod protected recoder.java.declaration.ClassDeclaration embedMethod(recoder.java.declaration.MethodDeclaration mdecl, Context context)(Code) wraps a RECODER MethodDeclaration in a class Parameters:   mdecl - the recoder.java.declaration.MethodDeclaration to wrap Parameters:   context - the recoder.java.declaration.ClassDeclarationwhere the method has to be embedded the enclosing recoder.java.declaration.ClassDeclaration extractPositionInfo protected int[] extractPositionInfo(String errorMessage)(Code) tries to parse recoders exception position information filterField protected ListOfField filterField(FieldDeclaration field)(Code) extracts all fields out of fielddeclaration Parameters:   field - the FieldDeclaration of which the fieldspecifications have to be extracted a ListOfField the includes all field specifications foundint the field declaration of the given list find protected ProgramVariable find(String name, ListOfField fields)(Code) retrieves a field with the given name out of the list Parameters:   name - a String with the name of the field to be looked for Parameters:   fields - the ListOfField where we have to look for the field the program variable of the given name or null if notfound getKeYClass protected Class getKeYClass(Class recoderClass)(Code) gets the KeY-Class related to the recoder one Parameters:   recoderClass - the original Class the related KeY Class getKeYClassConstructor protected Constructor getKeYClassConstructor(Class recoderClass)(Code) determines the right standard constructor of the KeYClass Parameters:   recoderClass - the Class of the recoder AST object the Constructor of the right KeY-Class getKeYClassConstructorCache protected HashMap getKeYClassConstructorCache()(Code) returns the hashmap of a concrete RecodeR class to the constructor of its corresponding KeY class. Speeds up reflection. Attention must be overwritten by subclasses! getKeYName protected String getKeYName(Class recoderClass)(Code) constructs the name of the corresponding KeYClass Parameters:   recoderClass - Class that is the original recoder String containing the KeY-Classname getMethodCache protected HashMap getMethodCache()(Code) returns the hashmap of a concrete Java AST class to its corresponding convert method. Speeds up reflection. Attention must be overwritten by subclasses! getProgramVariableForFieldSpecification protected ProgramVariable getProgramVariableForFieldSpecification(recoder.java.declaration.FieldSpecification recoderVarSpec)(Code) getRecoderVarSpec protected recoder.java.declaration.VariableSpecification getRecoderVarSpec(recoder.java.reference.VariableReference vr)(Code) getServiceConfiguration public KeYCrossReferenceServiceConfiguration getServiceConfiguration()(Code) insertToMap protected void insertToMap(recoder.ModelElement r, ModelElement k)(Code) parseSpecialClasses public void parseSpecialClasses()(Code) if not parsed yet the special classes are read in and converted positionInfo protected PositionInfo positionInfo(recoder.java.SourceElement se)(Code) readBlock public JavaBlock readBlock(String block, Context context)(Code) parses a given JavaBlock using the context to determine the right references Parameters:   block - a String describing a java block Parameters:   context - recoder.java.CompilationUnit in which the block has to be interprested the parsed and resolved JavaBlock readBlockWithEmptyContext public JavaBlock readBlockWithEmptyContext(String block)(Code) parses a given JavaBlock using the context to determine the right references using an empty context Parameters:   block - a String describing a java block the parsed and resolved JavaBlock readBlockWithProgramVariables public JavaBlock readBlockWithProgramVariables(Namespace varns, String s)(Code) readCompilationUnit public CompilationUnit readCompilationUnit(String cUnitString)(Code) readCompilationUnitsAsFiles public CompilationUnit[] readCompilationUnitsAsFiles(String[] cUnitStrings)(Code) rec2key public KeYRecoderMapping rec2key()(Code) recoderBlock protected recoder.java.StatementBlock recoderBlock(String block, Context context)(Code) parses a given JavaBlock using the context to determine the right references and returns a statement block of recoder. Parameters:   block - a String describing a java block Parameters:   context - recoder.java.CompilationUnit in which the block has to be interpreted the parsed and resolved recoder statement block recoderCompilationUnits protected recoder.list.CompilationUnitMutableList recoderCompilationUnits(String[] cUnitStrings)(Code) recoderCompilationUnitsAsFiles protected recoder.list.CompilationUnitMutableList recoderCompilationUnitsAsFiles(String[] cUnitStrings)(Code) reportError protected void reportError(String message, Throwable e)(Code) setUpSort protected void setUpSort(Sort s)(Code) Insert sorts into the namespace, add symbols that may have been defined by a sort to the function namespace (e.g. functions for collection sorts) transformModel protected void transformModel(recoder.list.CompilationUnitMutableList cUnits)(Code) Methods inherited from java.lang.Object protected Object clone() throws CloneNotSupportedException(Code)(Java Doc) public boolean equals(Object o)(Code)(Java Doc) protected void finalize() throws Throwable(Code)(Java Doc) final native public Class getClass()(Code)(Java Doc) public int hashCode()(Code)(Java Doc) final public void notify() throws IllegalMonitorStateException(Code)(Java Doc) final public void notifyAll() throws IllegalMonitorStateException(Code)(Java Doc) public String toString()(Code)(Java Doc) final public void wait() throws IllegalMonitorStateException, InterruptedException(Code)(Java Doc) final public void wait(long ms) throws IllegalMonitorStateException, InterruptedException(Code)(Java Doc) final public void wait(long ms, int ns) throws IllegalMonitorStateException, InterruptedException(Code)(Java Doc)