Skip to content

Commit 900287f

Browse files
authored
Add Chopper convenience method that just selects a set of names to create a single program (#897)
1 parent ce12a0a commit 900287f

File tree

1 file changed

+14
-0
lines changed

1 file changed

+14
-0
lines changed

src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,20 @@ trait ChopperLike { this: ViperGraphs with Cut =>
7575
chopWithMetrics(choppee)(selection, bound, penalty)._1
7676
}
7777

78+
/**
79+
* chops `choppee` into a single Viper program containing only the selected members. See [[chop]] for more details.
80+
*
81+
* @param choppee Targeted program.
82+
* @param selection Specifies the names of all members that should be verified.
83+
* @return Chopped program, if anything was selected.
84+
*/
85+
def chop(
86+
choppee: ast.Program,
87+
selection: Set[String],
88+
): Option[ast.Program] = {
89+
chopWithMetrics(choppee)(Some(m => selection.contains(m.name)))._1.headOption
90+
}
91+
7892
/**
7993
* chops `choppee` into multiple Viper programs and returns metrics. See [[chop]] for more details.
8094
*

0 commit comments

Comments
 (0)