Merge pull request checkedc#10 from dtarditi/master

Implicit conversions and comparison operands.

Author: dtarditi

spec/bounds_safety/core-extensions.tex

@@ -183,7 +183,9 @@ \section{Operations involving pointer types}
   Pointers to objects of the same type can be compared for equality or
   inequality. The pointers do not have to be the same kind of pointer.
   To support reasoning about program behavior, the result of comparing
-  pointers to different objects must be defined.
+  pointers to different objects must be defined.  Safe pointers can also
+  be compared for equality or inequality with 0 and void pointers, 
+  just like unsafe pointers.
 \item
   Pointers to objects of the same type can be compared relationally. Relational comparisons are the
   \verb|<|, \verb|<=|, \verb|>|, \verb|>=| operators. The pointers do not have to be

spec/bounds_safety/interoperation.tex

@@ -281,7 +281,7 @@ \subsection{Implicit conversions involving safe pointers}
 \label{section:implicit-conversions}
 
 C allows implicit conversions at assignments, function call arguments,
-conditional expressions, and comparisons.  The purpose of
+and conditional expressions.  The purpose of
 implicit conversions is to make programs shorter and easier to
 read.  This section defines implicit conversions that are
 allowed for safe pointer types.
@@ -297,10 +297,10 @@ \subsubsection{From unsafe pointers to safe pointers}
 unsafe pointer and the safe pointer are compatible.
 
 This can be done for the right-hand side of an assignment, a call argument,
-an arm of a conditional expression, and an operand of a comparison.
-The type of the left-hand side of the assignment, the parameter, the other 
-arm of the conditional expression, or the other operand of the comparison
-must be the safe pointer type that is the target of the implicit conversion.
+or an arm of a conditional expression.
+The type of the left-hand side of the assignment, the parameter, or the other 
+arm of the conditional expression must be the safe pointer type that is the
+target of the implicit conversion.
 
 For now, compatibility is defined as the following:
 \begin{itemize}
@@ -331,9 +331,9 @@ \subsubsection{From safe pointers to safe pointers}
 An expression with a safe pointer type can be converted implicitly to the same kind
 of safe pointer type with a \texttt{void} referent type.   
 This can be done for the right-hand side of an assignment, a call argument, 
-an arm of a conditional expression, and an operand of a comparison.  
-The type of the left-hand side of the assignment, the parameter, the other
-arm of the conditional expression, or the other operand of the comparison
+and an arm of a conditional expression.  
+The type of the left-hand side of the assignment, the parameter, or the other
+arm of the conditional expression
 must be the safe \void\ pointer type that is the target of the implicit
 conversion. For example, implicit conversions from 
 \ptrinst{\var{T}} to \ptrvoid\ and from \arrayptrinst{\var{T}} to \arrayptrvoid\ are allowed 
@@ -343,22 +343,19 @@ \subsubsection{From safe pointers to safe pointers}
 The philosophy behind this is the same one that is used in C++: places where type-safety
 can be compromised by a cast should be explicit in the code.
 
-For comparisons, if one operand has type \ptrinst{\var{T}} and the other
-operand has type \arrayptrinst{\var{T}}, the operand with type \ptrinst{\var{T}}
-can be converted implicitly  to \arrayptrinst{\var{T}}.
-
 \subsubsection{Between safe pointers and integers}
 
 The null pointer (0) can be converted implicitly to any safe pointer type.   
 A safe pointer can be converted implicitly to the \texttt{\_Bool} type.
 
-\subsubsection{Illegal implicit conversions}
+Some C compilers extend C by allowing implicit conversions between pointers
+and integers or between pointers to incompatible types.  Implicit conversions
+from integers to safe pointers are typically not useful in Checked C because
+the checking of bounds declarations fails or the resulting pointer cannot
+be used to access memory.   The rules for checking bounds declarations only
+allow the target type to be \arrayptr\ type and the bounds of the expression to be
+\boundsnone.
 
-All other implicit conversions involving safe pointer types are not allowed.
-A compiler must treat a program containing those conversions as erroneous.
-Many C compilers allow implicit conversions between pointers and integers or
-between pointers to incompatible types.  They issue warning messages for
-those conversions.  These extensions are not permitted for safe pointers.
 
 \subsubsection{Examples}