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

PVS Bug 470


Synopsis:        bug in pvs-lisp-theory
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Jul 10 11:00:02 2000
Originator:      Jean-Christophe Filliatre
Organization:    csl.sri.com
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  
  Shankar, Sam,
  
  I've found  a bug  in the Lisp  ground evaluator,  while experimenting
  with the ML one. Here is a small theory to illustrate it:
  
  ======================================================================
  test: theory begin
  
    u : var [int,int]
  
    g(u) : int = u`1
  
    c : int = g(1,2)
  
  end test
  ======================================================================
  
  The error is 
  
      "Error: The lists of keys and data are of unequal length."
  
  Apparently,   it   comes  from   the   function  pvs2cl-operator2   in
  pvseval-update.lisp, when it tries to make an association list between
  formal ans actual arguments, lines 332-335:
  
  ======================================================================
  		       (pairlis
  			formals
  			(append actuals
  				arguments))
  ======================================================================
  
  In that case,  the formal arguments list has length  1, and the actual
  arguments list has length 2.
  
  I  don't see how  to fix  that, but  I'm interested  in the  patch, of
  course, for the ML extractor.
  
  Remark: everything is fine  with the non-destructive translation of c,
  which  is  the expected  one.  Only  the  destructive one  causes  the
  problem.
  
  -- 
  Jean-Christophe Filliatre    
    Computer Science Laboratory   Phone (650) 859-5173
    SRI International             FAX   (650) 859-2844
    333 Ravenswood Ave.           email filliatr@csl.sri.com
    Menlo Park, CA 94025, USA     web   http://www.csl.sri.com/~filliatr
  
    

How-To-Repeat: 

Fix: 

 [davesc]
 This is ok now, fixed as a side effect of other things.

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