inconsistent behavior of 'show-declaration' and 'find-declaration' when used on function arguments - Githubissues

SRI-CSL / PVS

The People's Verification System

http://pvs.csl.sri.com

GNU General Public License v2.0

135 stars 32 forks source link

inconsistent behavior of 'show-declaration' and 'find-declaration' when used on function arguments #59

Closed pmasci closed 3 years ago

pmasci commented 5 years ago

Description of the problem

The pvs lisp command 'find-declaration' is unable to find the declaration of function arguments, while 'show-declaration' finds it.

PVS versions

PVS Version 6.0 - International Allegro CL Enterprise Edition 9.0 [64-bit Linux (x86-64)] (Jan 14, 2013 3:07) - International Allegro CL Enterprise Edition 9.0 [64-bit Linux (x86-64)]
PVS Version 7.0 - International Allegro CL Enterprise Edition 10.1 [64-bit Linux (x86-64) SMP]

Steps for reproducing the bug

Step 1. Create the following theory

foo_th: THEORY
 BEGIN
   f(x: int): int
   g(ww: int): int = f(ww)
 END foo_th

Step 2. After typechecking, type the following commands in the *pvs* buffer (show-declaration "test" "pvs" '(4 24)) (find-declaration "ww")

Output on PVS7 and PVS6

pvs(1): (show-declaration "test" "pvs" '(4 24)) % From theory findme: ww: int nil pvs(2): (find-declaration "ww") nil