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

PVS Bug 1080


Synopsis:        ["Michael Roe" : Array overrides in PVS]
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Mon Oct 24 12:35:00 -0700 2011
Originator:      "Peter G. Neumann"
Release:         PVS 5.0
Organization:    csl.sri.com
Environment: 
 System:          
 Architecture: 

Description: 
  Sam,
  Mike probably shou have included you on this.
  Peter
  
                  ---------------
  
  From: "Michael Roe" <mroe@cornstalk.org.uk>
  To: "'John Rushby'" <Rushby@csl.sri.com>, <shankar@csl.sri.com>,
          <bruno@csl.sri.com>
  Subject: Array overrides in PVS
  Date: Sun, 23 Oct 2011 16:36:46 +0100
  
  Hi,
  
  We've run into a problem with using PVS on the CTSRD project and I wondered
  if any of the PVS experts at SRI would be able to help.
  
  I've included below a short program that illustrates the problem. The PVS
  ground evaluator isn't able to evaluate test2, but as it's a just an array
  assignment (and then reading the element that wasn't assigned to), I think
  it should work.
  
  Thanks in advance,
  Mike
  
  ======================
  
  ArrayTest : THEORY
  
  BEGIN
  
    Byte : TYPE+ = {n : int | 0 <= n AND n <= 255} CONTAINING 0
  
    MappedAddr : TYPE+ = {n : int | 0 <= n AND n <= 1} CONTAINING 0
  
    Memory : TYPE+ = ARRAY [MappedAddr -> Byte]
  
    cReset : Memory = id
  
    cStore(s : Memory, x : Byte) : Memory = s WITH [(0) := x]
  
    test1 : Byte = cStore(cReset, 42)(0)
  
    test2 : Byte = cStore(cReset, 42)(1)
  
  END ArrayTest

How-To-Repeat: 

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