| Method Summary |
|
| public void | addListener(DebuggerListener listener)
|
| public void | addTestCase(String file, String method, Node n)
|
| public ListOfProgramVariable | arrayOfExpression2ListOfProgVar(ArrayOfExpression aoe, int start)
|
| public static boolean | containsImplicitAttr(Term t)
|
| public SourceElement | determineFirstAndActiveStatement(Node node)
determines and returns the first and active statement if the applied
taclet worked on a modality. |
| public void | extractInput(Node n, PosInOccurrence pio)
|
| public void | extractPrecondition(Node node, PosInOccurrence pio)
|
| public void | fireDebuggerEvent(DebuggerEvent event)
|
| public SetOfTerm | getArrayIndex(PosInOccurrence pio2)
|
| public SetOfTerm | getArrayLocations(PosInOccurrence pio2)
|
| public BreakpointManager | getBpManager()
|
| public StateVisualization | getCurrentState()
|
| public ITNode | getCurrentTree()
|
| public ProgramMethod | getDebuggingMethod()
|
| public PosInOccurrence | getExecutionTerminatedNormal(Node n)
|
| public HashMap | getInputPV2term()
|
| public ListOfTerm | getLocations(PosInOccurrence pio2)
|
| public KeYMediator | getMediator()
|
| public MethodFrame | getMethodFrame(SourceElement context)
|
| public int | getMethodStackSize(Node n)
|
| public static String | getMethodString(MethodDeclaration md)
|
| public Node | getNodeForTC(String file, String method)
|
| public HashSet | getParam(MethodBodyStatement mbs)
|
| public Function | getPostPredicate()
|
| public Sequent | getPrecondition()
|
| public SourceElementId | getProgramCounter(JavaBlock jb)
|
| public SourceElementId | getProgramCounter(Node n)
|
| public SourceElementId | getProgramCounter(PosInOccurrence pio)
|
| public PosInOccurrence | getProgramPIO(Sequent s)
|
| public int | getRunLimit()
|
| public ProgramVariable | getSelfPV()
|
| public Term | getSelfTerm()
|
| public SetOfTerm | getSymbolicInputValues()
|
| public ListOfTerm | getSymbolicInputValuesAsList()
|
| public HashMap | getTerm2InputPV()
|
| public ClassType | getType()
|
| public HashMap | getValuesForLocation(HashSet locs, PosInOccurrence pio)
|
| public static VisualDebugger | getVisualDebugger()
|
| public void | initialize()
|
| public static boolean | isDebuggingMode()
|
| public boolean | isInitPhase()
|
| public boolean | isSepStatement(ProgramElement pe)
|
| public boolean | isStaticMethod()
|
| public JavaBlock | modalityTopLevel(PosInOccurrence pio)
|
| public String | prettyPrint(ListOfTerm l)
|
| public String | prettyPrint(ListOfTerm l, LinkedList objects, SymbolicObject thisObject)
|
| public String | prettyPrint(SetOfTerm l, LinkedList objects, SymbolicObject thisObject)
|
| public String | prettyPrint(Term l)
|
| public String | prettyPrint(Term l, LinkedList sos, SymbolicObject so)
|
| public static void | print(Object o)
|
| public static void | print(String s)
|
| public void | printTestCases()
|
| public ListOfTerm | removeImplicite(ListOfTerm list)
|
| public boolean | run()
|
| public boolean | run(ListOfGoal goals)
|
| public static void | setDebuggingMode(boolean mode)
|
| public void | setInitPhase(boolean initPhase)
|
| public void | setInputPV2term(HashMap inputPV2term)
|
| public void | setProofStrategy(Proof proof, boolean splittingAllowed, boolean inUpdateAndAssumes)
|
| public void | setSelfPV(ProgramVariable selfPV)
|
| public void | setStaticMethod(boolean staticMethod)
|
| public void | setTerm2InputPV(HashMap inputValues)
|
| public void | setType(ClassType type)
|
| public ListOfTerm | simplify(ListOfTerm terms)
|
| public boolean | stepInto()
|
| public boolean | stepInto(ListOfGoal goals)
|
| public boolean | stepInto(ListOfGoal goals, int steps)
|
| public void | stepOver()
|
| public void | stepOver(ListOfGoal goals)
|
| public boolean | stepToFirstSep()
|
| public synchronized void | visualize(ITNode n)
|
