Renaming proverArgs annotation and cleaning up annotation handling

[marcoeilers]

This PR

• renames the annotation currently called proverArgs, (i.e. for example @proverArgs("smt.arith.solver=6")) to proverConfigArgs (i.e. for example @proverConfigArgs("smt.arith.solver=6")). This change makes the annotation's name consistent with the corresponding command line option --proverConfigArgs, which serves the same function, and fixes an accidental name clash with the --proverArgs command line option which also exists but does something different (it passes command line options to Z3).
• enables the proverConfigArgs annotation also for function verification (it previously only worked for methods)
• moves all annotation handling code from various places in the code that sometimes duplicated functionality to a single new AnnotationSupporter.

These changes address two problems raised in issue #931.

[Copilot]

Pull Request Overview

This PR renames the proverArgs annotation to proverConfigArgs, centralizes annotation handling in a new AnnotationSupporter, and extends proverConfigArgs support to function verification.

• Renamed and unified annotation parsing for prover configuration flags
• Refactored exhale, join, and state consolidation annotation logic into AnnotationSupporter
• Enabled and reset prover configuration options in function verification units

Reviewed Changes

Copilot reviewed 8 out of 8 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
src/main/scala/verifier/DefaultMainVerifier.scala	Switched to AnnotationSupporter for exhale and join mode annotations; updated proverConfigArgs printing
src/main/scala/verifier/BaseVerifier.scala	Replaced inline stateConsolidationMode parsing with AnnotationSupporter call
src/main/scala/supporters/functions/FunctionVerificationUnit.scala	Added function-level proverConfigArgs support and reset logic
src/main/scala/supporters/MethodSupporter.scala	Replaced ad-hoc proverArgs parsing with AnnotationSupporter.getProverConfigArgs
src/main/scala/supporters/AnnotationSupporter.scala	New helper for all annotation parsing and warning reporting
src/main/scala/rules/ExecutionFlowController.scala	Replaced inline exhaleMode parsing with AnnotationSupporter.getExhaleMode
src/main/scala/rules/Brancher.scala	Renamed brancher variables from proverArgs to proverConfigArgs
silver	Updated submodule commit

Comments suppressed due to low confidence (3)

src/main/scala/supporters/AnnotationSupporter.scala:22

• [nitpick] Add Scaladoc comments to this method (and the others in AnnotationSupporter) to explain its purpose, parameters, return value, and side effects (warnings).

  def getProverConfigArgs(member: ast.Member, reporter: Reporter): Map[String, String] = {

src/main/scala/verifier/DefaultMainVerifier.scala:324

• [nitpick] The variable name mce is not immediately clear to readers. Consider renaming to something like moreCompleteExhaleEnabled or shouldUseMoreCompleteExhale for clarity.

    val mce = AnnotationSupporter.getExhaleMode(member, reporter) match {

src/main/scala/supporters/functions/FunctionVerificationUnit.scala:153

• New handling of @proverConfigArgs for functions is introduced here; consider adding unit or integration tests to verify that function-level annotations are correctly parsed and applied.

      val proverOptions: Map[String, String] = AnnotationSupporter.getProverConfigArgs(function, reporter)