Skip to content

Commit 957b469

Browse files
authored
Add conversion rules for Float/Double negation (KeYProject#3520)
2 parents a59c293 + 1989ce9 commit 957b469

File tree

1 file changed

+11
-0
lines changed

1 file changed

+11
-0
lines changed

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,11 @@
88
}
99

1010
\rules(programRules:Java, floatRules:assumeStrictfp) {
11+
translateJavaUnaryMinusFloat {
12+
\find(javaUnaryMinusFloat(f1))
13+
\replacewith(negFloat(f1))
14+
\heuristics(javaFloatSemantics)
15+
};
1116

1217
translateJavaAddFloat {
1318
\find(javaAddFloat(f1, f2))
@@ -33,6 +38,12 @@
3338
\heuristics(javaFloatSemantics)
3439
};
3540

41+
translateJavaUnaryMinusDouble {
42+
\find(javaUnaryMinusDouble(d1))
43+
\replacewith(negDouble(d1))
44+
\heuristics(javaFloatSemantics)
45+
};
46+
3647
translateJavaAddDouble {
3748
\find(javaAddDouble(d1, d2))
3849
\replacewith(addDouble(d1, d2))

0 commit comments

Comments
 (0)