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

PVS Bug 1038


Synopsis:        bin files make proof fail
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Mon May 19 03:30:01 -0700 2008
Originator:      Hendrik Tews
Release:         PVS 4.1
Organization:    cs.ru.nl
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  for the PVS repository at
  http://www.cs.ru.nl/~tews/Robin/robin-hw-model-2008-05-15.tgz 
  the presents of some bin files make some proofs fail:
  
  - typecheck pageing-data.pvs
  - save-context
  - exit pvs and restart
  - typecheck expressions.pvs
  - now the proof of ptr_to_nonzero_object will fail
  - after make clean (rm -rf pvsbin) and with a fresh PVS the proof
    succeeds
  
  Bye,
  
  Hendrik

How-To-Repeat: 

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