Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

SilFrontend API for Viper frontend usage #732

Merged
merged 6 commits into from
Aug 17, 2023

Conversation

marcoeilers
Copy link
Contributor

@marcoeilers marcoeilers commented Aug 14, 2023

  • 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
Copy link
Contributor

@vakaras vakaras left a comment

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