Add well-definedness checks for built-in axiomatisations

[viper-admin]

Created by @alexanderjsummers on 2014-11-10 16:57
Last updated on 2020-02-03 13:35

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]

@alexanderjsummers commented on 2014-11-10 16:57

see also Silicon issue 129

[viper-admin]

@fabiopakk commented on 2020-02-03 13:24

This seems not to be affecting any longer the file: src/test/resources/all/sequences/sequences.vpr

The comment in line 60, prior to commit <https://github.com/viperproject/silver/commit/74b03d1259c76a1adda3f936ec4e7e793bd5719a> states “CLOSE ISSUE

I’ll therefore close this issue and file another issue in a similar way that issue 129 was superseded by 104 in Silicon.

[viper-admin]

@fabiopakk commented on 2020-02-03 13:31

Superseded by #295

[viper-admin]

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

• changed state from new to resolved

[viper-admin]

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

• changed the assignee from (none) to @fabiopakk

[alexanderjsummers]

If I understand correctly, we made the axioms more complete; we don't add well-definedness restrictions but instead have axioms which tell us something even when dropping too many elements, etc.