@@ -25,8 +25,7 @@ private module Cached {
2525 newtype TSplitKind =
2626 TInitializerSplitKind ( ) or
2727 TConditionalCompletionSplitKind ( ) or
28- TAssertionSplitKind ( ) or
29- TExceptionHandlerSplitKind ( )
28+ TAssertionSplitKind ( )
3029
3130 cached
3231 newtype TSplit =
@@ -35,8 +34,7 @@ private module Cached {
3534 TAssertionSplit ( AssertionSplitting:: Assertion a , int i , boolean success ) {
3635 exists ( a .getExpr ( i ) ) and
3736 success in [ false , true ]
38- } or
39- TExceptionHandlerSplit ( ExceptionClass ec )
37+ }
4038}
4139
4240import Cached
@@ -449,179 +447,3 @@ module AssertionSplitting {
449447 }
450448 }
451449}
452-
453- module ExceptionHandlerSplitting {
454- private newtype TMatch =
455- TAlways ( ) or
456- TMaybe ( ) or
457- TNever ( )
458-
459- /**
460- * A split for elements belonging to a `catch` clause, which determines the type of
461- * exception to handle. For example, in
462- *
463- * ```csharp
464- * try
465- * {
466- * if (M() > 0)
467- * throw new ArgumentException();
468- * else if (M() < 0)
469- * throw new ArithmeticException("negative");
470- * else
471- * return;
472- * }
473- * catch (ArgumentException e)
474- * {
475- * Log.Write("M() positive");
476- * }
477- * catch (ArithmeticException e) when (e.Message != null)
478- * {
479- * Log.Write($"M() {e.Message}");
480- * }
481- * ```
482- *
483- * all control flow nodes in
484- * ```csharp
485- * catch (ArgumentException e)
486- * ```
487- * and
488- * ```csharp
489- * catch (ArithmeticException e) when (e.Message != null)
490- * ```
491- * have two splits: one representing the `try` block throwing an `ArgumentException`,
492- * and one representing the `try` block throwing an `ArithmeticException`.
493- */
494- class ExceptionHandlerSplit extends Split , TExceptionHandlerSplit {
495- private ExceptionClass ec ;
496-
497- ExceptionHandlerSplit ( ) { this = TExceptionHandlerSplit ( ec ) }
498-
499- /** Gets the exception type that this split represents. */
500- ExceptionClass getExceptionClass ( ) { result = ec }
501-
502- override string toString ( ) { result = "exception: " + ec .toString ( ) }
503- }
504-
505- private class ExceptionHandlerSplitKind extends SplitKind , TExceptionHandlerSplitKind {
506- override int getListOrder ( ) { result = AssertionSplitting:: getNextListOrder ( ) }
507-
508- override string toString ( ) { result = "ExceptionHandler" }
509- }
510-
511- int getNextListOrder ( ) { result = AssertionSplitting:: getNextListOrder ( ) + 1 }
512-
513- private class ExceptionHandlerSplitImpl extends SplitImpl instanceof ExceptionHandlerSplit {
514- override ExceptionHandlerSplitKind getKind ( ) { any ( ) }
515-
516- override predicate hasEntry ( AstNode pred , AstNode succ , Completion c ) {
517- // Entry into first catch clause
518- exists ( Statements:: TryStmtTree ts |
519- super .getExceptionClass ( ) = ts .getAThrownException ( pred , c )
520- |
521- succ ( pred , succ , c ) and
522- succ = ts .( TryStmt ) .getCatchClause ( 0 ) .( SpecificCatchClause )
523- )
524- }
525-
526- override predicate hasEntryScope ( CfgScope scope , AstNode first ) { none ( ) }
527-
528- /**
529- * Holds if this split applies to catch clause `scc`. The parameter `match`
530- * indicates whether the catch clause `scc` may match the exception type of
531- * this split.
532- */
533- private predicate appliesToCatchClause ( SpecificCatchClause scc , TMatch match ) {
534- exists ( Statements:: TryStmtTree ts , ExceptionClass ec |
535- ec = super .getExceptionClass ( ) and
536- ec = ts .getAThrownException ( _, _) and
537- scc = ts .( TryStmt ) .getACatchClause ( )
538- |
539- if scc .getCaughtExceptionType ( ) = ec .getABaseType * ( )
540- then match = TAlways ( )
541- else
542- if scc .getCaughtExceptionType ( ) = ec .getASubType + ( )
543- then match = TMaybe ( )
544- else match = TNever ( )
545- )
546- }
547-
548- /**
549- * Holds if this split applies to control flow element `pred`, where `pred`
550- * is a valid predecessor with completion `c`.
551- */
552- private predicate appliesToPredecessor ( AstNode pred , Completion c ) {
553- this .appliesTo ( pred ) and
554- ( succ ( pred , _, c ) or scopeLast ( _, pred , c ) ) and
555- (
556- pred instanceof SpecificCatchClause
557- implies
558- pred =
559- any ( SpecificCatchClause scc |
560- if c instanceof MatchingCompletion
561- then
562- exists ( TMatch match | this .appliesToCatchClause ( scc , match ) |
563- c =
564- any ( MatchingCompletion mc |
565- if mc .isMatch ( ) then match != TNever ( ) else match != TAlways ( )
566- )
567- )
568- else (
569- ( scc .isLast ( ) and c instanceof ThrowCompletion )
570- implies
571- exists ( TMatch match | this .appliesToCatchClause ( scc , match ) | match != TAlways ( ) )
572- )
573- )
574- )
575- }
576-
577- /**
578- * Holds if this split applies to `pred`, and `pred` may exit this split
579- * with throw completion `c`, because it belongs to the last `catch` clause
580- * in a `try` statement.
581- */
582- private predicate hasLastExit ( AstNode pred , ThrowCompletion c ) {
583- this .appliesToPredecessor ( pred , c ) and
584- exists ( TryStmt ts , SpecificCatchClause scc , int last |
585- last ( ts .getCatchClause ( last ) , pred , c )
586- |
587- ts .getCatchClause ( last ) = scc and
588- scc .isLast ( ) and
589- c .getExceptionClass ( ) = super .getExceptionClass ( )
590- )
591- }
592-
593- override predicate hasExit ( AstNode pred , AstNode succ , Completion c ) {
594- this .appliesToPredecessor ( pred , c ) and
595- succ ( pred , succ , c ) and
596- (
597- // Exit out to `catch` clause block
598- first ( any ( SpecificCatchClause scc ) .getBlock ( ) , succ )
599- or
600- // Exit out to a general `catch` clause
601- succ instanceof GeneralCatchClause
602- or
603- // Exit out from last `catch` clause (no catch clauses match)
604- this .hasLastExit ( pred , c )
605- )
606- }
607-
608- override predicate hasExitScope ( CfgScope scope , AstNode last , Completion c ) {
609- // Exit out from last `catch` clause (no catch clauses match)
610- this .hasLastExit ( last , c ) and
611- scopeLast ( scope , last , c )
612- }
613-
614- override predicate hasSuccessor ( AstNode pred , AstNode succ , Completion c ) {
615- this .appliesToPredecessor ( pred , c ) and
616- this .appliesSucc ( pred , succ , c ) and
617- not first ( any ( SpecificCatchClause scc ) .getBlock ( ) , succ ) and
618- not succ instanceof GeneralCatchClause and
619- not exists ( TryStmt ts , SpecificCatchClause scc , int last |
620- last ( ts .getCatchClause ( last ) , pred , c )
621- |
622- ts .getCatchClause ( last ) = scc and
623- scc .isLast ( )
624- )
625- }
626- }
627- }
0 commit comments