diff --git a/ivory-backend-c.cabal b/ivory-backend-c.cabal
--- a/ivory-backend-c.cabal
+++ b/ivory-backend-c.cabal
@@ -2,7 +2,7 @@
 --  see http://haskell.org/cabal/users-guide/
 
 name:                ivory-backend-c
-version:             0.1.0.4
+version:             0.1.0.5
 author:              Galois, Inc.
 maintainer:          leepike@galois.com
 category:            Language
@@ -24,6 +24,7 @@
 library
   exposed-modules:      Ivory.Compile.C,
                         Ivory.Compile.C.Gen,
+                        Ivory.Compile.C.Gen.Const,
                         Ivory.Compile.C.Modules,
                         Ivory.Compile.C.Prop,
                         Ivory.Compile.C.Types,
diff --git a/runtime/ivory_asserts.h b/runtime/ivory_asserts.h
--- a/runtime/ivory_asserts.h
+++ b/runtime/ivory_asserts.h
@@ -54,11 +54,11 @@
 
 #else /* IVORY_TEST */
 
-#define REQUIRES(arg)
-#define ENSURES(arg)
-#define ASSUMES(arg)
-#define ASSERTS(arg)
-#define COMPILER_ASSERTS(arg)
+#define REQUIRES(arg)           (void)(arg)
+#define ENSURES(arg)            (void)(arg)
+#define ASSUMES(arg)            (void)(arg)
+#define ASSERTS(arg)            (void)(arg)
+#define COMPILER_ASSERTS(arg)   (void)(arg)
 
 #endif /* IVORY_TEST */
 
diff --git a/src/Ivory/Compile/C/Gen.hs b/src/Ivory/Compile/C/Gen.hs
--- a/src/Ivory/Compile/C/Gen.hs
+++ b/src/Ivory/Compile/C/Gen.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE CPP            #-}
-{-# LANGUAGE PackageImports #-}
 {-# LANGUAGE QuasiQuotes    #-}
 
 -- | Ivory backend targeting language-c-quote.
@@ -7,13 +6,14 @@
 module Ivory.Compile.C.Gen where
 
 import           Language.C.Quote.GCC
-import qualified "language-c-quote" Language.C.Syntax                     as C
+import qualified Language.C.Syntax                     as C
 
 import qualified Ivory.Language.Array                  as I
 import qualified Ivory.Language.Proc                   as P
 import qualified Ivory.Language.Syntax                 as I
 import           Ivory.Language.Syntax.Concrete.Pretty
 
+import           Ivory.Compile.C.Gen.Const (makeTargetConstIf)
 import           Ivory.Compile.C.Prop
 import           Ivory.Compile.C.Types
 
@@ -146,7 +146,7 @@
 
 -- | C type conversion, with a special case for references and pointers.
 toType' :: Bool -> I.Type -> C.Type
-toType' b ty = case ty of
+toType' decay ty = case ty of
   I.TyVoid              -> [cty| void |]
   I.TyChar              -> [cty| char |]
   I.TyInt i             -> intSize i
@@ -156,23 +156,26 @@
   I.TyFloat             -> [cty| float |]
   I.TyDouble            -> [cty| double |]
   I.TyStruct nm         -> [cty| struct $id:nm |]
-  I.TyConstRef t        -> [cty| const $ty:(arrCase t) |]
   I.TyCArray t          -> [cty| $ty:(toType t) * |]
   I.TyArr len t         -> [cty| $ty:(toType t)[$uint:len] |]
   I.TyProc retTy argTys ->
     [cty| $ty:(toType retTy) (*)
           ($params:(map (toParam . toType) argTys)) |]
   I.TyOpaque            -> error "Opaque type is not implementable."
-  I.TyRef t             -> arrCase t
-  I.TyPtr t             -> arrCase t
+  I.TyRef t             -> arrCase False  t
+  I.TyPtr t             -> arrCase False  t
+  I.TyConstRef t        -> arrCase True   t
+  I.TyConstPtr t        -> arrCase True   t
   where
-  arrCase t = case t of
-    I.TyArr len t'
-      -> if b then [cty| $ty:(toType t') * |]
-              else [cty| $ty:(toType t')[$uint:len] |]
-    I.TyCArray t'
-      -> [cty| $ty:(toType t') * |]
-    _ -> [cty| $ty:(toType t)  * |]
+  arrCase isTargetConst t =
+    makeTargetConstIf isTargetConst $
+    case t of
+      I.TyArr len t'
+        -> if decay then [cty| $ty:(toType t') * |]
+                    else [cty| $ty:(toType t')[$uint:len] |]
+      I.TyCArray t'
+        -> [cty| $ty:(toType t') * |]
+      _ -> [cty| $ty:(toType t)  * |]
 
 intSize :: I.IntSize -> C.Type
 intSize I.Int8  = [cty| typename int8_t  |]
diff --git a/src/Ivory/Compile/C/Gen/Const.hs b/src/Ivory/Compile/C/Gen/Const.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/Compile/C/Gen/Const.hs
@@ -0,0 +1,56 @@
+module Ivory.Compile.C.Gen.Const (makeTargetConst, makeTargetConstIf) where
+
+import           Data.Loc (noLoc)
+import qualified Language.C.Syntax as C
+
+makeTargetConstIf :: Bool -> C.Type -> C.Type
+makeTargetConstIf c t = if c then makeTargetConst t else t
+
+makeTargetConst :: C.Type -> C.Type
+makeTargetConst = modifyTargetQuals (C.Tconst noLoc :)
+
+modifyTargetQuals :: ([C.TypeQual] -> [C.TypeQual]) -> C.Type -> C.Type
+modifyTargetQuals f typ@(C.Type _ decl _) = case decl of
+  C.Array _ _ decl1 _ -> go decl1
+  C.Ptr _ decl1 _     -> go decl1
+  _                   -> typ
+  where
+    go decl1 = case decl1 of
+      C.DeclRoot{} ->
+        -- `typ` is rank 1 pointer, modify base
+        (modifyTypeDeclSpec . modifyDeclSpecQuals) f typ
+      C.Ptr{} ->
+        -- `typ` is rank >1 pointer, modify second pointer level
+        (modifyTypeDecl . modifyNestedDecl . modifyPtrQuals) f typ
+      _ ->
+        -- nothing to do here
+        typ
+modifyTargetQuals _ typ@C.AntiType{} = internalError typ
+
+modifyDeclSpecQuals
+  :: ([C.TypeQual] -> [C.TypeQual]) -> C.DeclSpec -> C.DeclSpec
+modifyDeclSpecQuals f declSpec = case declSpec of
+  C.DeclSpec storage quals spec loc -> C.DeclSpec storage (f quals) spec loc
+  C.AntiDeclSpec{}                  -> internalError declSpec
+  C.AntiTypeDeclSpec{}              -> internalError declSpec
+
+modifyNestedDecl :: (C.Decl -> C.Decl) -> C.Decl -> C.Decl
+modifyNestedDecl f decl0 = case decl0 of
+  C.Array quals size decl loc -> C.Array quals size (f decl) loc
+  C.Ptr quals decl loc        -> C.Ptr quals (f decl) loc
+  _                           -> decl0
+
+modifyPtrQuals :: ([C.TypeQual] -> [C.TypeQual]) -> C.Decl -> C.Decl
+modifyPtrQuals f (C.Ptr quals decl loc)  = C.Ptr (f quals) decl loc
+modifyPtrQuals _ decl                    = decl
+
+modifyTypeDecl :: (C.Decl -> C.Decl) -> C.Type -> C.Type
+modifyTypeDecl f (C.Type declSpec decl loc) = C.Type declSpec (f decl) loc
+modifyTypeDecl _ typ@C.AntiType{}           = internalError typ
+
+modifyTypeDeclSpec :: (C.DeclSpec -> C.DeclSpec) -> C.Type -> C.Type
+modifyTypeDeclSpec f (C.Type declSpec decl loc) = C.Type (f declSpec) decl loc
+modifyTypeDeclSpec _ typ@C.AntiType{}           = internalError typ
+
+internalError :: Show a => a -> b
+internalError a = error $ "internal language-c-quote data leaked: " ++ show a