fact: Definition f_test_int_or_ptr := {| fn_return := tint; fn_callconv := cc_default; fn_params := ((_x, (talignas 3%N (tptr tvoid))) :: nil); fn_vars := nil; fn_temps := nil; fn_body := (Sreturn (Some (Ecast (Ebinop Oand (Ecast (Etempvar _x (talignas 3%N (tptr tvoid))) tlong) (Econst_int (Int.repr 1) tint) tlong) tint))) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)