Fixing the elaboration of casts from pointer types to _Bool

as specified by (§6.3.1.2#1), converting the value to 0 or 1.

frontend/model/driver.lem

@@ -760,6 +760,11 @@ let perform_memop_request2 loc memop cvals tid mk_th_st =
         ND.return (mk_th_st (Core.Vobject (Core.OVinteger ival)))
 
     | (Mem_common.IntFromPtr, [Core.Vctype ref_ty; Core.Vctype (Ctype.Ctype _ (Ctype.Basic (Ctype.Integer ity))); Core.Vobject (Core.OVpointer ptr_val)]) ->
+        begin if ity = Ctype.Bool then
+          ND.print_debug 0 [Debug.DB_driver] (fun () -> "IntFromPtr called on _Bool --> this is probably a bug in the elaboration")
+        else
+          ND.return ()
+        end >>= fun () -> (* DEBUG *)
         liftMem (Mem.intfromptr loc ref_ty ity ptr_val) >>= fun ival ->
         ND.return (mk_th_st (Core.Vobject (Core.OVinteger ival)))
 

frontend/model/translation.lem

@@ -1827,17 +1827,21 @@ else if AilTypesAux.is_pointer cast_ty && AilTypesAux.is_arithmetic e_ty then
 
 else if AilTypesAux.is_arithmetic cast_ty && AilTypesAux.is_pointer e_ty then
               (* making an integer from a pointer *)
-              let ref_ty = fromJust "Translation.translate_expression, AilEcast 2" (AilTypesAux.referenced_type e_ty) in
-              Caux.mk_wseq_e e_wrp.E.sym_pat core_e (
-                  Caux.mk_case_e e_wrp.E.sym_pe
-                    [ ( Caux.mk_specified_pat obj_wrp.E.sym_pat
-                      , Caux.mk_wseq_e (Caux.mk_sym_pat let_sym (C.BTy_object C.OTy_integer))
-                          (C.Expr [] (C.Ememop Mem_common.IntFromPtr [Caux.mk_ail_ctype_pe ref_ty; Caux.mk_ail_ctype_pe cast_ty; obj_wrp.E.sym_pe]))
-                          (Caux.mk_pure_e (Caux.mk_specified_pe (Caux.mk_sym_pe let_sym))) )
-                    ; ( Caux.mk_unspecified_pat (Caux.mk_empty_pat C.BTy_ctype)
-                      , (* Casting an unspecified pointer to an integer type gives an unspecified integer *)
-                        Caux.mk_pure_e (Caux.mk_unspecified_pe cast_ty) ) ]
-              )
+              if AilTypesAux.atomic_qualified_unqualified AilTypesAux.is_Bool cast_ty then
+                (* STD §6.3.1.2#1 *)
+                Caux.mk_wseq_e e_wrp.E.sym_pat core_e (stdlib.mkproc_loaded_pointer_to_Bool e_wrp.E.sym_pe)
+              else
+                let ref_ty = fromJust "Translation.translate_expression, AilEcast 2" (AilTypesAux.referenced_type e_ty) in
+                Caux.mk_wseq_e e_wrp.E.sym_pat core_e (
+                    Caux.mk_case_e e_wrp.E.sym_pe
+                      [ ( Caux.mk_specified_pat obj_wrp.E.sym_pat
+                        , Caux.mk_wseq_e (Caux.mk_sym_pat let_sym (C.BTy_object C.OTy_integer))
+                            (C.Expr [] (C.Ememop Mem_common.IntFromPtr [Caux.mk_ail_ctype_pe ref_ty; Caux.mk_ail_ctype_pe cast_ty; obj_wrp.E.sym_pe]))
+                            (Caux.mk_pure_e (Caux.mk_specified_pe (Caux.mk_sym_pe let_sym))) )
+                      ; ( Caux.mk_unspecified_pat (Caux.mk_empty_pat C.BTy_ctype)
+                        , (* Casting an unspecified pointer to an integer type gives an unspecified integer *)
+                          Caux.mk_pure_e (Caux.mk_unspecified_pe cast_ty) ) ]
+                )
 
 else (* pointer <-> pointer cast *)
               let () = Debug.warn [Debug.DB_elaboration] (fun () ->

tests/ci/0338-cast-pointer-to-_Bool.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdlib.h>
+#include <stdint.h>
+
+int main(void)
+{
+  int x;
+  uintptr_t ui = (uintptr_t)1234;
+  assert (1 == (_Bool)&x);
+  assert (1 == (_Bool)(int*)ui);
+  assert (0 == (_Bool)NULL);
+}

tests/tests.sh

@@ -203,6 +203,7 @@ citests=(
   0335-non_decimal_unsigned_long_int_constants.c
   0336-scalar-init-with_braces.syntax-only.c
   0337-scalar-init-with_braces.undef.c
+  0338-cast-pointer-to-_Bool.c
 )
 
 # TESTS THAT ARE KNOW TO FAIL (for example .error test for which we need to improve the message)