Re: Formal semantics for C

• To: Fergus Henderson <fjh@cs.mu.oz.au>
• Subject: Re: Formal semantics for C
• From: Corky Cartwright <cork@rice.edu>
• Date: Thu, 27 Dec 2001 11:51:27 -0600 (CST)
• Cc: matthias@ccs.neu.edu, kfl@it.edu, types@cis.upenn.edu
• In-Reply-To: <20011228001534.A8225@hg.cs.mu.oz.au>
• References: <200112251446.fBPEk5Q19557@saul.cis.upenn.edu> <15401.31359.196762.870718@frosty.cs.rice.edu> <20011228001534.A8225@hg.cs.mu.oz.au>

  > Compiler optimization researchers perform non-trivial analyses of C
  > programs (e.g., a pointer alias analysis) by ducking the issue of unsafe
  > operations: the simply assume that unsafe operations are never executed.

  This is not "ducking the issue".  On the contrary, this is an approach
  whose correctness can be proven from the semantics of C, as specified
  in the C standard or more formally in the works referred to earlier.

Nonsense!  These optimizations are incorrect (do not preserve the
meaning of programs) because they presume programs never perform unsafe
operation, but in fact they do.  

-- Corky Cartwright

• Re: Formal semantics for C
• From: Fergus Henderson <fjh@cs.mu.oz.au>

• Re: Formal semantics for C
• From: Corky Cartwright <cork@rice.edu>
• Re: Formal semantics for C
• From: Fergus Henderson <fjh@cs.mu.oz.au>

• Prev: Component Pascal type system is unsound
• Next: Formal semantics for C++ type inference?
• Index(es):
  • Main
  • Thread