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

PVS Bug 1028


Synopsis:        latex-proof latex error: You can't use `macro parameter character #' in horizontal mode
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Tue Mar 11 12:30:00 -0700 2008
Originator:      Hendrik Tews
Release:         PVS 4.1
Organization:    cs.ru.nl
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  for some infix operators latex-proof generates invalid latex, for
  instance 
  
  Expanding the definition of  ##,
  
  or
  
  Expanding the definition of ^,
  
  See for example the generated latex for read_data_valid_in_mem
  (abstract_data.pvs) or bit_set_full_mask_TCC1 (bits.pvs) in the
  tar file of the "prettyprint-expanded dies with..." bug report.
  
  Bye,
  
  Hendrik

How-To-Repeat: 

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