Skip to content

Enable Lizard with the latest Viper IDE / ViperServer #1

@aterga

Description

@aterga

Since Viper IDE started using a new language server implementation, this extension cannot be used anymore.

This ticket would cover re-enabling Lizard with the latest Viper tool releases.

In the meantime, one can still get Lizard to work with Viper IDE v3.0.1 and https://github.com/viperproject/viper-ide/releases/tag/21.07-RC3 and the following verification backend spec in settings.json:

(note the following arguments: --disableCaching, --counterexample native, --enableMoreCompleteExhale)

"viperSettings.verificationBackends": [
        {
            "v": "674a514867b1",
            "name": "silicon-debug",
            "type": "silicon",
            "paths": [],
            "engine": "ViperServer",
            "timeout": 100000,
            "stages": [
                {
                    "name": "verify",
                    "isVerification": true,
                    "mainMethod": "viper.silicon.SiliconRunner",
                    "customArguments": "--z3Exe /usr/local/bin/z3 --disableCaching --counterexample native --enableMoreCompleteExhale $fileToVerify$"
                }
            ],
            "stoppingTimeout": 5000
        },
]

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions