fact: Definition test_int_or_ptr_spec := DECLARE _test_int_or_ptr WITH x : val PRE [int_or_ptr_type] PROP (valid_int_or_ptr x) PARAMS (x) GLOBALS () SEP () POST [ tint ] PROP() RETURN(Vint (Int.repr (match x with | Vint _ => if Archi.ptr64 then 0 else 1 | Vlong _ => if Archi.ptr64 then 1 else 0 | _ => 0 end))) SEP().
imports: VST.veric.rmaps CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.CertiGC.GCGraph CertiGraph.CertiGC.spatial_gcgraph CertiGraph.CertiGC.env_graph_gc CertiGraph.msl_ext.iter_sepcon