fact: Definition f_freeSet := {| fn_return := tvoid; fn_callconv := cc_default; fn_params := ((_subsets, (tptr (Tstruct _subset noattr))) :: nil); fn_vars := nil; fn_temps := nil; fn_body := (Scall None (Evar _freeN (Tfunction (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ((Etempvar _subsets (tptr (Tstruct _subset noattr))) :: nil)) |}.
imports: Coq(String List ZArith) compcert(Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs)