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
76480379
Commit
76480379
authored
Nov 22, 2019
by
Joachim Müssig
Browse files
create newest version of false positiv example 'mixtureLoops'
parent
50f4c070
Changes
5
Hide whitespace changes
Inline
Side-by-side
testdata/FalsePositiveExamples/mixtureloops/SDG/MixtureWithLoop.pdg
View file @
76480379
...
...
@@ -13,7 +13,7 @@ HE 4;
HE 5;
HE 6;
HE 9;
HE 2
39
;
HE 2
44
;
PS 3;
PS 4;
CF 4;
...
...
@@ -23,7 +23,7 @@ CD 9;
CE 2;
CE 3;
CE 4;
CE 2
39
;
CE 2
44
;
}
EXIT 2 {
O exit;
...
...
@@ -43,7 +43,7 @@ P 4;
S "MixtureWithLoop.java":0,0-0,0;
B "<exception>":-2;
Z 0;
CF 2
39
: "exc";
CF 2
44
: "exc";
PO 36;
}
FRMI 4 {
...
...
@@ -55,7 +55,7 @@ S "MixtureWithLoop.java":0,0-0,0;
B "<param> 1":-2;
Z 0;
LD ["null"];
PS 2
39
;
PS 2
44
;
CF 5;
}
NORM 5 {
...
...
@@ -80,13 +80,13 @@ B "MixtureWithLoop.main([Ljava/lang/String;)V":4;
Z 0;
HE 7;
HE 8;
HE 24
0
;
HE 24
5
;
PS 7;
PS 8;
CF 251;
CE 7;
CE 8;
CE 24
0
;
CE 24
5
;
CE 251;
CL 37: "virtual";
}
...
...
@@ -98,11 +98,11 @@ P 4;
S "MixtureWithLoop.java":5,0-5,0;
B "<param> 0":-2;
Z 0;
PS 24
0
;
PS 24
5
;
CF 6;
CD 6;
SU 8;
SU 24
0
;
SU 24
5
;
PI 40;
}
ACTO 8 {
...
...
@@ -214,7 +214,7 @@ P 4;
S "MixtureWithLoop.java":6,0-6,0;
B "MixtureWithLoop.main([Ljava/lang/String;)V":13;
Z 0;
CF 2
39
;
CF 2
44
;
}
ENTR 20 {
O entry;
...
...
@@ -263,13 +263,13 @@ Z 0;
U "com.ibm.wala.FakeRootClass.fakeWorldClinit()V";
HE 24;
HE 25;
HE 24
3
;
HE 24
1
;
HE 248;
PS 24;
CF 248;
CD 25;
CE 24;
CE 24
3
;
CE 24
1
;
CE 248;
}
ACTO 24 {
...
...
@@ -383,7 +383,7 @@ U "java.lang.Object.<init>()V";
HE 32;
HE 33;
HE 34;
HE 24
4
;
HE 24
2
;
HE 246;
HE 249;
PS 32;
...
...
@@ -392,7 +392,7 @@ CF 249;
CD 34;
CE 32;
CE 33;
CE 24
4
;
CE 24
2
;
CE 246;
CE 249;
}
...
...
@@ -404,7 +404,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<param> 0":-2;
Z 0;
PS 24
4
;
PS 24
2
;
CF 31;
CD 31;
DD 249;
...
...
@@ -431,13 +431,13 @@ B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
HE 35;
HE 36;
HE 24
5
;
HE 24
3
;
PS 35;
PS 36;
CF 253;
CE 35;
CE 36;
CE 24
5
;
CE 24
3
;
CE 253;
CL 1: "virtual";
}
...
...
@@ -449,7 +449,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "<param> 1":-2;
Z 0;
PS 24
5
;
PS 24
3
;
CF 34;
PI 4;
}
...
...
@@ -478,7 +478,7 @@ HE 38;
HE 39;
HE 40;
HE 41;
HE 2
41
;
HE 2
39
;
PS 39;
PS 40;
CF 40;
...
...
@@ -486,7 +486,7 @@ CD 41;
CE 38;
CE 39;
CE 40;
CE 2
41
;
CE 2
39
;
}
EXIT 38 {
O exit;
...
...
@@ -506,7 +506,7 @@ P 6;
S "MixtureWithLoop.java":0,0-0,0;
B "<exception>":-2;
Z 0;
CF 2
41
: "exc";
CF 2
39
: "exc";
PO 8;
}
FRMI 40 {
...
...
@@ -518,7 +518,7 @@ S "MixtureWithLoop.java":0,0-0,0;
B "<param> 0":-2;
Z 0;
LD ["null"];
PS 2
41
;
PS 2
39
;
CF 42;
DD 42;
}
...
...
@@ -534,7 +534,7 @@ U "java.lang.Object.<init>()V";
HE 42;
HE 43;
HE 44;
HE 24
2
;
HE 24
0
;
HE 247;
HE 250;
PS 42;
...
...
@@ -543,7 +543,7 @@ CF 250;
CD 44;
CE 42;
CE 43;
CE 24
2
;
CE 24
0
;
CE 247;
CE 250;
}
...
...
@@ -555,7 +555,7 @@ P 6;
S "MixtureWithLoop.java":1,0-1,0;
B "<param> 0":-2;
Z 0;
PS 24
2
;
PS 24
0
;
CF 41;
CD 41;
DD 250;
...
...
@@ -580,7 +580,7 @@ P 6;
S "MixtureWithLoop.java":1,0-1,0;
B "MixtureWithLoop.<init>()V":4;
Z 0;
CF 2
41
;
CF 2
39
;
}
ENTR 46 {
O entry;
...
...
@@ -2322,36 +2322,14 @@ FRMO 239 {
O form-out;
V "[M] |0|UNIQ(code)";
T "I";
P 4;
S "MixtureWithLoop.java":0,0-0,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 2;
PO 245;
}
ACTO 240 {
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
P 4;
S "MixtureWithLoop.java":5,0-5,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 8;
DH 239;
}
FRMO 241 {
O form-out;
V "[M] |0|UNIQ(code)";
T "I";
P 6;
S "MixtureWithLoop.java":0,0-0,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 38;
PO 24
0
;
PO 24
5
;
}
ACTO 24
2
{
ACTO 24
0
{
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
...
...
@@ -2362,9 +2340,9 @@ Z 0;
CF 43: "exc";
CF 44;
DD 247;
DH 2
41
;
DH 2
39
;
}
ACTO 24
3
{
ACTO 24
1
{
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
...
...
@@ -2375,7 +2353,7 @@ Z 0;
CF 24: "exc";
CF 25;
}
ACTO 24
4
{
ACTO 24
2
{
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
...
...
@@ -2387,7 +2365,7 @@ CF 33: "exc";
CF 35;
DD 246;
}
ACTO 24
5
{
ACTO 24
3
{
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
...
...
@@ -2398,6 +2376,28 @@ Z 0;
CF 21;
CF 36: "exc";
}
FRMO 244 {
O form-out;
V "[M] |0|UNIQ(code)";
T "I";
P 4;
S "MixtureWithLoop.java":0,0-0,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 2;
PO 243;
}
ACTO 245 {
O act-out;
V "[M] |0|UNIQ(code)";
T "I";
P 4;
S "MixtureWithLoop.java":5,0-5,0;
B "Ljava/lang/Object.code":-4;
Z 0;
CF 8;
DH 244;
}
NORM 246 {
O compound;
V "immutable";
...
...
@@ -2405,7 +2405,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
CF 24
4
;
CF 24
2
;
DD 25;
}
NORM 247 {
...
...
@@ -2415,7 +2415,7 @@ P 6;
S "MixtureWithLoop.java":0,0-0,0;
B "MixtureWithLoop.<init>()V":-1;
Z 0;
CF 24
2
;
CF 24
0
;
DD 40;
}
NORM 248 {
...
...
@@ -2425,9 +2425,9 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
CF 24
3
;
CF 24
1
;
DD 24;
DD 24
3
;
DD 24
1
;
}
NORM 249 {
O compound;
...
...
@@ -2438,7 +2438,7 @@ B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-1;
Z 0;
CF 246;
DD 33;
DD 24
4
;
DD 24
2
;
}
NORM 250 {
O compound;
...
...
@@ -2449,7 +2449,7 @@ B "MixtureWithLoop.<init>()V":-1;
Z 0;
CF 247;
DD 43;
DD 24
2
;
DD 24
0
;
}
NORM 251 {
O compound;
...
...
@@ -2458,7 +2458,7 @@ P 4;
S "MixtureWithLoop.java":5,0-5,0;
B "MixtureWithLoop.main([Ljava/lang/String;)V":-9;
Z 0;
CF 24
0
;
CF 24
5
;
}
NORM 252 {
O compound;
...
...
@@ -2478,7 +2478,7 @@ P 5;
S "com/ibm/wala/FakeRootClass.java":0,0-0,0;
B "com.ibm.wala.FakeRootClass.fakeRootMethod()V":-9;
Z 0;
CF 24
5
;
CF 24
3
;
}
NORM 254 {
O compound;
...
...
testdata/FalsePositiveExamples/mixtureloops/mixtureloopsNew.joak
0 → 100644
View file @
76480379
directoryPath : "/home/joachim/git/KeYJoana/keyjoana/testdata/FalsePositiveExamples/mixtureloops",
pathKeY : "dependencies/Key/KeY.jar",
javaClass : "",
pathToJar : "testdata/build/src.jar",
pathToJavaFile : "src/",
pathToSDG : "SDG/MixtureWithLoop.pdg",
entryMethod : "MixtureWithLoop",
annotationPath : "",
fullyAutomatic : true,
pathToSaver : "SDG/MixtureWithLoop.dispro",
sources : [{securityLevel : "high", description : {from : "programPart", programPart : "parameter <param> 1 of method int MixtureWithLoop.testMethod(int, int)"}}],
sinks : [{securityLevel : "low", description : {from : "programPart", programPart : "exit of method int MixtureWithLoop.testMethod(int, int)"}}]
\ No newline at end of file
testdata/FalsePositiveExamples/mixtureloops/slices/sliceSource50Sink47/src/MixtureWithLoop.java
View file @
76480379
public
class
MixtureWithLoop
{
public
static
void
main
(
String
[
]
args
)
{
new
MixtureWithLoop
(
)
.
testMethod
(
1
,
2
)
;
}
public
int
testMethod
(
int
high
,
int
low
)
{
int
l
=
mixtureWithLoop
(
low
,
high
)
;
return
l
;
}
private
int
mixtureWithLoop
(
int
l
,
int
h
)
{
int
x
=
arrayInsecure
(
l
,
h
)
;
x
=
loopOverride
(
l
,
x
)
;
x
+=
arrayAccess
(
x
,
h
)
;
x
=
justSet
(
l
,
x
)
;
int
y
=
loopOverride
(
l
,
h
)
;
return
x
+
y
;
}
public
int
loopOverride
(
int
l
,
int
h
)
{
int
y
=
l
;
for
(
int
i
=
0
;
i
<
5
;
i
++
)
{
if
(
i
<
4
)
{
l
=
l
+
h
;
}
else
{
public
static
void
main
(
String
[
]
args
)
{
new
MixtureWithLoop
(
)
.
testMethod
(
1
,
2
)
;
}
public
int
testMethod
(
int
high
,
int
low
)
{
int
l
=
mixtureWithLoop
(
low
,
high
)
;
return
l
;
}
private
int
mixtureWithLoop
(
int
l
,
int
h
)
{
int
x
=
arrayInsecure
(
l
,
h
)
;
x
=
loopOverride
(
l
,
x
)
;
x
+=
arrayAccess
(
x
,
h
)
;
x
=
justSet
(
l
,
x
)
;
int
y
=
loopOverride
(
l
,
h
)
;
return
x
+
y
;
}
public
int
loopOverride
(
int
l
,
int
h
)
{
int
y
=
l
;
for
(
int
i
=
0
;
i
<
5
;
i
++
)
{
if
(
i
<
4
)
{
l
=
l
+
h
;
}
else
{
assume
(
false
);
l
=
y
;
}
}
return
l
;
}
private
int
arrayInsecure
(
int
low
,
int
high
)
{
return
0
;
}
private
int
arrayAccess
(
int
l
,
int
h
)
{
int
[
]
array
=
new
int
[
3
]
;
array
[
0
]
=
l
;
array
[
1
]
=
h
;
array
[
2
]
=
array
[
1
]
;
return
array
[
2
]
;
}
private
int
justSet
(
int
l
,
int
h
)
{
int
[
]
array
=
new
int
[
5
]
;
array
[
0
]
=
5
;
array
[
1
]
=
h
;
l
=
array
[
0
]
;
return
l
;
}
l
=
y
;
}
}
return
l
;
}
private
int
arrayInsecure
(
int
low
,
int
high
)
{
return
0
;
}
private
int
arrayAccess
(
int
l
,
int
h
)
{
int
[
]
array
=
new
int
[
3
]
;
array
[
0
]
=
l
;
array
[
1
]
=
h
;
array
[
2
]
=
array
[
1
]
;
return
array
[
2
]
;
}
private
int
justSet
(
int
l
,
int
h
)
{
int
[
]
array
=
new
int
[
5
]
;
array
[
0
]
=
5
;
array
[
1
]
=
h
;
l
=
array
[
0
]
;
return
l
;
}
/*@
@ requires true;
@ ensures b;
...
...
testdata/FalsePositiveExamples/mixtureloops/src/MixtureWithLoop.java
View file @
76480379
public
class
MixtureWithLoop
{
public
static
void
main
(
String
[
]
args
)
{
new
MixtureWithLoop
(
)
.
testMethod
(
1
,
2
)
;
}
public
int
testMethod
(
int
high
,
int
low
)
{
int
l
=
mixtureWithLoop
(
low
,
high
)
;
return
l
;
}
private
int
mixtureWithLoop
(
int
l
,
int
h
)
{
int
x
=
arrayInsecure
(
l
,
h
)
;
x
=
loopOverride
(
l
,
x
)
;
x
+=
arrayAccess
(
x
,
h
)
;
x
=
justSet
(
l
,
x
)
;
int
y
=
loopOverride
(
l
,
h
)
;
return
x
+
y
;
}
public
int
loopOverride
(
int
l
,
int
h
)
{
int
y
=
l
;
for
(
int
i
=
0
;
i
<
5
;
i
++
)
{
if
(
i
<
4
)
{
l
=
l
+
h
;
}
else
{
l
=
y
;
}
}
return
l
;
}
private
int
arrayInsecure
(
int
low
,
int
high
)
{
return
0
;
}
private
int
arrayAccess
(
int
l
,
int
h
)
{
int
[
]
array
=
new
int
[
3
]
;
array
[
0
]
=
l
;
array
[
1
]
=
h
;
array
[
2
]
=
array
[
1
]
;
return
array
[
2
]
;
}
private
int
justSet
(
int
l
,
int
h
)
{
int
[
]
array
=
new
int
[
5
]
;
array
[
0
]
=
5
;
array
[
1
]
=
h
;
l
=
array
[
0
]
;
return
l
;
}
public
static
void
main
(
String
[
]
args
)
{
new
MixtureWithLoop
(
)
.
testMethod
(
1
,
2
)
;
}
public
int
testMethod
(
int
high
,
int
low
)
{
int
l
=
mixtureWithLoop
(
low
,
high
)
;
return
l
;
}
private
int
mixtureWithLoop
(
int
l
,
int
h
)
{
int
x
=
arrayInsecure
(
l
,
h
)
;
x
=
loopOverride
(
l
,
x
)
;
x
+=
arrayAccess
(
x
,
h
)
;
x
=
justSet
(
l
,
x
)
;
int
y
=
loopOverride
(
l
,
h
)
;
return
x
+
y
;
}
public
int
loopOverride
(
int
l
,
int
h
)
{
int
y
=
l
;
for
(
int
i
=
0
;
i
<
5
;
i
++
)
{
if
(
i
<
4
)
{
l
=
l
+
h
;
}
else
{
l
=
y
;
}
}
return
l
;
}
private
int
arrayInsecure
(
int
low
,
int
high
)
{
return
0
;
}
private
int
arrayAccess
(
int
l
,
int
h
)
{
int
[
]
array
=
new
int
[
3
]
;
array
[
0
]
=
l
;
array
[
1
]
=
h
;
array
[
2
]
=
array
[
1
]
;
return
array
[
2
]
;
}
private
int
justSet
(
int
l
,
int
h
)
{
int
[
]
array
=
new
int
[
5
]
;
array
[
0
]
=
5
;
array
[
1
]
=
h
;
l
=
array
[
0
]
;