Settings: Verification Backends

Settings: Verification Backends

This block contains a list of verification backend specifications. By default the backends silicon and carbon are specified.

• name: The name of the backend. Use silicon or carbon for overwriting the default backends.
• type: The type of the backend: use either silicon or carbon
• paths: a list of all jar-dependencies.
• timeout: After timeout milliseconds the verification is expected to yield no useful result and is terminated.
• engine: The engine to run the backend with: use ViperServer
• stages: A list of stages represent the individual steps involved in the verification.
  • name: the name of the stage
  • isVerification: Is this stage a verification stage or something else? (e.g. a inference stage)
  • mainMethod: the main method to invoke when starting the stage.
  • customArguments: additional command line arguments for starting the stage process
  • onParsingError: the name of the follow-up stage in case of a parsing error
  • onTypeCheckingError: the name of the follow-up stage in case of a type checking error
  • onVerificationError: the name of the follow-up stage in case of a verification error
  • onSuccess: The name of the stage to start in case of a success
  • stoppingTimeout: After timeout milliseconds the viperServer is expeted to have terminated

Default Settings:

"viperSettings.verificationBackends": [
  {
    "v": "674a514867b1",
    "name": "silicon",
    "type": "silicon",
    "paths": [],
    "engine": "ViperServer",
    "timeout": 100000,
    "stages": [
      {
        "name": "verify",
        "isVerification": true,
        "mainMethod": "viper.silicon.SiliconRunner",
        "customArguments": "--z3Exe $z3Exe$ $disableCaching$ $fileToVerify$"
      }
    ],
    "stoppingTimeout": 5000
  },
  {
    "v": "674a514867b1",
    "name": "carbon",
    "type": "carbon",
    "paths": [],
    "engine": "ViperServer",
    "timeout": 100000,
    "stages": [
      {
        "name": "verify",
        "isVerification": true,
        "mainMethod": "viper.carbon.Carbon",
        "customArguments": "--z3Exe $z3Exe$ --boogieExe $boogieExe$ $disableCaching$ $fileToVerify$"
      }
    ],
    "stoppingTimeout": 5000
  }
]