Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 865


Synopsis:        TAB i prompt fails
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Fri Nov 12 12:00:00 2004
Originator:      "Ricky W. Butler"
Organization:    larc.nasa.gov
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
      The TAB i command has not been working right since I upgraded
  to Redhat 9.  I have isolated the problem to the
  concat function call in "pvs-soriorq-internal" located in
  the emacs/emacs-src/pvs-prover-helps.el file.  Apparently
  concat can no longer accept a numeric argument so
  
      (concat which " " prompt " " count
  
  crashes on "count".  If you make it (number-to-string count)
  things seem to work again.   Here is my full repair of the defun:
  
  
  (defun pvs-soriorq-internal (which prompt num paren)
     "Internal function to insert a skolem or inst command."
     (let* ((count 1)
  	(arglist "")
  	(nextarg (read-from-minibuffer (concat which " " prompt " " 
  (number-to-string count)
  						" [CR to quit]: ")
  					"")))
       (while (not (string= nextarg ""))
         (setq count (1+ count))
         (setq arglist (concat arglist "\"" nextarg "\" "))
         (setq nextarg (read-from-minibuffer (concat which " " prompt " " 
  (number-to-string count)
  						  " [CR to quit]: ")
  					  "")))
       (if (string= arglist "")
  	(insert (concat "(" which "! " num ")"))
  	(insert (concat "(" which " " num
  			(if paren " ("  " ")
  			arglist
  			(if paren "))" ")")
  			)))))
  

How-To-Repeat: 

Fix: 
Fixed as described.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools