@@ -362,6 +362,12 @@ module Make<
362362 v .asConstantValue ( ) = c .asConstantValue ( )
363363 }
364364
365+ private predicate trivialHasValue ( Expr e , GuardValue v ) {
366+ constantHasValue ( e , v )
367+ or
368+ e instanceof NonNullExpr and v .isNonNullValue ( )
369+ }
370+
365371 /** Holds if `t` is an exception-like successor type. */
366372 private predicate exceptionLike ( SuccessorType t ) {
367373 t instanceof ExceptionSuccessor or
@@ -822,7 +828,7 @@ module Make<
822828 v2 .isNonNullValue ( )
823829 )
824830 ) and
825- not exprHasValue ( g2 , v2 ) // disregard trivial guard
831+ not trivialHasValue ( g2 , v2 ) // disregard trivial guard
826832 }
827833
828834 bindingset [ g1, v1]
@@ -845,7 +851,7 @@ module Make<
845851 // g1 === ... ? e : g2
846852 g2 = getBranchExpr ( cond , branch .booleanNot ( ) ) and
847853 v2 = v1 and
848- not exprHasValue ( g2 , v2 ) // disregard trivial guard
854+ not trivialHasValue ( g2 , v2 ) // disregard trivial guard
849855 )
850856 }
851857
@@ -854,7 +860,7 @@ module Make<
854860 private predicate impliesStepSsaGuard ( SsaDefinition def1 , GuardValue v1 , Guard g2 , GuardValue v2 ) {
855861 def1 .( SsaExplicitWrite ) .getValue ( ) = g2 and
856862 v1 = v2 and
857- not exprHasValue ( g2 , v2 ) // disregard trivial guard
863+ not trivialHasValue ( g2 , v2 ) // disregard trivial guard
858864 or
859865 exists ( Expr e , GuardValue ev |
860866 guardDeterminesPhiInput ( g2 , v2 .getDualValue ( ) , def1 , e ) and
@@ -1104,7 +1110,7 @@ module Make<
11041110 call .getMethod ( ) = wrapperGuard ( ppos , v1 , v2 ) and
11051111 call .getArgument ( apos ) = g2 and
11061112 parameterMatch ( pragma [ only_bind_out ] ( ppos ) , pragma [ only_bind_out ] ( apos ) ) and
1107- not exprHasValue ( g2 , v2 ) // disregard trivial guard
1113+ not trivialHasValue ( g2 , v2 ) // disregard trivial guard
11081114 )
11091115 }
11101116 }
0 commit comments