ESC/Java2
© 2003,2004,2005 David Cok and Joseph Kiniry
© 2005 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

Uses of Class
escjava.prover.SList

Packages that use SList
escjava.prover   
escjava.translate   
 

Uses of SList in escjava.prover
 

Subclasses of SList in escjava.prover
(package private)  class SNil
          The single SNil instance represents the empty list of SExps.
(package private)  class SPair
          A SPair is a pair of a SExp and a SList; together with the SNil class, it is used to implement lists of SExps.
 

Fields in escjava.prover declared as SList
 SList SPair.tail
          The tail of our list; this field should not be modified by clients and should be non-null.
(package private)  SList SimplifyResult.labels
           
(package private)  SList SimplifyResult.context
           
 

Methods in escjava.prover that return SList
 SList SubProcess.readSList()
           
 SList SubProcess.readSLists()
          Read a (possibly empty) series of SLists from this subprocess.
 SList SubProcess.readSExps(char stop)
           
static SList SList.make()
           
static SList SList.make(java.lang.Object a1)
           
static SList SList.make(java.lang.Object a1, java.lang.Object a2)
           
static SList SList.make(java.lang.Object a1, java.lang.Object a2, java.lang.Object a3)
           
static SList SList.make(java.lang.Object a1, java.lang.Object a2, java.lang.Object a3, java.lang.Object a4)
           
static SList SList.make(java.lang.Object a1, java.lang.Object a2, java.lang.Object a3, java.lang.Object a4, java.lang.Object a5)
           
static SList SList.make(java.lang.Object a1, java.lang.Object a2, java.lang.Object a3, java.lang.Object a4, java.lang.Object a5, java.lang.Object a6)
           
static SList SList.make(java.lang.Object a1, java.lang.Object a2, java.lang.Object a3, java.lang.Object a4, java.lang.Object a5, java.lang.Object a6, java.lang.Object a7)
           
static SList SList.make(java.lang.Object a1, java.lang.Object a2, java.lang.Object a3, java.lang.Object a4, java.lang.Object a5, java.lang.Object a6, java.lang.Object a7, java.lang.Object a8)
           
static SList SList.fromArray(SExp[] a)
           
 SList SList.getList()
           
 SList SList.append(SList x)
           
static SList SList.reverseD(SList l)
          Destructive list reversal
 SList SList.addFront(SExp x)
           
 SList SList.addEnd(SExp x)
           
 SList SimplifyResult.getLabels()
           
 SList SimplifyResult.getContext()
           
 SList SExp.getList()
          If we represent a list, return it as an SList; otherwise, throw SExpTypeError.
 

Methods in escjava.prover with parameters of type SList
 SList SList.append(SList x)
           
static SList SList.reverseD(SList l)
          Destructive list reversal
 

Constructors in escjava.prover with parameters of type SList
TriggerlessQuantWarning(SList labels, SList context, SExp e0, int n, SExp e1)
           
SPair(SExp head, SList tail)
          Return a new list with given head and tail.
SimplifyResult(int kind, SList labels, SList context)
           
 

Uses of SList in escjava.translate
 

Methods in escjava.translate that return SList
private static SList ErrorMsg.pruneCC(SList cc)
          Prune out s-expressions from the counterexample context that are almost certainly irrelevant.
 

Methods in escjava.translate with parameters of type SList
(package private) static java.lang.String Suggestion.generate(int warningTag, java.lang.Object auxInfo, RoutineDecl rd, Set directTargets, SList cc, int locDecl)
           
private static java.lang.String Suggestion.gInvariant(Expr E, RoutineDecl rd, SList cc, int locDecl)
           
private static boolean Suggestion.brokenObjIsMadeUp(SList cc)
           
static void ErrorMsg.print(java.lang.String name, SList labelList, SList counterexampleContext, RoutineDecl rd, Set directTargets, java.io.PrintStream out)
          Prints an error message for proof obligation name, where labelList and counterexampleContext are labels and counterexample from Simplify.
private static void ErrorMsg.printErrorMessage(java.lang.String s, SList counterexampleContext, RoutineDecl rd, Set directTargets, java.io.PrintStream out, boolean assocOnly)
          Parses s and prints a nice error message to out.
private static void ErrorMsg.displayInvariantContext(SList counterexampleContext, java.io.PrintStream out)
           
private static SList ErrorMsg.pruneCC(SList cc)
          Prune out s-expressions from the counterexample context that are almost certainly irrelevant.
 


ESC/Java2
© 2003,2004,2005 David Cok and Joseph Kiniry
© 2005 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

The ESC/Java2 Project Homepage