viperproject
Make sequence axiomatisation common with Silicon
Created by @fabiopakk on 2020-02-03 13:30
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 Silicon (104). 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.
Updates on Silicon's side, see https://github.com/viperproject/silicon/issues/104#issuecomment-596196782
