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
fb230341
Commit
fb230341
authored
Nov 20, 2019
by
Joachim Müssig
Browse files
code clear up, javadoc
parent
434d47af
Changes
4
Hide whitespace changes
Inline
Side-by-side
src/gui/DisproHandler.java
View file @
fb230341
...
@@ -6,7 +6,6 @@
...
@@ -6,7 +6,6 @@
package
gui
;
package
gui
;
import
java.io.IOException
;
import
java.io.IOException
;
import
java.util.ArrayList
;
import
java.util.Collection
;
import
java.util.Collection
;
import
java.util.HashMap
;
import
java.util.HashMap
;
import
java.util.HashSet
;
import
java.util.HashSet
;
...
@@ -15,7 +14,6 @@ import java.util.Map;
...
@@ -15,7 +14,6 @@ import java.util.Map;
import
java.util.Set
;
import
java.util.Set
;
import
org.fxmisc.richtext.CodeArea
;
import
org.fxmisc.richtext.CodeArea
;
import
org.jgrapht.ext.JGraphModelAdapter.CellFactory
;
import
edu.kit.joana.ifc.sdg.core.SecurityNode
;
import
edu.kit.joana.ifc.sdg.core.SecurityNode
;
import
edu.kit.joana.ifc.sdg.core.violations.ClassifiedViolation
;
import
edu.kit.joana.ifc.sdg.core.violations.ClassifiedViolation
;
...
@@ -37,7 +35,6 @@ import javafx.scene.layout.AnchorPane;
...
@@ -37,7 +35,6 @@ import javafx.scene.layout.AnchorPane;
import
javafx.scene.paint.Color
;
import
javafx.scene.paint.Color
;
import
javafx.util.Callback
;
import
javafx.util.Callback
;
import
joanakey.JoanaAndKeYCheckData
;
import
joanakey.JoanaAndKeYCheckData
;
import
joanakey.customlistener.SummaryEdgeAndMethodToCorresData
;
import
joanakey.customlistener.ViolationsWrapperListener
;
import
joanakey.customlistener.ViolationsWrapperListener
;
import
joanakey.errorhandling.ErrorLogger
;
import
joanakey.errorhandling.ErrorLogger
;
import
joanakey.persistence.DisprovingProject
;
import
joanakey.persistence.DisprovingProject
;
...
@@ -49,7 +46,7 @@ import keyjoana.settings.SettingsObserver;
...
@@ -49,7 +46,7 @@ import keyjoana.settings.SettingsObserver;
/**
/**
*
*
* @author holger
* @author holger
, joachim
*/
*/
public
class
DisproHandler
implements
ViolationsWrapperListener
,
SettingsObserver
{
public
class
DisproHandler
implements
ViolationsWrapperListener
,
SettingsObserver
{
...
@@ -91,7 +88,6 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
...
@@ -91,7 +88,6 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
private
AnchorPane
anchorPaneKeyContract
;
private
AnchorPane
anchorPaneKeyContract
;
private
Map
<
Integer
,
ViolationChop
>
itemIndexToViolation
=
new
HashMap
<>();
private
Map
<
Integer
,
ViolationChop
>
itemIndexToViolation
=
new
HashMap
<>();
private
Map
<
ViolationChop
,
Boolean
>
violationChecked
=
new
HashMap
<>();
private
Map
<
Integer
,
SDGEdge
>
itemIndexToSummaryEdge
=
new
HashMap
<>();
private
Map
<
Integer
,
SDGEdge
>
itemIndexToSummaryEdge
=
new
HashMap
<>();
private
HashMap
<
Integer
,
SDGNodeTuple
>
currentIndexToNodeTuple
=
new
HashMap
<>();
private
HashMap
<
Integer
,
SDGNodeTuple
>
currentIndexToNodeTuple
=
new
HashMap
<>();
private
Map
<
SDGEdge
,
StaticCGJavaMethod
>
summaryEdgesAndCorresJavaMethods
;
private
Map
<
SDGEdge
,
StaticCGJavaMethod
>
summaryEdgesAndCorresJavaMethods
;
...
@@ -103,7 +99,6 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
...
@@ -103,7 +99,6 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
private
SDGEdge
currentSelectedEdge
;
private
SDGEdge
currentSelectedEdge
;
private
StaticCGJavaMethod
currentSelectedMethod
;
private
StaticCGJavaMethod
currentSelectedMethod
;
private
CurrentActionLogger
currentActionLogger
;
private
CurrentActionLogger
currentActionLogger
;
private
boolean
autoRunIsRunning
=
false
;
private
boolean
useSlicing
=
false
;
private
boolean
useSlicing
=
false
;
private
boolean
useLoopUnwinding
=
false
;
private
boolean
useLoopUnwinding
=
false
;
private
boolean
useMethodInlining
=
false
;
private
boolean
useMethodInlining
=
false
;
...
@@ -204,6 +199,11 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
...
@@ -204,6 +199,11 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
setSUViewListFactory
();
setSUViewListFactory
();
}
}
/**
* enable or disable all Buttons
* (auto run, mark as disproven, reset loop invariant, save loop invariant, open selected in KeY and try Disprove)
* @param disable true to disable all {@link Button}s or false to enable all {@link Button}s.
*/
public
void
setAllButtonsDisable
(
boolean
disable
)
{
public
void
setAllButtonsDisable
(
boolean
disable
)
{
buttonRunAuto
.
setDisable
(
disable
);
buttonRunAuto
.
setDisable
(
disable
);
buttonMarkAsDisproved
.
setDisable
(
disable
);
buttonMarkAsDisproved
.
setDisable
(
disable
);
...
@@ -213,6 +213,9 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
...
@@ -213,6 +213,9 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
buttonTryDisprove
.
setDisable
(
disable
);
buttonTryDisprove
.
setDisable
(
disable
);
}
}
/**
* toggle availability of all Buttons except the Auto run button.
*/
private
void
toggleButtonsForAutoRun
()
{
private
void
toggleButtonsForAutoRun
()
{
buttonMarkAsDisproved
.
setDisable
(!
buttonMarkAsDisproved
.
isDisabled
());
buttonMarkAsDisproved
.
setDisable
(!
buttonMarkAsDisproved
.
isDisabled
());
buttonResetLoopInvariant
.
setDisable
(!
buttonResetLoopInvariant
.
isDisabled
());
buttonResetLoopInvariant
.
setDisable
(!
buttonResetLoopInvariant
.
isDisabled
());
...
@@ -342,6 +345,12 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
...
@@ -342,6 +345,12 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
return
disprovingProject
;
return
disprovingProject
;
}
}
/**
* generate a new {@link DisprovingProject} with the given {@link JoanaAndKeYCheckData}. This method disable all Buttons while generating
* the {@link DisprovingProject}.
* @param checkData
*/
public
void
handleNewDispro
(
JoanaAndKeYCheckData
checkData
)
{
public
void
handleNewDispro
(
JoanaAndKeYCheckData
checkData
)
{
setAllButtonsDisable
(
true
);
setAllButtonsDisable
(
true
);
backgroundDisproCreator
.
generateFromCheckData
(
checkData
,
(
dispro
,
worked
)
->
{
backgroundDisproCreator
.
generateFromCheckData
(
checkData
,
(
dispro
,
worked
)
->
{
...
@@ -769,7 +778,6 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
...
@@ -769,7 +778,6 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
// labelSomeOtherData.setText("All security violations have been disproved with KeY!");
// labelSomeOtherData.setText("All security violations have been disproved with KeY!");
this
.
setSomeOtherMessageAndColor
(
"All security violations have been disproved with KeY!"
,
Color
.
GREEN
);
this
.
setSomeOtherMessageAndColor
(
"All security violations have been disproved with KeY!"
,
Color
.
GREEN
);
buttonRunAuto
.
setDisable
(
true
);
buttonRunAuto
.
setDisable
(
true
);
//TODO: check this method !
displayAllViolationChecked
();
displayAllViolationChecked
();
// AutomationHelper.playSound(SOUND);
// AutomationHelper.playSound(SOUND);
});
});
...
@@ -822,7 +830,7 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
...
@@ -822,7 +830,7 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
}
}
//TODO: "CLOSED" check with datastructure
//TODO: "CLOSED" check with datastructure
. Dont use the the list item name ?
private
void
displayAllViolationChecked
()
{
private
void
displayAllViolationChecked
()
{
// for (int i : itemIndexToViolation.keySet()) {
// for (int i : itemIndexToViolation.keySet()) {
for
(
int
i
=
0
;
i
<
listViewUncheckedChops
.
getItems
().
size
();
i
++)
{
for
(
int
i
=
0
;
i
<
listViewUncheckedChops
.
getItems
().
size
();
i
++)
{
...
@@ -884,8 +892,6 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
...
@@ -884,8 +892,6 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
if
(
item
.
startsWith
(
"CLOSED"
))
{
if
(
item
.
startsWith
(
"CLOSED"
))
{
setStyle
(
"-fx-control-inner-background: "
+
HIGHLIGHTED_CONTROL_INNER_BACKGROUND
+
";"
);
setStyle
(
"-fx-control-inner-background: "
+
HIGHLIGHTED_CONTROL_INNER_BACKGROUND
+
";"
);
//TODO: dont disable, so you can still see the disproven edges. But disable the buttons for closed summary edges !
// setDisable(true);
// setDisable(true);
if
(!
violationsWrapper
.
allCheckedOrDisproved
())
{
if
(!
violationsWrapper
.
allCheckedOrDisproved
())
{
listViewUncheckedChops
.
getSelectionModel
().
select
(
0
);
listViewUncheckedChops
.
getSelectionModel
().
select
(
0
);
...
@@ -903,8 +909,8 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
...
@@ -903,8 +909,8 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
}
}
/**
/**
* this method set the cell factory of the
violation
listView.
* this method set the cell factory of the
summary edges
listView.
* Change the cells
if the violation
is closed/checked
* Change the cells
occurrence if the summary edge
is closed/checked
*/
*/
private
void
setSUViewListFactory
()
{
private
void
setSUViewListFactory
()
{
listViewSummaryEdges
.
setCellFactory
(
new
Callback
<
ListView
<
String
>,
ListCell
<
String
>>()
{
listViewSummaryEdges
.
setCellFactory
(
new
Callback
<
ListView
<
String
>,
ListCell
<
String
>>()
{
...
@@ -936,6 +942,11 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
...
@@ -936,6 +942,11 @@ public class DisproHandler implements ViolationsWrapperListener, SettingsObserve
}
}
/**
* set the gui status 'other message' to the given message in the given color
* @param message you want to print at the gui
* @param color in which you would like to have the message
*/
public
void
setSomeOtherMessageAndColor
(
String
message
,
javafx
.
scene
.
paint
.
Color
color
)
{
public
void
setSomeOtherMessageAndColor
(
String
message
,
javafx
.
scene
.
paint
.
Color
color
)
{
this
.
labelSomeOtherData
.
setText
(
message
);
this
.
labelSomeOtherData
.
setText
(
message
);
this
.
labelSomeOtherData
.
setTextFill
(
color
);
this
.
labelSomeOtherData
.
setTextFill
(
color
);
...
...
src/gui/JoanaKeYInterfacer.java
View file @
fb230341
...
@@ -8,6 +8,7 @@ package gui;
...
@@ -8,6 +8,7 @@ package gui;
import
java.io.IOException
;
import
java.io.IOException
;
import
java.util.ArrayList
;
import
java.util.ArrayList
;
import
edu.kit.joana.ifc.sdg.graph.SDG
;
import
edu.kit.joana.ifc.sdg.graph.SDGEdge
;
import
edu.kit.joana.ifc.sdg.graph.SDGEdge
;
import
edu.kit.joana.ifc.sdg.graph.SDGNodeTuple
;
import
edu.kit.joana.ifc.sdg.graph.SDGNodeTuple
;
import
joanakey.AutomationHelper
;
import
joanakey.AutomationHelper
;
...
@@ -19,11 +20,10 @@ import joanakey.violations.ViolationChop;
...
@@ -19,11 +20,10 @@ import joanakey.violations.ViolationChop;
import
joanakey.violations.ViolationsDisproverSemantic
;
import
joanakey.violations.ViolationsDisproverSemantic
;
import
joanakey.violations.ViolationsDisproverSemantic.PO_TYPE
;
import
joanakey.violations.ViolationsDisproverSemantic.PO_TYPE
;
import
joanakey.violations.ViolationsWrapper
;
import
joanakey.violations.ViolationsWrapper
;
import
keyjoana.settings.SettingsObserver
;
/**
/**
*
*
this class can be used to start the disproving process with KeY (also with command line mode)
* @author holger
* @author holger
, joachim
*/
*/
public
class
JoanaKeYInterfacer
{
public
class
JoanaKeYInterfacer
{
...
@@ -83,6 +83,14 @@ public class JoanaKeYInterfacer {
...
@@ -83,6 +83,14 @@ public class JoanaKeYInterfacer {
}
}
}
}
/**
* try to disprove the given summary Edge with KeY in command line mode.
* @param e {@link SDGEdge} you want to disprove
* @param tuple
* @param corresMethod
* @return true if successfully disproven. Otherwise return False.
* @throws IOException
*/
public
boolean
tryDisproveEdge
(
public
boolean
tryDisproveEdge
(
SDGEdge
e
,
SDGEdge
e
,
SDGNodeTuple
tuple
,
SDGNodeTuple
tuple
,
...
@@ -111,6 +119,11 @@ public class JoanaKeYInterfacer {
...
@@ -111,6 +119,11 @@ public class JoanaKeYInterfacer {
return
worked
;
return
worked
;
}
}
/**
* mark the given {@link SDGEdge} as disproven and remove it from the {@link SDG} in {@link ViolationsWrapper}.
* @param currentSelectedEdge the {@link SDGEdge} you want to mark as disproven.
* @throws IllegalArgumentException
*/
public
void
markAsDisproved
(
SDGEdge
currentSelectedEdge
)
throws
IllegalArgumentException
{
public
void
markAsDisproved
(
SDGEdge
currentSelectedEdge
)
throws
IllegalArgumentException
{
if
(
currentSelectedEdge
==
null
)
{
if
(
currentSelectedEdge
==
null
)
{
throw
new
IllegalArgumentException
(
"No method selected!"
);
throw
new
IllegalArgumentException
(
"No method selected!"
);
...
@@ -132,11 +145,19 @@ public class JoanaKeYInterfacer {
...
@@ -132,11 +145,19 @@ public class JoanaKeYInterfacer {
this
.
useSlicedFiles
=
selected
;
this
.
useSlicedFiles
=
selected
;
}
}
/**
* set method inlining option for the disproving process
* @param selected true, if you want to use method inlining
*/
public
void
setUseMethodInlining
(
boolean
selected
)
{
public
void
setUseMethodInlining
(
boolean
selected
)
{
this
.
useMethodInlining
=
selected
;
this
.
useMethodInlining
=
selected
;
javaForKeyCreator
.
setMethodInlining
(
selected
);
javaForKeyCreator
.
setMethodInlining
(
selected
);
}
}
/**
* set loop unwinding option for the disproving process
* @param selected true, if you want to use loop unwinding
*/
public
void
setUseLoopUnwinding
(
boolean
selected
)
{
public
void
setUseLoopUnwinding
(
boolean
selected
)
{
this
.
useLoopUnwinding
=
selected
;
this
.
useLoopUnwinding
=
selected
;
javaForKeyCreator
.
setUseLoopUnwinding
(
selected
);
javaForKeyCreator
.
setUseLoopUnwinding
(
selected
);
...
...
src/gui/MainWindowController.java
View file @
fb230341
...
@@ -37,7 +37,7 @@ import keyjoana.util.FilesUtil;
...
@@ -37,7 +37,7 @@ import keyjoana.util.FilesUtil;
/**
/**
*
*
* @author holger
* @author holger
,joachim
*/
*/
public
class
MainWindowController
implements
Initializable
,
SettingsObserver
{
public
class
MainWindowController
implements
Initializable
,
SettingsObserver
{
...
@@ -282,6 +282,7 @@ public class MainWindowController implements Initializable, SettingsObserver {
...
@@ -282,6 +282,7 @@ public class MainWindowController implements Initializable, SettingsObserver {
});
});
}
}
@SuppressWarnings
(
"unused"
)
@Deprecated
@Deprecated
private
void
reloadLastFile
()
{
private
void
reloadLastFile
()
{
if
(
lastFileLoaded
==
null
)
{
if
(
lastFileLoaded
==
null
)
{
...
@@ -340,9 +341,7 @@ public class MainWindowController implements Initializable, SettingsObserver {
...
@@ -340,9 +341,7 @@ public class MainWindowController implements Initializable, SettingsObserver {
keyJoanaSettings
.
addSettingObserver
(
settingsManager
);
keyJoanaSettings
.
addSettingObserver
(
settingsManager
);
keyJoanaSettings
.
addSettingObserver
(
this
);
keyJoanaSettings
.
addSettingObserver
(
this
);
settingsManager
.
loadSettings
();
settingsManager
.
loadSettings
();
//TODO: load settings from file with settingsmanager
//TODO: remove boolean settings (loopundwind, method expand, slicing, and use keyJoanaSettings instead
disproHandler
=
new
DisproHandler
(
actionLogger
,
labelProjName
,
labelSummaryEdge
,
labelSomeOtherData
,
disproHandler
=
new
DisproHandler
(
actionLogger
,
labelProjName
,
labelSummaryEdge
,
labelSomeOtherData
,
menuBarMain
,
listViewUncheckedEdges
,
listViewUncheckedChops
,
listViewCalledMethodsOfSE
,
menuBarMain
,
listViewUncheckedEdges
,
listViewUncheckedChops
,
listViewCalledMethodsOfSE
,
listViewLoopsOfSE
,
listViewFormalInoutPairs
,
anchorPaneMethodCode
,
anchorPaneLoopInvariant
,
listViewLoopsOfSE
,
listViewFormalInoutPairs
,
anchorPaneMethodCode
,
anchorPaneLoopInvariant
,
...
...
src/gui/RecentlyUsedFilesManager.java
View file @
fb230341
...
@@ -9,7 +9,7 @@ import java.util.ArrayList;
...
@@ -9,7 +9,7 @@ import java.util.ArrayList;
/**
/**
* this class manages the recently loaded files
* this class manages the recently loaded files
* @author joachim
muessig
* @author joachim
*
*
*/
*/
public
class
RecentlyUsedFilesManager
{
public
class
RecentlyUsedFilesManager
{
...
@@ -93,7 +93,6 @@ public class RecentlyUsedFilesManager {
...
@@ -93,7 +93,6 @@ public class RecentlyUsedFilesManager {
if
(
recentlyUsedFiles
.
size
()
>
maxNumberOfSavedRecentlyLoadedFiles
)
{
if
(
recentlyUsedFiles
.
size
()
>
maxNumberOfSavedRecentlyLoadedFiles
)
{
recentlyUsedFiles
.
remove
(
recentlyUsedFiles
.
size
()-
1
);
recentlyUsedFiles
.
remove
(
recentlyUsedFiles
.
size
()-
1
);
}
}
//TODO:Update list/stack/array for the recently loaded file
//Update mostRecentlyUsedFile
//Update mostRecentlyUsedFile
//store new content in the File for recently loaded files
//store new content in the File for recently loaded files
try
{
try
{
...
...
Write
Preview
Supports
Markdown
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