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

PVS Bug 361


Synopsis:        musimp problem
Severity:        serious
Priority:        medium
Responsible:     shankar (Natarajan Shankar)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Sep 13 02:20:03 1999
Originator:      Natarajan Shankar
Organization:    csl.sri.com
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  
  In ~shankar/conferences/FM99/tutorial/mupigeon.pvs,
  when attempting the proof of phi using model-check,
  I get:
  
  phi :  
  
    |-------
  [1]   FORALL (n: [pigeon -> [hole -> bool]]): NOT phi(n)
  
  Rerunning step: (MODEL-CHECK)[mu_init]: v1.4 Copyright (C) 1992-1997 G. Janss
 en, Eindhoven University
  
  Error: Received signal number 11 (Segmentation violation)
    [condition type: SYNCHRONOUS-OPERATING-SYSTEM-SIGNAL]
  
  Restart actions (select using :continue):
   0: Return to Top Level (an "abort" restart)
  [1] PVS(55): :bt
  Evaluation stack:
  
  DECODE-ARRAY <-
    UNCURRY-APPLICATION-AND-MU-CONVERT <-
    (METHOD CONVERT-PVS-TO-MU* (APPLICATION)) <-
    (METHOD CONVERT-PVS-TO-MU* :AROUND ...) <-
    (:INTERNAL (:EFFECTIVE-METHOD 1 NIL ...) 0) <-
    [... CONVERT-PVS-TO-MU* ] <- CONVERT-PVS-TO-MU-FORMULA <-
    CONVERT-PVS-TO-MU-BINDING-EXPR <-
    (METHOD CONVERT-PVS-TO-MU* :AROUND ...) <-
    (:INTERNAL (:EFFECTIVE-METHOD 1 NIL ...) 0) <-
    [... CONVERT-PVS-TO-MU* ] <- CONVERT-PVS-TO-MU-FORMULA <-
    CONVERT-PVS-TO-MU-BINDING-EXPR <-
    (METHOD CONVERT-PVS-TO-MU* :AROUND ...) <-
    (:INTERNAL (:EFFECTIVE-METHOD 1 NIL ...) 0) <-
    [... CONVERT-PVS-TO-MU* ] <- CONVERT-PVS-TO-MU-CONJUNCTION <-
    (METHOD CONVERT-PVS-TO-MU* (APPLICATION)) <-
    (METHOD CONVERT-PVS-TO-MU* :AROUND ...) <-
    (:INTERNAL (:EFFECTIVE-METHOD 1 NIL ...) 0) <-
    [... CONVERT-PVS-TO-MU* ] <- CONVERT-PVS-TO-MU-FORMULA <-
    CONVERT-PVS-TO-MU <- RUN-MUSIMP <- (:INTERNAL MUSIMP-FUN 0) <-
    RULE-APPLY <- (METHOD PROOFSTEPPER (PROOFSTATE)) <-
    [... PROOFSTEPPER ] <- (LABELS (METHOD PROVE* #) PROVE*-INT) <-
    (METHOD PROVE* (PROOFSTATE)) <- [... PROVE* ] <- APPLY-STEP-BODY <-
    (:INTERNAL APPLY-STEP 0) <- RULE-APPLY <-
    (METHOD PROOFSTEPPER (PROOFSTATE)) <- [... PROOFSTEPPER ] <-
    (LABELS (METHOD PROVE* #) PROVE*-INT)(METHOD PROVE* (PROOFSTATE)) <-
    [... PROVE* ] <-  ...
  
  [1] PVS(56): 

From:    Hassen Saidi <saidi@csl.sri.com>
Date:    Sun, 12 Sep 1999 13:25:23 PDT

 In decode-array there is mu_mk_abstraction () bindex !!
 This is the problem. Let me figure out what is the argiment for 
 mu_mk_abstraction.

 Hassen.

How-To-Repeat: 

Fix: 

 [davesc, 9/12/01]
 I've corrected the type error (passing lisp nil instead of an empty C list)
 in the decode-array function.  However, this example now reports "could not
 decode binary encoding of scalars".  I'll ask hassen/shankar to look at this.

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