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

PVS Bug 745


Synopsis:        musimp causing segmentation violation
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Fri Feb 21 18:35:01 2003
Originator:      Paul Jackson
Organization:    inf.ed.ac.uk
Release:         PVS 3.0
Environment: 
 System:          
 Architecture: 

Description: 
  Am using default PVS installation at SRI CSL:
  
  PVS Version 3.1
  Allegro CL Enterprise Edition
  6.2 [Linux (x86)] (Feb 14, 2003 18:42)
  
  
  Consider theory:
  
  mu_exp : THEORY 
   BEGIN
    State : TYPE = upto(4)
  
    x,y : VAR State
    N(x,y) : bool = 
         x = 0  AND y = 1
      OR x = 1 AND y = 2
      OR x = 2 AND y = 1
  
    I(x) : bool = x = 0
   
    R : VAR pred[State]
  
    a1 : LEMMA mu(lambda R: lambda x : I(x) OR Exists y : N(y,x) AND R(y))
               (2)
  
  
   END mu_exp
  
  
  Running musimp on Lemma a1 yields:
  
  pvs(58): 
  
  a1 :  
  
    |-------
  {1}   mu(LAMBDA R: LAMBDA x: I(x) OR (EXISTS y: N(y, x) AND R(y)))(2)
  
  Rule? (musimp)
  ~[mu b94.L b99,b100,b101.[L .b101?b100?b99?b102:b103:b99?b104:b105:b100?b99?b
 106:b107:b99?b108:b109](b117,b116,b115,b114,b113,b112,b111,b110) + (E b118,b11
 9,b120.(b120 + b119 + 1) & (~b120 + ~b119 & ~b118) & b121 & [mu_init]: Package
  already initialized.
  Added Relational variable `b124' to Ip.
  Added Relational variable `b125' to Ip.
  Added Relational variable `b126' to Ip.
  Added Relational variable `b127' to Ip.
  Added Relational variable `b128' to Ip.
  Looking up Relational variable: `b124'.
  Looking up Relational variable: `b125'.
  Looking up Relational variable: `b126'.
  Looking up Relational variable: `b127'.
  Looking up Relational variable: `b128'.
    
  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: Abort entirely from this process.
  [1] pvs(63): :bt
  Evaluation stack:
  
  run-musimp <-
    (:internal musimp-fun 0) <- rule-apply <-
    (method proofstepper (proofstate)) <- [... proofstepper ] <-
    prove*-int <- prove* <- prove-decl-body <-
    (method dpi-start* (# function)) <-
    (method prove-decl (formula-decl)) <-
    (method prove-decl :around ...) <-
    (:internal (:effective-method 1 t ...) 0) <- [... prove-decl ] <-
    (method prove (formula-decl)) <-
    (:internal (:effective-method 1 t ...) 0) <- prove-file-at <- eval <-
    tpl:top-level-read-eval-print-loop <- tpl:start-interactive-top-level
  
  [1] pvs(64): 

How-To-Repeat: 

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