From b51e849f9398cbeb65416b4c71476407917e3125 Mon Sep 17 00:00:00 2001
From: kroening <kroening@6afb6bc1-c8e4-404c-8f48-9ae832c5b171>
Date: Fri, 21 Jun 2013 14:41:57 +0000
Subject: [PATCH] -fsingle-precision-constant

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@2661 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
---
 doc/html-manual/modeling-floating-point.shtml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/doc/html-manual/modeling-floating-point.shtml b/doc/html-manual/modeling-floating-point.shtml
index 6ee66efd91..099776c47a 100644
--- a/doc/html-manual/modeling-floating-point.shtml
+++ b/doc/html-manual/modeling-floating-point.shtml
@@ -47,7 +47,12 @@
 <li><p class="justified">
   Constant expressions are evaluated at `run' time wherever possible
   and so will respect changes in the rounding mode.  In effect,
-  the <code>FENV_ACCESS</code> pragma is always off.
+  the <code>FENV_ACCESS</code> pragma is always off.  Note that
+  floating point constants are treated as doubles (unless they are
+  followed by <code>f</code> when they are float) as specified in the
+  C standard.  <code>goto-cc</code>
+  supports <code>-fsingle-precision-constant</code>, which allows the
+  (non-standard) treatment of constants as floats.
   </p></li>
 </ul>