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

PVS Bug 1040


Synopsis:        more latex-proof problems II
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Mon May 19 11:35:01 -0700 2008
Originator:      Hendrik Tews
Release:         PVS 4.1
Organization:    cs.ru.nl
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  I encounted more problems with latex-proof in the PVS repository at
  http://www.cs.ru.nl/~tews/Robin/robin-hw-model-2008-05-15.tgz:
  
  - For the following lemmas latex proof fails with
  
      Found 'eof' when expecting 'opsym, !id!, IF, TRUE, FALSE, [||], (||), {||
 }, (, or !number!'
  
    max_linear_offset_val (constants.pvs)
    pde_valid_to_byte (paging-data-modes.pvs)
    pte_valid_to_byte (paging-data-modes.pvs)
    plain_memory_inv_pred_write_data (plain_memory.pvs)
    while_terminates (statement-rewrites.pvs)
    hoare_while (statement-rewrites.pvs)
  
  
  - For the following two one gets Error: Stack overflow (signal
    1000)
  
    search_not_found (search-example.pvs)
    search_found (search-example.pvs)
  
  
  - The complete list of lemmas for which the verbose latex proof
    contains invalid tex is:
  
  	linear_resolve_same_page_address 
  	device_plain_unchanged_memory_invariant 
  	device_plain_read_side_effect_unchanged 
  	device_plain_write_side_effect_unchanged 
  	device_plain_transformers_ok2 
  	linear_plain_transformers_ok 
  	linear_plain_unchanged_memory_invariant 
  	linear_unchanged_invariant 
  	plain_memory_transformer_invariant_write_data 
  	plain_mem_write_list_states 
  
    (The first 4 have been reported in #1034 already.) 
  
  
  Bye,
  
  Hendrik

How-To-Repeat: 

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