Undeclared functions in invariants

[maditaP]

Using an undeclared function with declared parameters in an invariant results in an error about the parameters being undeclared:

Doing the same anywhere else in the code behaves as one would expect:

coproc test() -> ()
{
    var declared: Bool = true
    var x: Bool = undeclared(declared)
    @invariant(undeclared(declared))
    while true {
       x = true
    }
}

[umutdural]

I can't reproduce this in the main branch with the given example. For both of the following procs, I have the error on the undeclared (correctly) and it is thrown by the resolve phase and not tycheck.

coproc test() -> ()
{
    var declared: Bool = true
    @invariant(undeclared(declared))
    while true {
       x = true
    }
}

coproc test() -> ()
{
    var declared: Bool = true
    var x: Bool = undeclared(declared)
}

But I recall an old bug in the resolve phase that causes the resolver to skip some parameters of annotations, maybe this issue happens on an old commit before that is fixed?

[umutdural]

Interestingly this reproduces the error for me:

coproc test() -> ()
{
    var invariant: Bool = true
    var declared: Bool = true
    @invariant(undeclared(declared))
    while (true) {
    }

}

so I think this is related to the issue #101.

[maditaP]

Yes exactly. I'm sorry, for me the bug appeared on this (I forgot about having the function declaration above):

domain Invariants {
     func invariant(x: Bool) : EUReal = 0
}
coproc test() -> ()
{
    var declared: Bool = true
    @invariant(undeclared(declared))
    while true {
       declared = true
    }
}