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

PVS Bug 561


Synopsis:        prove-untried-pvs-file does not automatically typecheck
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed May  2 12:20:01 2001
Originator:      Sam Owre
Organization:    csl.sri.com
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Running the batch file
  
  ;;----batch.el----
  (pvs-message "Hello")
  (change-context "~/pvs-specs/test2.3")
  (let ((current-prefix-arg t))
   (prove-untried-pvs-file "test" "(grind$)") )
  
  where test.pvs exists in the specified context does nothing because the
  theory has not been typechecked.  Same for prove-untried-theory.
  
  Sam
  

How-To-Repeat: 

Fix: 
Fixed prove-untried-pvs-file and prove-untried-theory to typecheck the
file or theory.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools