[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] pvs 4.2 error: no methods applicable for generic function



Hi,

I was looking around in the pvs site (bugs list, suggestions list...) to find out a solution for my problem.
I didn't find. But I found this conversation below and I see that Jim was with the same problem as me.

The problem (A) - error: no methods applicable for generic function

With me, this occur with the pvs 4.2, when I am tcp my specs, or when I am doing a proof, after any command.
Sometimes I stay a week, maybe two, without annoying me with this problem, but suddenly it appears again.

When it occurs the pvs just crashes and the only way that I found to continue working is close the pvs (in fact, kill the pvs)
go to the context where I was working, delete .pvscontext and /pvsbin, and then start again.


Did you find how to fix Jim's problem?
Did you have an idea how to fix my problem?

Thanks in advance,
Andréia.


************************************************************************

Hi Jim,

This is a bug in PVS - could you please send me your specs, so that we
can get this fixed?

Thanks,
Sam Owre

jim armstrong <armstrong.jm@xxxxxxxxx> wrote:


> Hi,
>
> Can anyone there tell me what the following errors are:
>
> A) error: no methods applicable for generic function
>
>
> B) break: repeated bindings in make-subtype-tcc-decl

>
>
>
> A occurs whilst "tcp" is running proofs of proof obligations, but I've had it
> occur in proofs
>
> done in previous versions of PVS that I have re-installed. It appears to be

> emitted by "grind".
>
> It looks like some sort of lisp error. Doing the proofs again step by step gets
> rid of it altogether.
>
>
>
> B is a total mystery to me: it occurs when type-checking. It is provoked by

> certain type declarations.
>
> You can comment bits out to discover which declarations. These declarations
> look fine (e.g. they parse ok),
>
> but they are always dependent-type declarations where certain fields are

> function types.
>
>
> I re-jigged one declaration that was causing B and simplifying things
> mysteriously got rid of it.
>
> But then when I declared a constant of said type, B returns when

> PVS type-checks that constant.
>
>
> B worries me the most, since either a declaration is type-correct or it isn't.
> It can raise tccs but I don't see how no
>
> tccs (provable or otherwise) can be defined for it.

>
>
> thanks in advance
>
>
> jim

************************************************************************************************************