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

PVS Bug 453


Synopsis:        Nonemptiness TCCs
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Mar 21 21:00:00 2000
Originator:      Bruno Dutertre
Organization:    csl.sri.com
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------0F3F0AD00D3B1BA3BA05B4A1
  Content-Type: text/plain; charset=us-ascii
  Content-Transfer-Encoding: 7bit
  
  Sam,
  
  I've put the example in the attached file. There are three
  TCCs for the types key, nonce, and identity.
  
  Bruno
  --------------0F3F0AD00D3B1BA3BA05B4A1
  Content-Type: text/plain; charset=us-ascii;
   name="data.pvs"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
   filename="data.pvs"
  
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %  Message types for Enclaves's        %
  %  join and leave protocols            %
  %  and the group membership protocol   %
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
  data: THEORY
  
    BEGIN
  
    field : DATATYPE
      BEGIN
        No(nx: nat): nonce?
        Id(ix: nat): identity?
        Key(kx: nat): key?
      END field
  
    key: NONEMPTY_TYPE = (key?)
  
    nonce: NONEMPTY_TYPE = (nonce?)
  
    identity: NONEMPTY_TYPE = (identity?)
  
    data: DATATYPE 
      BEGIN
        clear(content: list[field]): clear_text?
        crypto(content: list[field], skey: key): crypto?
      END data
  
    END data
  
  --------------0F3F0AD00D3B1BA3BA05B4A1--

How-To-Repeat: 

Fix: 
Fixed check-nonempty-type and set-adt-nonemptiness to set as nonempty the
recognizer type of a given constructor whose accessor types are all known
to be nonempty (also includes constructors without accessors).
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools