Skip to content

SilFrontend API for Viper frontend usage#732

Merged
marcoeilers merged 6 commits into
masterfrom
meilers_term_plugin_deactive_flag
Aug 17, 2023
Merged

SilFrontend API for Viper frontend usage#732
marcoeilers merged 6 commits into
masterfrom
meilers_term_plugin_deactive_flag

Conversation

@marcoeilers

@marcoeilers marcoeilers commented Aug 14, 2023

Copy link
Copy Markdown
Contributor
  • Offers a new trait with two methods for easy usage of SilFrontend by actual Viper frontends. Compared to working with Verifier instances directly, these take care of plugins (i.e., they run the relevant plugin phases automatically; command line arguments can be used to select which plugins to run) and don't require calling a bunch of boilerplate methods. Compared to existing SilFrontend classes, these are made to be used by frontends (without parsing etc.) and correctly pass command line options to plugins.
  • Usage is simple:
    val f = new SiliconFrontendAPI(reporter)  // or CarbonFrontendAPI, or MinimalSiliconFrontendAPI (skips consistency checks)
    f.initialize(args) // command line arguments without any dummy filename
    val res1 = f.verify(program1)
    val res2 = f.verify(program2)
    f.stop()
    
  • Re-added option to disable default plugins.

Tested with adapted versions of Prusti and Nagini.

@marcoeilers marcoeilers requested a review from vakaras August 17, 2023 15:04

@vakaras vakaras left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. Thanks!

@marcoeilers marcoeilers merged commit 8bd26f5 into master Aug 17, 2023
@marcoeilers marcoeilers deleted the meilers_term_plugin_deactive_flag branch August 17, 2023 15:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants