translateJavaAddFloat {
\find ( javaAddFloat ( f1 , f2 ))
\replacewith ( addFloat ( f1 , f2 ))
\heuristics (javaFloatSemantics )
};defined in: floatRulesAssumeStrictfp.key Line: 12 Offset :4translateJavaSubFloat {
\find ( javaSubFloat ( f1 , f2 ))
\replacewith ( subFloat ( f1 , f2 ))
\heuristics (javaFloatSemantics )
};defined in: floatRulesAssumeStrictfp.key Line: 18 Offset :4translateJavaMulFloat {
\find ( javaMulFloat ( f1 , f2 ))
\replacewith ( mulFloat ( f1 , f2 ))
\heuristics (javaFloatSemantics )
};defined in: floatRulesAssumeStrictfp.key Line: 24 Offset :4translateJavaDivFloat {
\find ( javaDivFloat ( f1 , f2 ))
\replacewith ( divFloat ( f1 , f2 ))
\heuristics (javaFloatSemantics )
};defined in: floatRulesAssumeStrictfp.key Line: 30 Offset :4translateJavaAddDouble {
\find ( javaAddDouble ( d1 , d2 ))
\replacewith ( addDouble ( d1 , d2 ))
\heuristics (javaFloatSemantics )
};defined in: floatRulesAssumeStrictfp.key Line: 36 Offset :4translateJavaSubDouble {
\find ( javaSubDouble ( d1 , d2 ))
\replacewith ( subDouble ( d1 , d2 ))
\heuristics (javaFloatSemantics )
};defined in: floatRulesAssumeStrictfp.key Line: 42 Offset :4translateJavaMulDouble {
\find ( javaMulDouble ( d1 , d2 ))
\replacewith ( mulDouble ( d1 , d2 ))
\heuristics (javaFloatSemantics )
};defined in: floatRulesAssumeStrictfp.key Line: 48 Offset :4translateJavaDivDouble {
\find ( javaDivDouble ( d1 , d2 ))
\replacewith ( divDouble ( d1 , d2 ))
\heuristics (javaFloatSemantics )
};defined in: floatRulesAssumeStrictfp.key Line: 54 Offset :4doubleSin {
\schemaVar \program Variable #loc;
\schemaVar \program SimpleExpression #se;
\schemaVar \formula post ;
\schemaVar \modalOperator { diamond , box , diamond_transaction , box_transaction } #allmodal;
\find ( \modality{#allmodal}{.. #loc = java.lang.Math.sin(#se); ...}\endmodality ( post ))
\replacewith ( { #loc:= sinDouble ( #se)} \modality{#allmodal}{.. ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: floatRulesAssumeStrictfp.key Line: 62 Offset :4doubleCos {
\schemaVar \program Variable #loc;
\schemaVar \program SimpleExpression #se;
\schemaVar \formula post ;
\schemaVar \modalOperator { diamond , box , diamond_transaction , box_transaction } #allmodal;
\find ( \modality{#allmodal}{.. #loc = java.lang.Math.cos(#se); ...}\endmodality ( post ))
\replacewith ( { #loc:= cosDouble ( #se)} \modality{#allmodal}{.. ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: floatRulesAssumeStrictfp.key Line: 72 Offset :4doubleAcos {
\schemaVar \program Variable #loc;
\schemaVar \program SimpleExpression #se;
\schemaVar \formula post ;
\schemaVar \modalOperator { diamond , box , diamond_transaction , box_transaction } #allmodal;
\find ( \modality{#allmodal}{.. #loc = java.lang.Math.acos(#se); ...}\endmodality ( post ))
\replacewith ( { #loc:= acosDouble ( #se)} \modality{#allmodal}{.. ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: floatRulesAssumeStrictfp.key Line: 82 Offset :4doubleAsin {
\schemaVar \program Variable #loc;
\schemaVar \program SimpleExpression #se;
\schemaVar \formula post ;
\schemaVar \modalOperator { diamond , box , diamond_transaction , box_transaction } #allmodal;
\find ( \modality{#allmodal}{.. #loc = java.lang.Math.asin(#se); ...}\endmodality ( post ))
\replacewith ( { #loc:= asinDouble ( #se)} \modality{#allmodal}{.. ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: floatRulesAssumeStrictfp.key Line: 92 Offset :4doubleTan {
\schemaVar \program Variable #loc;
\schemaVar \program SimpleExpression #se;
\schemaVar \formula post ;
\schemaVar \modalOperator { diamond , box , diamond_transaction , box_transaction } #allmodal;
\find ( \modality{#allmodal}{.. #loc = java.lang.Math.tan(#se); ...}\endmodality ( post ))
\replacewith ( { #loc:= tanDouble ( #se)} \modality{#allmodal}{.. ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: floatRulesAssumeStrictfp.key Line: 102 Offset :4doubleAtan2 {
\schemaVar \program Variable #loc;
\schemaVar \program SimpleExpression #se1;
\schemaVar \program SimpleExpression #se2;
\schemaVar \formula post ;
\schemaVar \modalOperator { diamond , box , diamond_transaction , box_transaction } #allmodal;
\find ( \modality{#allmodal}{.. #loc = java.lang.Math.atan2(#se1, #se2); ...}\endmodality ( post ))
\replacewith ( { #loc:= atan2Double ( #se1, #se2)} \modality{#allmodal}{.. ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: floatRulesAssumeStrictfp.key Line: 112 Offset :4doubleSqrt {
\schemaVar \program Variable #loc;
\schemaVar \program SimpleExpression #se;
\schemaVar \formula post ;
\schemaVar \modalOperator { diamond , box , diamond_transaction , box_transaction } #allmodal;
\find ( \modality{#allmodal}{.. #loc = java.lang.Math.sqrt(#se); ...}\endmodality ( post ))
\replacewith ( { #loc:= sqrtDouble ( #se)} \modality{#allmodal}{.. ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: floatRulesAssumeStrictfp.key Line: 123 Offset :4doublePow {
\schemaVar \program Variable #loc;
\schemaVar \program SimpleExpression #se1;
\schemaVar \program SimpleExpression #se2;
\schemaVar \formula post ;
\schemaVar \modalOperator { diamond , box , diamond_transaction , box_transaction } #allmodal;
\find ( \modality{#allmodal}{.. #loc = java.lang.Math.pow(#se1, #se2); ...}\endmodality ( post ))
\replacewith ( { #loc:= powDouble ( #se1, #se2)} \modality{#allmodal}{.. ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: floatRulesAssumeStrictfp.key Line: 133 Offset :4doubleExp {
\schemaVar \program Variable #loc;
\schemaVar \program SimpleExpression #se;
\schemaVar \formula post ;
\schemaVar \modalOperator { diamond , box , diamond_transaction , box_transaction } #allmodal;
\find ( \modality{#allmodal}{.. #loc = java.lang.Math.exp(#se); ...}\endmodality ( post ))
\replacewith ( { #loc:= expDouble ( #se)} \modality{#allmodal}{.. ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: floatRulesAssumeStrictfp.key Line: 144 Offset :4doubleAtan {
\schemaVar \program Variable #loc;
\schemaVar \program SimpleExpression #se;
\schemaVar \formula post ;
\schemaVar \modalOperator { diamond , box , diamond_transaction , box_transaction } #allmodal;
\find ( \modality{#allmodal}{.. #loc = java.lang.Math.atan(#se); ...}\endmodality ( post ))
\replacewith ( { #loc:= atanDouble ( #se)} \modality{#allmodal}{.. ...}\endmodality ( post ))
\heuristics (simplify_prog )
};defined in: floatRulesAssumeStrictfp.key Line: 154 Offset :4