Make sequence axiomatisation common with Carbon

[viper-admin]

Created by @alexanderjsummers on 2014-07-14 12:34 Last updated on 2020-02-03 13:32

We should find a way to make the two verifiers use the same file for sequence, set axioms etc. to avoid diverging fixes. Feature request also filed for Carbon (https://github.com/viperproject/silicon/issues/295). Probably the best way is to ~~have a .bpl file and then read it for Carbon and convert it for Silicon.~~ source the axioms from Viper files.

Moreover, the sequence, set, multiset axioms have implicit preconditions on certain operations (e.g., drop from a sequence is only axiomatised in the case in which the index is non-negative). We should either make the axioms more permissive, or add well-definedness checks which ensure that these conditions hold at use-site. These checks should be made consistently in both Silicon and Carbon.

[viper-admin]

@mschwerhoff commented on 2019-12-24 10:31

See also https://github.com/viperproject/silicon/issues/129.

‌

[viper-admin]

@mschwerhoff on 2019-12-24 10:31:

• edited the title
• edited the description

[viper-admin]

@fabiopakk on 2020-02-03 13:32:

• edited the description

[mschwerhoff]

Updates:

• As of 7175ff5, Silicon sources its set, multiset and sequence axioms from Viper files
• As of 59f89af, Silicon provides command-line options for overriding the axiomatisations it uses. See also https://github.com/viperproject/silicon/issues/405#issuecomment-596196263.