package No_Caching with SPARK_Mode is
   type Mult_Bit_Boolean is (NV_FALSE, NV_TRUE);
   for Mult_Bit_Boolean use (NV_FALSE => 16#55_AA#,
                             NV_TRUE => 16#AA_55#);
   procedure Handle (V : Mult_Bit_Boolean);
   procedure Do_Something;
   procedure Do_Something_Else;
end No_Caching;