The pvs lisp command 'find-declaration' reports wrong declaration range when the command is executed after 'show-declaration'.
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. Save the following theories in test.pvs
lib: THEORY
BEGIN
T3: TYPE
END lib
findme: THEORY
BEGIN IMPORTING lib
t3: T3
END findme
Step 2. After typechecking, type the following commands in the *pvs* buffer:
(find-declaration "T3")
(show-declaration "test" "pvs" '(11 7))
(find-declaration "T3")
Description of the bug
The pvs lisp command 'find-declaration' reports wrong declaration range when the command is executed after 'show-declaration'.
PVS versions
Steps for reproducing the bug
Step 1. Save the following theories in test.pvs
Step 2. After typechecking, type the following commands in the *pvs* buffer: (find-declaration "T3") (show-declaration "test" "pvs" '(11 7)) (find-declaration "T3")
Output on PVS7 and PVS6
pvs(1): (find-declaration "T3") (("T3 type function_props_alt " "T3" "function_props_alt" nil (1505 32 1505 36) "T3: TYPE") ("T3 type relation_props2 " "T3" "relation_props2" nil (1617 33 1617 37) "T3: TYPE") ("T3 type function_props " "T3" "function_props" nil (1463 28 1463 32) "T3: TYPE") ("T3 type transpose " "T3" "transpose" nil (303 22 303 26) "T3: TYPE") ("T3 type relation_props " "T3" "relation_props" nil (1594 28 1594 32) "T3: TYPE") ("T3 type map_props " "T3" "map_props" nil (4816 23 4816 27) "T3: TYPE") ("T3 type function_props2 " "T3" "function_props2" nil (1526 33 1526 37) "T3: TYPE") ("T3 type lib " "T3" "lib" "test" (4 2 4 10) "T3: TYPE")) pvs(2): (show-declaration "test" "pvs" '(11 7)) % From theory lib: T3: TYPE nil pvs(3): (find-declaration "T3") (("T3 type function_props_alt " "T3" "function_props_alt" nil (1505 32 1505 36) "T3: TYPE") ("T3 type relation_props2 " "T3" "relation_props2" nil (1617 33 1617 37) "T3: TYPE") ("T3 type function_props " "T3" "function_props" nil (1463 28 1463 32) "T3: TYPE") ("T3 type transpose " "T3" "transpose" nil (303 22 303 26) "T3: TYPE") ("T3 type relation_props " "T3" "relation_props" nil (1594 28 1594 32) "T3: TYPE") ("T3 type map_props " "T3" "map_props" nil (4816 23 4816 27) "T3: TYPE") ("T3 type function_props2 " "T3" "function_props2" nil (1526 33 1526 37) "T3: TYPE") ("T3 type lib " "T3" "lib" "test" (2 0 2 8) "T3: TYPE"))