|
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 |
||||||||||
PREV NEXT | FRAMES NO FRAMES |
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
SExp s. |
(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 SExp s. |
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 SList s 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 |
||||||||||
PREV NEXT | FRAMES NO FRAMES |