Outputs differ between Silicon and Carbon

[viper-admin]

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:

• FollyRWSpinlock_err_mod.sil

However, different reasons are given:

• Carbon: insufficient permission
• Silicon: Assertion false might not hold

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]

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

• edited the title

[viper-admin]

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

• edited the title