Skip to content

Add support for indexing strings#961

Merged
jcp19 merged 2 commits intomasterfrom
string-indexing
Aug 27, 2025
Merged

Add support for indexing strings#961
jcp19 merged 2 commits intomasterfrom
string-indexing

Conversation

@jcp19
Copy link
Copy Markdown
Contributor

@jcp19 jcp19 commented Aug 17, 2025

This PR:

At the moment, violating the precondition of an indexing operation (i.e., passing an invalid index to a string) leads to a bad error message, similar to precondition of unknown may not hold. This is similar to other parts of our encoding, where we are not able to generate good error messages when the precondition of a function internal to our encoding may not hold. PR viperproject/silver#815 will hopefully allow us to fix that by attaching an error message to the precondition directly in the encoding.

Comment thread src/main/scala/viper/gobra/translator/encodings/StringEncoding.scala Outdated
Copy link
Copy Markdown
Member

@ArquintL ArquintL left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@jcp19 jcp19 merged commit 3900029 into master Aug 27, 2025
3 of 4 checks passed
@jcp19 jcp19 deleted the string-indexing branch August 27, 2025 09:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Low sensitivity doesn't transfer when converting string to []byte

2 participants