Skip to content

Commit 388e20b

Browse files
committed
ghost modifier in Java are back
1 parent 2e7d533 commit 388e20b

File tree

2 files changed

+2
-5
lines changed

2 files changed

+2
-5
lines changed

key.core/build.gradle

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ dependencies {
2222

2323
api project(':key.util')
2424

25-
def JP_VERSION = "3.28.0-K12.5"
25+
def JP_VERSION = "3.28.0-K12.7"
2626
api "org.key-project.proofjava:javaparser-core:$JP_VERSION"
2727
api "org.key-project.proofjava:javaparser-core-serialization:$JP_VERSION"
2828
api "org.key-project.proofjava:javaparser-symbol-solver-core:$JP_VERSION"

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -412,15 +412,13 @@
412412
\displayname "variableDeclaration"
413413
};
414414

415-
/*
416415
variableDeclarationGhost {
417416
\find(\modality{#allmodal}{.. ghost #t #v0; ...}\endmodality (post))
418417
\replacewith(\modality{#allmodal}{.. ...}\endmodality (post))
419418
\addprogvars(#v0)
420419
\heuristics(simplify_prog, simplify_prog_subset)
421420
\displayname "ghostDeclaration"
422421
};
423-
*/
424422

425423
variableDeclarationAssign {
426424
\find(\modality{#allmodal}{.. #t #v0 = #vi; ...}\endmodality (post))
@@ -436,13 +434,12 @@
436434
\displayname "variableDeclaration"
437435
};
438436

439-
/*
440437
variableDeclarationGhostAssign {
441438
\find(\modality{#allmodal}{.. ghost #t #v0 = #vi; ...}\endmodality (post))
442439
\replacewith(\modality{#allmodal}{.. ghost #t #v0; #v0 = #vi; ...}\endmodality (post))
443440
\heuristics(simplify_prog, simplify_prog_subset)
444441
\displayname "ghostDeclaration"
445-
};*/
442+
};
446443

447444
variableDeclarationMult {
448445
\find(\modality{#allmodal}{.. #multvardecl ...}\endmodality (post))

0 commit comments

Comments
 (0)