Added missing case (fixes Silicon issue #742)

marcoeilers · marcoeilers · commit bfdf70b13df6 · 2023-08-14T19:05:38.000+02:00
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -140,6 +140,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
         case PMapType(_, _) => Seq("Map")
         case PDomainType(d, _) if d.name == "PredicateInstance" => Seq("PredicateInstances")
         case PDomainType(d, _) => Seq(d.name)
+        case gt: PGenericType => Seq(gt.genericName)
       }
       !typeNames.exists(tn => wfTypeName.contains(tn))
     }

Original file line number	Diff line number	Diff line change
`@@ -140,6 +140,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,`
`140`	`140`	`case PMapType(_, _) => Seq("Map")`
`141`	`141`	`case PDomainType(d, _) if d.name == "PredicateInstance" => Seq("PredicateInstances")`
`142`	`142`	`case PDomainType(d, _) => Seq(d.name)`
	`143`	`+ case gt: PGenericType => Seq(gt.genericName)`
`143`	`144`	`}`
`144`	`145`	`!typeNames.exists(tn => wfTypeName.contains(tn))`
`145`	`146`	`}`