Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

unexpected Viper error: PredicateInstanceNoAccess #828

Open
gottschali opened this issue Jan 27, 2025 · 0 comments
Open

unexpected Viper error: PredicateInstanceNoAccess #828

gottschali opened this issue Jan 27, 2025 · 0 comments

Comments

@gottschali
Copy link

Gobra reports an unexpected Viper error for the following Gobra program:

package issue

type List struct {
	next *List
	Value int
}

pred elems(l *List) {
    l != nil ==> (acc(l) && elems(l.next))
}

requires elems(l)
decreases
func foo(l *List) {
    // invariant elems(l)
    decreases elems(l)
    for l != nil {
        unfold elems(l)
        l = l.next
    }
}

Error:

13:14:39.481 [ForkJoinPool-3-worker-1] ERROR viper.gobra.reporting.FileWriterReporter - Error at: <pred_term.gobra:16:15> 
Encountered an unexpected Viper error. This is a bug. The following information is for debugging purposes:
  Accessing predicate instance might fail. There might be insufficient permission to access elems_92443cc4_F(l_V0_CN0) ([email protected])

    error is PredicateInstanceNoAccess
    error offending node = PI_elems_92443cc4_F(l_V0_CN0)
    error offending node src = Some(Info(decreases  elems(l) ,elems_92443cc4_F(l_V0_CN0),Origin([email protected],elems(l)),Vector()))
    reason is InsufficientPermission
    reason offending node = elems_92443cc4_F(l_V0_CN0)
    reason offending node src = None
        . 
    . 
@gottschali gottschali changed the title unexpected Viper error: PredicateInstanceNoAccess unexpected Viper error: PredicateInstanceNoAccess Jan 27, 2025
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

No branches or pull requests

1 participant