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

[PVS-Help] Error: No Method Applicable for Generic Function


This seems like a PVS bug, since I saw many other instances of the same 
error on the bug list. I have encountered the same error many times but I 
have somehow found a solution to it until now.

My problem is the following. In a nutshell my theory looks something like 

theory1: THEORY


   lib: LIBRARY = "foo/"
   IMPORTING lib@theory2, theory3

END theory1

Now theory2 that is located in the directory "foo" looks something like this

theory2: THEORY

  IMPORTING theory2a


END theory2

I can successfully typecheck theory2 independently. When I create a dmp file 
, all the dependencies are also included. In short, everything works out 

However, when I import theory2 into theory1 I get the error that is 
mentioned in the subject line. Also I notice that the dmp file for theory 1 
does not include its dependencies (i.e. theory 2 etc.) even though during 
the typechecking of theory1, the bin files of the import chain are located 

As a result I cannot even send the complete dmp file of theory1. Any 
suggestions will be greatly appreciated.

Thank you in advance