intRulesCheckedSemantics.key

Taclets

No choice condition specified

translateCheckedUnaryMinusInt

translateCheckedUnaryMinusInt  {
\find (                    checkedUnaryMinusInt   (                   left ))
  \replacewith (                    neg   (                   left ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 17 Offset :4

translateCheckedUnaryMinusLong

translateCheckedUnaryMinusLong  {
\find (                    checkedUnaryMinusLong   (                   left ))
  \replacewith (                    neg   (                   left ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 23 Offset :4

translateCheckedBitwiseNegateInt

translateCheckedBitwiseNegateInt  {
\find (                    checkedBitwiseNegateInt   (                   left ))
  \replacewith (                    sub   (                   neg   (                   left ),                    1 ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 29 Offset :4

translateCheckedBitwiseNegateLong

translateCheckedBitwiseNegateLong  {
\find (                    checkedBitwiseNegateLong   (                   left ))
  \replacewith (                    sub   (                   neg   (                   left ),                    1 ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 35 Offset :4

translateCheckedAddInt

translateCheckedAddInt  {
\find (                    checkedAddInt   (                   left ,                    right ))
  \replacewith (                    add   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 41 Offset :4

translateCheckedAddLong

translateCheckedAddLong  {
\find (                    checkedAddLong   (                   left ,                    right ))
  \replacewith (                    add   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 47 Offset :4

translateCheckedSubInt

translateCheckedSubInt  {
\find (                    checkedSubInt   (                   left ,                    right ))
  \replacewith (                    sub   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 53 Offset :4

translateCheckedSubLong

translateCheckedSubLong  {
\find (                    checkedSubLong   (                   left ,                    right ))
  \replacewith (                    sub   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 58 Offset :4

translateCheckedMulInt

translateCheckedMulInt  {
\find (                    checkedMulInt   (                   left ,                    right ))
  \replacewith (                    mul   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 64 Offset :4

translateCheckedMulLong

translateCheckedMulLong  {
\find (                    checkedMulLong   (                   left ,                    right ))
  \replacewith (                    mul   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 70 Offset :4

translateCheckedDivInt

translateCheckedDivInt  {
\find (                    checkedDivInt   (                   left ,                    right ))
  \replacewith (                    jdiv   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 76 Offset :4

translateCheckedDivLong

translateCheckedDivLong  {
\find (                    checkedDivLong   (                   left ,                    right ))
  \replacewith (                    jdiv   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 82 Offset :4

translateCheckedShiftRightInt

translateCheckedShiftRightInt  {
\find (                    checkedShiftRightInt   (                   left ,                    right ))
  \replacewith (                    shiftright   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 88 Offset :4

translateCheckedShiftRightLong

translateCheckedShiftRightLong  {
\find (                    checkedShiftRightLong   (                   left ,                    right ))
  \replacewith (                    shiftright   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 94 Offset :4

translateCheckedShiftLeftInt

translateCheckedShiftLeftInt  {
\find (                    checkedShiftLeftInt   (                   left ,                    right ))
  \replacewith (                    shiftleft   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 100 Offset :4

translateCheckedShiftLeftLong

translateCheckedShiftLeftLong  {
\find (                    checkedShiftLeftLong   (                   left ,                    right ))
  \replacewith (                    shiftleft   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 106 Offset :4

translateCheckedBitwiseOrInt

translateCheckedBitwiseOrInt  {
\find (                    checkedBitwiseOrInt   (                   left ,                    right ))
  \replacewith (                    binaryOr   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 126 Offset :4

translateCheckedBitwiseOrLong

translateCheckedBitwiseOrLong  {
\find (                    checkedBitwiseOrLong   (                   left ,                    right ))
  \replacewith (                    binaryOr   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 132 Offset :4

translateCheckedBitwiseAndInt

translateCheckedBitwiseAndInt  {
\find (                    checkedBitwiseAndInt   (                   left ,                    right ))
  \replacewith (                    binaryAnd   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 138 Offset :4

translateCheckedBitwiseAndLong

translateCheckedBitwiseAndLong  {
\find (                    checkedBitwiseAndLong   (                   left ,                    right ))
  \replacewith (                    binaryAnd   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 144 Offset :4

translateCheckedBitwiseXOrInt

translateCheckedBitwiseXOrInt  {
\find (                    checkedBitwiseXOrInt   (                   left ,                    right ))
  \replacewith (                    binaryXOr   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 150 Offset :4

translateCheckedBitwiseXOrLong

translateCheckedBitwiseXOrLong  {
\find (                    checkedBitwiseXOrLong   (                   left ,                    right ))
  \replacewith (                    binaryXOr   (                   left ,                    right ))
\heuristics  (simplify )

};

defined in: intRulesCheckedSemantics.key Line: 156 Offset :4

KeY Logic Documentation

Defined symbols in the KeY System

Overview