Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
mihai.herda
keyjoana
Commits
9fddb767
Commit
9fddb767
authored
Nov 22, 2019
by
Joachim Müssig
Browse files
clear up code, javadoc
parent
979b9413
Changes
2
Hide whitespace changes
Inline
Side-by-side
src/joanakey/javaforkeycreator/JavaForKeYCreator.java
View file @
9fddb767
...
...
@@ -39,7 +39,7 @@ import joanakey.violations.ViolationsDisproverSemantic;
/**
*
* @author holger
* @author holger
, joachim
*/
public
class
JavaForKeYCreator
{
...
...
@@ -271,7 +271,6 @@ public class JavaForKeYCreator {
for
(
SDGNode
currentEntry
:
entries
)
{
String
call
=
methodCall
.
toString
();
if
(
call
.
startsWith
(
currentEntry
.
getLabel
()))
{
//System.out.println("entry found: "+currentEntry);
result
.
add
(
currentEntry
);
}
}
...
...
@@ -406,10 +405,6 @@ public class JavaForKeYCreator {
SDGNode
formIn
=
formIns
.
iterator
().
next
();
// String mostGeneralContract = generateMostGeneralContract(
// formIns.iterator().next(), formOuts.iterator().next(), methodCall);
//TODO: may cause nullpointer exception, because of stateSaver ?
allInput
=
getAllInputIf
((
n
)
->
{
return
true
;
...
...
@@ -534,7 +529,6 @@ public class JavaForKeYCreator {
String
sinkDescr
=
generateSinkDescr
(
formalOutNode
,
methodCorresToSE
);
sinkDescr
=
replaceExceptionSinkSource
(
sinkDescr
);
//TODO: why just one formalInnode ? calculate for each formal in node ?
String
pointsToDecsr
=
PointsToGenerator
.
generatePreconditionFromPointsToSet
(
sdg
,
formalInNode
,
stateSaver
);
...
...
src/joanakey/javaforkeycreator/KeYFileCreator.java
View file @
9fddb767
...
...
@@ -27,9 +27,10 @@ public class KeYFileCreator {
/**
* Creates the Information flow Proof Obligation for KeY.
*
* @param javaFile
* @param method
* @param pathToSave path for the proof obligation file
* @param useLoopUnwinding boolean setting, true if KeY should use loop unwinding
* @param useMethodInlining boolean setting, true if KeY should use method inlining
*/
public
static
void
createKeYFileIF
(
StaticCGJavaMethod
method
,
String
pathToSave
,
boolean
useLoopUnwinding
,
boolean
useMethodInlining
)
throws
IOException
{
...
...
@@ -40,7 +41,7 @@ public class KeYFileCreator {
String
methodnameKey
=
getMethodnameKey
(
method
);
final
String
settingsStr
=
AutomationHelper
.
getSettings
(
useLoopUnwinding
,
useMethodInlining
);
//TODO: depinding on options !!
final
String
settingsStr
=
AutomationHelper
.
getSettings
(
useLoopUnwinding
,
useMethodInlining
);
final
String
javaSourceStr
=
"./"
;
final
String
proofObligationTemplateString
=
"#Proof Obligation Settings\n"
...
...
@@ -61,6 +62,15 @@ public class KeYFileCreator {
javaSourceStr
,
proofObligationString
,
proofObFile
);
}
/**
* Generate the functional proof oblicagtion for KeY
* @param method
* @param pathToSave path for the proof obligation file
* @param useLoopUnwinding boolean setting, true if KeY should use loop unwinding
* @param useMethodInlining boolean setting, true if KeY should use method inlining
* @param normalBehaviour boolean setting, true if the method specification contains should 'normal behaviour'
* @throws IOException
*/
public
static
void
createKeYFileFunctional
(
StaticCGJavaMethod
method
,
String
pathToSave
,
boolean
normalBehaviour
,
boolean
useLoopUnwinding
,
boolean
useMethodInlining
)
throws
IOException
{
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment