poolKeyIsContentOfValue {
\schemaVar \term Seq slit ;
\find ( strContent ( strPool ( slit ) ) )
\replacewith ( slit )
\heuristics (simplify )
};defined in: String.key Line: 6 Offset :2poolIsInjective {
\schemaVar \term Seq slit1 , slit2 ;
\find ( strPool ( slit1 ) = strPool ( slit2 ) )
\replacewith ( slit1 = slit2 )
\heuristics (simplify )
};defined in: String.key Line: 14 Offset :2insert_constant_string_value {
\schemaVar \program ConstantStringVariable #csv ;
\assumes ( wellFormed ( heap ) ==> )
\find ( #csv )
\replacewith ( \if ( #constantvalue ( #csv ) = null ) \then ( null ) \else ( strPool ( ( Seq ) #constantvalue ( #csv ) ) ) ) \add ( #constantvalue ( #csv ) = null | ( strPool ( ( Seq ) #constantvalue ( #csv ) ) != null & select <[ boolean ]> ( heap , strPool ( ( Seq ) #constantvalue ( #csv ) ) , java.lang.Object #$created ) = TRUE ) ==> )
\heuristics (concrete )
};defined in: String.key Line: 22 Offset :2nullString {
\find ( strContent ( null ) )
\replacewith ( "null" )
\heuristics (concrete )
};defined in: String.key Line: 34 Offset :2stringAssignment {
\schemaVar \modalOperator { diamond , box } #normalassign ;
\schemaVar \program Variable #v ;
\schemaVar \program StringLiteral #slit ;
\schemaVar \formula post ;
\find ( \modality{#normalassign}{.. #v = #slit; ...}\endmodality ( post ) )
\replacewith ( { #v := strPool ( #slit ) } \modality{#normalassign}{.. ...}\endmodality ( post ) ) \add ( strPool ( #slit ) != null , select <[ boolean ]> ( heap , strPool ( #slit ) , java.lang.Object #$created ) = TRUE ==> )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 44 Offset :2stringConcat {
\schemaVar \modalOperator { diamond , box } #normalassign ;
\schemaVar \program Variable #v ;
\schemaVar \program SimpleStringExpression #sstr1 , #sstr2 ;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign} {..
#v = #sstr1 + #sstr2;
...}\endmodality ( post ) )
\varcond \replacewith ( { #v := sk } { heap := create ( heap , sk ) } \modality{#normalassign}{.. ...}\endmodality ( post ) ) \add ( strContent ( sk ) = seqConcat ( strContent ( #sstr1 ) , strContent ( #sstr2 ) ) ==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 63 Offset :2stringConcatIntExpLeft {
\schemaVar \modalOperator { diamond , box } #normalassign ;
\schemaVar \program Variable #v ;
\schemaVar \program SimpleStringExpression #sstrRight ;
\schemaVar \program AnyJavaTypeExpression #seLeft ;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign}
{.. #v = #seLeft + #sstrRight; ...}
\endmodality ( post ) )
\varcond \replacewith ( { #v := sk } { heap := create ( heap , sk ) } \modality{#normalassign}{.. ...}\endmodality ( post ) ) \add ( strContent ( sk ) = seqConcat ( clTranslateInt ( #seLeft ) , strContent ( #sstrRight ) ) ==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 83 Offset :2stringConcatIntExpRight {
\schemaVar \modalOperator { diamond , box } #normalassign ;
\schemaVar \program Variable #v ;
\schemaVar \program SimpleStringExpression #sstrLeft ;
\schemaVar \program AnyJavaTypeExpression #seRight ;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign}
{.. #v = #sstrLeft + #seRight; ...}
\endmodality ( post ) )
\varcond \replacewith ( { #v := sk } { heap := create ( heap , sk ) } \modality{#normalassign}{.. ...}\endmodality ( post ) ) \add ( strContent ( sk ) = seqConcat ( strContent ( #sstrLeft ) , clTranslateInt ( #seRight ) ) ==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 104 Offset :2stringConcatCharExpLeft {
\schemaVar \modalOperator { diamond , box } #normalassign ;
\schemaVar \program Variable #v ;
\schemaVar \program SimpleStringExpression #sstrRight ;
\schemaVar \program JavaCharExpression #seLeft ;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign}
{.. #v = #seLeft + #sstrRight; ...}
\endmodality ( post ) )
\varcond \replacewith ( { #v := sk } { heap := create ( heap , sk ) } \modality{#normalassign}{.. ...}\endmodality ( post ) ) \add ( strContent ( sk ) = seqConcat ( seqSingleton ( #seLeft ) , strContent ( #sstrRight ) ) ==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 124 Offset :2stringConcatCharExpRight {
\schemaVar \modalOperator { diamond , box } #normalassign ;
\schemaVar \program Variable #v ;
\schemaVar \program SimpleStringExpression #sstrLeft ;
\schemaVar \program JavaCharExpression #seRight ;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign}
{.. #v = #sstrLeft + #seRight; ...}
\endmodality ( post ) )
\varcond \replacewith ( { #v := sk } { heap := create ( heap , sk ) } \modality{#normalassign}{.. ...}\endmodality ( post ) ) \add ( strContent ( sk ) = seqConcat ( strContent ( #sstrLeft ) , seqSingleton ( #seRight ) ) ==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 145 Offset :2stringConcatBooleanLeft {
\schemaVar \modalOperator { diamond , box } #normalassign ;
\schemaVar \program Variable #v ;
\schemaVar \program SimpleStringExpression #sstrRight ;
\schemaVar \program SimpleJavaBooleanExpression #seLeft ;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign}
{.. #v = #seLeft + #sstrRight; ...}
\endmodality ( post ) )
\varcond \replacewith ( { #v := sk } { heap := create ( heap , sk ) } \modality{#normalassign}{.. ...}\endmodality ( post ) ) \add ( strContent ( sk ) = seqConcat ( \if ( #seLeft = TRUE ) \then ( "true" ) \else ( "false" ) , strContent ( #sstrRight ) ) ==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 165 Offset :2stringConcatBooleanRight {
\schemaVar \modalOperator { diamond , box } #normalassign ;
\schemaVar \program Variable #v ;
\schemaVar \program SimpleStringExpression #sstrLeft ;
\schemaVar \program SimpleJavaBooleanExpression #seRight ;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign}
{.. #v = #sstrLeft + #seRight; ...}
\endmodality ( post ) )
\varcond \replacewith ( { #v := sk } { heap := create ( heap , sk ) } \modality{#normalassign}{.. ...}\endmodality ( post ) ) \add ( strContent ( sk ) = seqConcat ( strContent ( #sstrLeft ) , \if ( #seRight = TRUE ) \then ( "true" ) \else ( "false" ) ) ==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 189 Offset :2stringConcatObjectLeft {
\schemaVar \modalOperator { diamond , box } #normalassign ;
\schemaVar \program Variable #v ;
\schemaVar \program SimpleStringExpression #sstrRight ;
\schemaVar \program SimpleNonStringObjectExpression #seLeft ;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign}
{.. #v = #seLeft + #sstrRight; ...}
\endmodality ( post ) )
\varcond "#seLeft not null" : \replacewith ( \modality{#normalassign}
{.. #v = #seLeft.toString() + #sstrRight; ...}
\endmodality ( post ) ) \add ( ==> #seLeft = null ) ;
"#seLeft null" : \replacewith ( { #v := sk } { heap := create ( heap , sk ) } \modality{#normalassign}{.. ...}\endmodality ( post ) ) \add ( #seLeft = null , strContent ( sk ) = seqConcat ( strContent ( null ) , strContent ( #sstrRight ) ) ==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 213 Offset :2stringConcatObjectRight {
\schemaVar \modalOperator { diamond , box } #normalassign ;
\schemaVar \program Variable #v ;
\schemaVar \program SimpleStringExpression #sstrLeft ;
\schemaVar \program SimpleNonStringObjectExpression #seRight ;
\schemaVar \formula post ;
\schemaVar \skolemTerm java.lang.String sk ;
\find ( \modality{#normalassign}
{.. #v = #sstrLeft + #seRight; ...}
\endmodality ( post ) )
\varcond "#seRight not null" : \replacewith ( \modality{#normalassign}
{.. #v = #sstrLeft + #seRight.toString(); ...}
\endmodality ( post ) ) \add ( ==> #seRight = null ) ;
"#seRight null" : \replacewith ( { #v := sk } { heap := create ( heap , sk ) } \modality{#normalassign}{.. ...}\endmodality ( post ) ) \add ( #seRight = null , strContent ( sk ) = seqConcat ( strContent ( #sstrLeft ) , strContent ( null ) ) ==> sk = null )
\heuristics (simplify_prog , simplify_prog_subset )
};defined in: String.key Line: 243 Offset :2