public class HelperClassForTests
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
static java.io.File |
DUMMY_KEY_FILE |
static java.io.File |
TESTCASE_DIRECTORY |
Constructor and Description |
---|
HelperClassForTests() |
Modifier and Type | Method and Description |
---|---|
static KeYEnvironment<DefaultUserInterfaceControl> |
createKeYEnvironment() |
static Services |
createServices() |
static Services |
createServices(java.io.File keyFile) |
Term |
extractProblemTerm(Proof p) |
static boolean |
isOneStepSimplificationEnabled(Proof proof)
Checks if one step simplification is enabled in the given
Proof . |
ProofAggregate |
parse(java.io.File file) |
ProofAggregate |
parse(java.io.File file,
Profile profile) |
ProofAggregate |
parseThrowException(java.io.File file) |
ProofAggregate |
parseThrowException(java.io.File file,
Profile profile) |
static void |
restoreTacletOptions(java.util.HashMap<java.lang.String,java.lang.String> options)
Restores the given taclet options.
|
static IProgramMethod |
searchProgramMethod(Services services,
java.lang.String containerTypeName,
java.lang.String methodFullName)
Searches a
IProgramMethod in the given Services . |
static java.util.HashMap<java.lang.String,java.lang.String> |
setDefaultTacletOptions()
Ensures that the default taclet options are defined.
|
static java.util.HashMap<java.lang.String,java.lang.String> |
setDefaultTacletOptions(java.io.File baseDir,
java.lang.String javaPathInBaseDir)
Ensures that the default taclet options are defined.
|
static java.util.HashMap<java.lang.String,java.lang.String> |
setDefaultTacletOptionsForTarget(java.io.File javaFile,
java.lang.String containerTypeName,
java.lang.String targetName)
Ensures that the default taclet options are defined.
|
static void |
setOneStepSimplificationEnabled(Proof proof,
boolean enabled)
Defines if one step simplification is enabled in general and within the
Proof . |
public static final java.io.File TESTCASE_DIRECTORY
public static final java.io.File DUMMY_KEY_FILE
public ProofAggregate parse(java.io.File file)
public ProofAggregate parse(java.io.File file, Profile profile)
public ProofAggregate parseThrowException(java.io.File file) throws ProofInputException
ProofInputException
public ProofAggregate parseThrowException(java.io.File file, Profile profile) throws ProofInputException
ProofInputException
public static boolean isOneStepSimplificationEnabled(Proof proof)
Proof
.proof
- The Proof
to read from or null
to return the general settings value.true
one step simplification is enabled, false
if disabled.public static void setOneStepSimplificationEnabled(Proof proof, boolean enabled)
Proof
.proof
- The optional Proof
.enabled
- true
use one step simplification, false
do not
use one step simplification.public static java.util.HashMap<java.lang.String,java.lang.String> setDefaultTacletOptions(java.io.File baseDir, java.lang.String javaPathInBaseDir) throws ProblemLoaderException, ProofInputException
baseDir
- The base directory which contains the java file.javaPathInBaseDir
- The path in the base directory to the java file.ProblemLoaderException
- Occurred Exception.ProofInputException
- Occurred Exception.public static java.util.HashMap<java.lang.String,java.lang.String> setDefaultTacletOptionsForTarget(java.io.File javaFile, java.lang.String containerTypeName, java.lang.String targetName) throws ProblemLoaderException, ProofInputException
javaFile
- The java file to load.containerTypeName
- The type name which provides the target.targetName
- The target to proof.ProblemLoaderException
- Occurred Exception.ProofInputException
- Occurred Exception.public static java.util.HashMap<java.lang.String,java.lang.String> setDefaultTacletOptions()
public static void restoreTacletOptions(java.util.HashMap<java.lang.String,java.lang.String> options)
options
- The taclet options to restore.public static IProgramMethod searchProgramMethod(Services services, java.lang.String containerTypeName, java.lang.String methodFullName)
IProgramMethod
in the given Services
.services
- The Services
to search in.containerTypeName
- The name of the type which contains the method.methodFullName
- The method name to search.IProgramMethod
in the type.public static Services createServices(java.io.File keyFile)
public static Services createServices()
public static KeYEnvironment<DefaultUserInterfaceControl> createKeYEnvironment() throws ProblemLoaderException
ProblemLoaderException
Copyright © 2003-2019 The KeY-Project.