search

viperproject / silicon

Symbolic-execution-based verifier for the Viper intermediate verification language.
Mozilla Public License 2.0
79 stars 31 forks source link

Outputs differ between Silicon and Carbon #366

Open viper-admin opened 5 years ago

viper-admin commented 5 years ago

Created by @fabiopakk on 2019-01-21 16:18 Last updated on 2019-01-21 16:28

In the file below, the same expected output is produced by both verifier backends, Exhale might fail. This file is in examples repository, in directory cav2017:

However, different reasons are given:

Either the verifiers could be improved to produce the same result or a better annotation could be created to accommodate such differences. The later could also be used to express the fact that Silicon halts after the first error that is encountered while Carbon reports them all.

viper-admin commented 5 years ago

@fabiopakk on 2019-01-21 16:20:

  • edited the title
viper-admin commented 5 years ago

@alexanderjsummers on 2019-01-21 16:28:

  • edited the title