diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml
index 4667d170c..f3ebcfb78 100644
--- a/sledge/cli/domain_itv.ml
+++ b/sledge/cli/domain_itv.ml
@@ -65,7 +65,8 @@ let rec apron_typ_of_llair_typ : Llair.Typ.t -> Texpr1.typ option = function
 
 let rec apron_texpr_of_llair_exp exp q =
   match (exp : Llair.Exp.t) with
-  | Reg {name} -> Some (Texpr1.Var (apron_var_of_name name))
+  | Reg {name} | Function {name} ->
+      Some (Texpr1.Var (apron_var_of_name name))
   | Integer {data} -> Some (Texpr1.Cst (Coeff.s_of_int (Z.to_int data)))
   | Float {data} -> (
     match Float.of_string_exn data with
@@ -198,7 +199,7 @@ let exec_inst i q =
 
 (** Treat any intrinsic function as havoc on the return register [aret] *)
 let exec_intrinsic ~skip_throw:_ aret i _ pre =
-  let name = Llair.Reg.name i in
+  let name = Llair.Function.name i in
   if
     List.exists
       [ "malloc"
@@ -302,8 +303,8 @@ let call ~summaries ~globals:_ ~actuals ~areturn ~formals ~freturn:_
 let dnf q = [q]
 
 let resolve_callee lookup ptr q =
-  match Llair.Reg.of_exp ptr with
-  | Some callee -> (lookup (Llair.Reg.name callee), q)
+  match Llair.Function.of_exp ptr with
+  | Some callee -> (lookup callee, q)
   | None -> ([], q)
 
 type summary = t
diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml
index dbdee9567..2b8fc867c 100644
--- a/sledge/cli/frontend.ml
+++ b/sledge/cli/frontend.ml
@@ -18,7 +18,7 @@ let pp_llblock fs t =
   Format.pp_print_string fs (Llvm.string_of_llvalue (Llvm.value_of_block t))
 
 ;;
-Reg.demangle :=
+Exp.demangle :=
   let open Ctypes in
   let cxa_demangle =
     (* char *__cxa_demangle(const char *, char *, size_t *, int * ) *)
@@ -452,7 +452,12 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Inst.t list * Exp.t
     | Instruction (Invoke | Alloca | Load | PHI | LandingPad | VAArg)
      |Argument ->
         ([], Exp.reg (xlate_name x llv))
-    | Function | GlobalVariable -> ([], Exp.reg (xlate_global x llv).reg)
+    | Function ->
+        ( []
+        , Exp.function_
+            (Function.mk (xlate_type x (Llvm.type_of llv)) (find_name llv))
+        )
+    | GlobalVariable -> ([], Exp.reg (xlate_global x llv).reg)
     | GlobalAlias -> xlate_value x (Llvm.operand llv 0)
     | ConstantInt -> ([], xlate_int x llv)
     | ConstantFP -> ([], xlate_float x llv)
@@ -916,7 +921,11 @@ let pp_code fs (insts, term, blocks) =
 
 let rec xlate_func_name x llv =
   match Llvm.classify_value llv with
-  | Function | GlobalVariable -> ([], Exp.reg (xlate_name x ~global:() llv))
+  | Function ->
+      ( []
+      , Exp.function_
+          (Function.mk (xlate_type x (Llvm.type_of llv)) (find_name llv)) )
+  | GlobalVariable -> ([], Exp.reg (xlate_name x ~global:() llv))
   | ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv)
   | Argument | Instruction _ -> xlate_value x llv
   | GlobalAlias -> xlate_func_name x (Llvm.operand llv 0)
@@ -1424,21 +1433,23 @@ let xlate_block : pop_thunk -> x -> Llvm.llbasicblock -> Llair.block list =
 
 let report_undefined func name =
   if Option.is_some (Llvm.use_begin func) then
-    [%Trace.info "undefined function: %a" Global.pp name]
+    [%Trace.info "undefined function: %a" Function.pp name]
 
 let xlate_function : x -> Llvm.llvalue -> Llair.func =
  fun x llf ->
   [%Trace.call fun {pf} -> pf "%a" pp_llvalue llf]
   ;
   undef_count := 0 ;
-  let name = xlate_global x llf in
+  let loc = find_loc llf in
+  let typ = xlate_type x (Llvm.type_of llf) in
+  let name = Function.mk typ (find_name llf) in
   let formals =
     Llvm.fold_left_params
       (fun rev_args param -> xlate_name x param :: rev_args)
       [] llf
   in
   let freturn =
-    match Reg.typ name.reg with
+    match typ with
     | Pointer {elt= Function {return= Some typ; _}} ->
         Some (Reg.program typ "freturn")
     | _ -> None
@@ -1466,10 +1477,10 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
         in
         trav_blocks (List.rev entry_blocks) entry_blk
       in
-      Func.mk ~name ~formals ~freturn ~fthrow ~entry ~cfg
+      Func.mk ~name ~formals ~freturn ~fthrow ~entry ~cfg ~loc
   | At_end _ ->
       report_undefined llf name ;
-      Func.mk_undefined ~name ~formals ~freturn ~fthrow )
+      Func.mk_undefined ~name ~formals ~freturn ~fthrow ~loc )
   |>
   [%Trace.retn fun {pf} -> pf "@\n%a" Func.pp]
 
diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml
index c7ce96d83..5aeb3a79f 100644
--- a/sledge/cli/sledge_cli.ml
+++ b/sledge/cli/sledge_cli.ml
@@ -75,6 +75,14 @@ let unmarshal file () =
     ~f:(fun ic -> (Marshal.from_channel ic : Llair.program))
     file
 
+let entry_points =
+  let void_to_void =
+    Llair.Typ.pointer
+      ~elt:(Llair.Typ.function_ ~args:IArray.empty ~return:None)
+  in
+  List.map (Config.find_list "entry-points") ~f:(fun name ->
+      Llair.Function.mk void_to_void name )
+
 let used_globals pgm preanalyze : Domain_used_globals.r =
   if preanalyze then
     let summary_table =
@@ -82,12 +90,12 @@ let used_globals pgm preanalyze : Domain_used_globals.r =
         { bound= 1
         ; skip_throw= false
         ; function_summaries= true
-        ; entry_points= Config.find_list "entry-points"
+        ; entry_points
         ; globals= Declared Llair.Reg.Set.empty }
         pgm
     in
     Per_function
-      (Llair.Reg.Map.map summary_table ~f:Llair.Reg.Set.union_list)
+      (Llair.Function.Map.map summary_table ~f:Llair.Reg.Set.union_list)
   else
     Declared
       (Llair.Reg.Set.of_iter
@@ -128,7 +136,6 @@ let analyze =
   fun program () ->
     let pgm = program () in
     let globals = used_globals pgm preanalyze_globals in
-    let entry_points = Config.find_list "entry-points" in
     let skip_throw = not exceptions in
     Domain_sh.simplify_states := not no_simplify_states ;
     Timer.enabled := stats ;
diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 3a0abe908..2de05504e 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -13,7 +13,7 @@ type exec_opts =
   { bound: int
   ; skip_throw: bool
   ; function_summaries: bool
-  ; entry_points: string list
+  ; entry_points: Llair.Function.t list
   ; globals: Domain_used_globals.r }
 
 module Make (Dom : Domain_intf.Dom) = struct
@@ -258,16 +258,14 @@ module Make (Dom : Domain_intf.Dom) = struct
   let exec_jump stk state block Llair.{dst; retreating} =
     Work.add ~prev:block ~retreating stk state dst
 
-  module RegTbl = HashTable.Make (Llair.Reg)
-
-  let summary_table = RegTbl.create ()
+  let summary_table = Llair.Function.Tbl.create ()
 
   let exec_call opts stk state block call globals =
     let Llair.{callee; actuals; areturn; return; recursive} = call in
     let Llair.{name; formals; freturn; locals; entry} = callee in
     [%Trace.call fun {pf} ->
-      pf "%a from %a with state@ %a" Llair.Reg.pp name.reg Llair.Reg.pp
-        return.dst.parent.name.reg Dom.pp state]
+      pf "%a from %a with state@ %a" Llair.Function.pp name
+        Llair.Function.pp return.dst.parent.name Dom.pp state]
     ;
     let dnf_states =
       if opts.function_summaries then Dom.dnf state else [state]
@@ -281,7 +279,7 @@ module Make (Dom : Domain_intf.Dom) = struct
           else
             let maybe_summary_post =
               let state = fst (domain_call ~summaries:false state) in
-              let* summary = RegTbl.find summary_table name.reg in
+              let* summary = Llair.Function.Tbl.find summary_table name in
               List.find_map ~f:(Dom.apply_summary state) summary
             in
             [%Trace.info
@@ -310,27 +308,26 @@ module Make (Dom : Domain_intf.Dom) = struct
   let pp_st () =
     [%Trace.printf
       "@[<v>%t@]" (fun fs ->
-          RegTbl.iteri summary_table ~f:(fun ~key ~data ->
-              Format.fprintf fs "@[<v>%a:@ @[%a@]@]@ " Llair.Reg.pp key
+          Llair.Function.Tbl.iteri summary_table ~f:(fun ~key ~data ->
+              Format.fprintf fs "@[<v>%a:@ @[%a@]@]@ " Llair.Function.pp key
                 (List.pp "@," Dom.pp_summary)
                 data ) )]
 
   let exec_return ~opts stk pre_state (block : Llair.block) exp =
     let Llair.{name; formals; freturn; locals} = block.parent in
-    [%Trace.call fun {pf} -> pf "from: %a" Llair.Reg.pp name.reg]
+    [%Trace.call fun {pf} -> pf "from: %a" Llair.Function.pp name]
     ;
     let summarize post_state =
       if not opts.function_summaries then post_state
       else
-        let globals =
-          Domain_used_globals.by_function opts.globals name.reg
-        in
+        let globals = Domain_used_globals.by_function opts.globals name in
         let function_summary, post_state =
           Dom.create_summary ~locals post_state
             ~formals:
               (Llair.Reg.Set.union (Llair.Reg.Set.of_list formals) globals)
         in
-        RegTbl.add_multi ~key:name.reg ~data:function_summary summary_table ;
+        Llair.Function.Tbl.add_multi ~key:name ~data:function_summary
+          summary_table ;
         pp_st () ;
         post_state
     in
@@ -350,8 +347,7 @@ module Make (Dom : Domain_intf.Dom) = struct
         (* Create and store a function summary for main *)
         if
           opts.function_summaries
-          && List.exists opts.entry_points
-               ~f:(String.equal (Llair.Reg.name name.reg))
+          && List.exists ~f:(Llair.Function.equal name) opts.entry_points
         then summarize exit_state |> (ignore : Dom.t -> unit) ;
         Work.skip )
     |>
@@ -359,7 +355,7 @@ module Make (Dom : Domain_intf.Dom) = struct
 
   let exec_throw stk pre_state (block : Llair.block) exc =
     let func = block.parent in
-    [%Trace.call fun {pf} -> pf "from %a" Llair.Reg.pp func.name.reg]
+    [%Trace.call fun {pf} -> pf "from %a" Llair.Function.pp func.name]
     ;
     let unwind formals scope from_call state =
       Dom.retn formals (Some func.fthrow) from_call
@@ -424,7 +420,7 @@ module Make (Dom : Domain_intf.Dom) = struct
               Dom.exec_assume state
                 (Llair.Exp.eq ptr
                    (Llair.Exp.label
-                      ~parent:(Llair.Reg.name jump.dst.parent.name.reg)
+                      ~parent:(Llair.Function.name jump.dst.parent.name)
                       ~name:jump.dst.lbl))
             with
             | Some state -> exec_jump stk state block jump |> Work.seq x
@@ -440,7 +436,7 @@ module Make (Dom : Domain_intf.Dom) = struct
             List.fold callees Work.skip ~f:(fun callee x ->
                 ( match
                     Dom.exec_intrinsic ~skip_throw:opts.skip_throw areturn
-                      callee.name.reg actuals state
+                      callee.name actuals state
                   with
                 | Some None ->
                     Report.invalid_access_term
@@ -454,7 +450,7 @@ module Make (Dom : Domain_intf.Dom) = struct
                 | None ->
                     exec_call opts stk state block {call with callee}
                       (Domain_used_globals.by_function opts.globals
-                         callee.name.reg) )
+                         callee.name) )
                 |> Work.seq x ) )
     | Return {exp} -> exec_return ~opts stk state block exp
     | Throw {exc} ->
@@ -495,13 +491,13 @@ module Make (Dom : Domain_intf.Dom) = struct
       ~f:(fun entry_point -> Llair.Func.find entry_point pgm.functions)
       opts.entry_points
     |> function
-    | Some {name= {reg}; formals= []; freturn; locals; entry} ->
+    | Some {name; formals= []; freturn; locals; entry} ->
         Some
           (Work.init
              (fst
                 (Dom.call ~summaries:opts.function_summaries
                    ~globals:
-                     (Domain_used_globals.by_function opts.globals reg)
+                     (Domain_used_globals.by_function opts.globals name)
                    ~actuals:[] ~areturn:None ~formals:[] ~freturn ~locals
                    (Dom.init pgm.globals)))
              entry)
@@ -513,9 +509,12 @@ module Make (Dom : Domain_intf.Dom) = struct
     | Some work -> Work.run ~f:(exec_block opts pgm) (work opts.bound)
     | None -> fail "no applicable harness" ()
 
-  let compute_summaries opts pgm : Dom.summary list Llair.Reg.Map.t =
+  let compute_summaries opts pgm : Dom.summary list Llair.Function.Map.t =
     assert opts.function_summaries ;
     exec_pgm opts pgm ;
-    RegTbl.fold summary_table Llair.Reg.Map.empty ~f:(fun ~key ~data map ->
-        match data with [] -> map | _ -> Llair.Reg.Map.add ~key ~data map )
+    Llair.Function.Tbl.fold summary_table Llair.Function.Map.empty
+      ~f:(fun ~key ~data map ->
+        match data with
+        | [] -> map
+        | _ -> Llair.Function.Map.add ~key ~data map )
 end
diff --git a/sledge/src/control.mli b/sledge/src/control.mli
index a528e59e0..3dc3a5545 100644
--- a/sledge/src/control.mli
+++ b/sledge/src/control.mli
@@ -11,12 +11,12 @@ type exec_opts =
   { bound: int  (** Loop/recursion unrolling bound *)
   ; skip_throw: bool  (** Treat throw as unreachable *)
   ; function_summaries: bool  (** Use function summarisation *)
-  ; entry_points: string list
+  ; entry_points: Llair.Function.t list
   ; globals: Domain_used_globals.r }
 
 module Make (Dom : Domain_intf.Dom) : sig
   val exec_pgm : exec_opts -> Llair.program -> unit
 
   val compute_summaries :
-    exec_opts -> Llair.program -> Dom.summary list Llair.Reg.Map.t
+    exec_opts -> Llair.program -> Dom.summary list Llair.Function.Map.t
 end
diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml
index 65fdaa8e1..57688cccd 100644
--- a/sledge/src/domain_intf.ml
+++ b/sledge/src/domain_intf.ml
@@ -23,7 +23,7 @@ module type Dom = sig
   val exec_intrinsic :
        skip_throw:bool
     -> Llair.Reg.t option
-    -> Llair.Reg.t
+    -> Llair.Function.t
     -> Llair.Exp.t list
     -> t
     -> t option option
@@ -45,7 +45,10 @@ module type Dom = sig
   val retn : Llair.Reg.t list -> Llair.Reg.t option -> from_call -> t -> t
 
   val resolve_callee :
-    (string -> Llair.func list) -> Llair.Exp.t -> t -> Llair.func list * t
+       (Llair.Function.t -> Llair.func list)
+    -> Llair.Exp.t
+    -> t
+    -> Llair.func list * t
 
   val recursion_beyond_bound : [`skip | `prune]
 
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 34988aca2..fc61d8612 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -69,7 +69,7 @@ let exec_inst inst pre =
   |> Option.map ~f:simplify
 
 let exec_intrinsic ~skip_throw r i es q =
-  Exec.intrinsic ~skip_throw q (Option.map ~f:X.reg r) (X.reg i)
+  Exec.intrinsic ~skip_throw q (Option.map ~f:X.reg r) (X.func i)
     (List.map ~f:X.term es)
   |> Option.map ~f:(Option.map ~f:simplify)
 
@@ -236,8 +236,8 @@ let retn formals freturn {areturn; unshadow; frame} q =
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
 let resolve_callee lookup ptr q =
-  match Llair.Reg.of_exp ptr with
-  | Some callee -> (lookup (Llair.Reg.name callee), q)
+  match Llair.Function.of_exp ptr with
+  | Some callee -> (lookup callee, q)
   | None -> ([], q)
 
 let recursion_beyond_bound = `prune
diff --git a/sledge/src/domain_unit.ml b/sledge/src/domain_unit.ml
index fd494b79d..5d0ffb849 100644
--- a/sledge/src/domain_unit.ml
+++ b/sledge/src/domain_unit.ml
@@ -32,8 +32,8 @@ let retn _ _ _ _ = ()
 let dnf () = [()]
 
 let resolve_callee lookup ptr _ =
-  match Llair.Reg.of_exp ptr with
-  | Some callee -> (lookup (Llair.Reg.name callee), ())
+  match Llair.Function.of_exp ptr with
+  | Some callee -> (lookup callee, ())
   | None -> ([], ())
 
 type summary = unit
diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml
index 82be51b26..9b2c57c42 100644
--- a/sledge/src/domain_used_globals.ml
+++ b/sledge/src/domain_used_globals.ml
@@ -43,7 +43,7 @@ let exec_inst inst st =
     Option.iter ~f:(fun uses -> pf "post:{%a}" pp uses)]
 
 let exec_intrinsic ~skip_throw:_ _ intrinsic actuals st =
-  let name = Llair.Reg.name intrinsic in
+  let name = Llair.Function.name intrinsic in
   if
     List.exists
       [ "malloc"
@@ -79,8 +79,8 @@ let call ~summaries:_ ~globals:_ ~actuals ~areturn:_ ~formals:_ ~freturn:_
 
 let resolve_callee lookup ptr st =
   let st = used_globals ptr st in
-  match Llair.Reg.of_exp ptr with
-  | Some callee -> (lookup (Llair.Reg.name callee), st)
+  match Llair.Function.of_exp ptr with
+  | Some callee -> (lookup callee, st)
   | None -> ([], st)
 
 (* A function summary is the set of global registers accessed by that
@@ -94,22 +94,22 @@ let apply_summary st summ = Some (Llair.Reg.Set.union st summ)
 (** Query *)
 
 type r =
-  | Per_function of Llair.Reg.Set.t Llair.Reg.Map.t
+  | Per_function of Llair.Reg.Set.t Llair.Function.Map.t
   | Declared of Llair.Reg.Set.t
 
-let by_function : r -> Llair.Reg.t -> t =
+let by_function : r -> Llair.Function.t -> t =
  fun s fn ->
-  [%Trace.call fun {pf} -> pf "%a" Llair.Reg.pp fn]
+  [%Trace.call fun {pf} -> pf "%a" Llair.Function.pp fn]
   ;
   ( match s with
   | Declared set -> set
   | Per_function map -> (
-    match Llair.Reg.Map.find fn map with
+    match Llair.Function.Map.find fn map with
     | Some gs -> gs
     | None ->
         fail
           "main analysis reached function %a that was not reached by \
            used-globals pre-analysis "
-          Llair.Reg.pp fn () ) )
+          Llair.Function.pp fn () ) )
   |>
   [%Trace.retn fun {pf} r -> pf "%a" Llair.Reg.Set.pp r]
diff --git a/sledge/src/domain_used_globals.mli b/sledge/src/domain_used_globals.mli
index e858a03ec..2fe681252 100644
--- a/sledge/src/domain_used_globals.mli
+++ b/sledge/src/domain_used_globals.mli
@@ -10,8 +10,8 @@
 include Domain_intf.Dom with type summary = Llair.Reg.Set.t
 
 type r =
-  | Per_function of Llair.Reg.Set.t Llair.Reg.Map.t
+  | Per_function of Llair.Reg.Set.t Llair.Function.Map.t
       (** per-function used-globals map *)
   | Declared of Llair.Reg.Set.t  (** program-wide set *)
 
-val by_function : r -> Llair.Reg.t -> summary
+val by_function : r -> Llair.Function.t -> summary
diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 7cd7d92b8..896a65c9f 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -63,6 +63,7 @@ module T = struct
 
   type t =
     | Reg of {name: string; global: bool; typ: Typ.t}
+    | Function of {name: string; typ: Typ.t [@ignore]}
     | Label of {parent: string; name: string}
     | Integer of {data: Z.t; typ: Typ.t}
     | Float of {data: string; typ: Typ.t}
@@ -81,6 +82,15 @@ module Set = struct
 end
 
 module Map = Map.Make (T)
+module Tbl = HashTable.Make (T)
+
+let demangle = ref (fun _ -> None)
+
+let pp_demangled ppf name =
+  match !demangle name with
+  | Some demangled when not (String.equal name demangled) ->
+      Format.fprintf ppf "“%s”" demangled
+  | _ -> ()
 
 let pp_op2 fs op =
   let pf fmt = Format.fprintf fs fmt in
@@ -120,6 +130,7 @@ let rec pp fs exp =
   match exp with
   | Reg {name; global= true} -> pf "%@%s" name
   | Reg {name; global= false} -> pf "%%%s" name
+  | Function {name} -> pf "&%s%a" name pp_demangled name
   | Label {name} -> pf "%s" name
   | Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null"
   | Integer {data} -> Trace.pp_styled `Magenta "%a" fs Z.pp data
@@ -162,6 +173,8 @@ let rec invariant exp =
   let@ () = Invariant.invariant [%here] exp [%sexp_of: t] in
   match exp with
   | Reg {typ} -> assert (Typ.is_sized typ)
+  | Function {typ= Pointer {elt= Function _}} -> ()
+  | Function _ -> assert false
   | Integer {data; typ} -> (
     match typ with
     | Integer {bits} ->
@@ -238,7 +251,7 @@ let rec invariant exp =
 
 and typ_of exp =
   match exp with
-  | Reg {typ} | Integer {typ} | Float {typ} -> typ
+  | Reg {typ} | Function {typ} | Integer {typ} | Float {typ} -> typ
   | Label _ -> Typ.ptr
   | Ap1 ((Signed _ | Unsigned _ | Convert _ | Splat), dst, _) -> dst
   | Ap1 (Select idx, typ, _) -> (
@@ -277,19 +290,6 @@ module Reg = struct
     let pp = Set.pp pp_exp
   end
 
-  module Map = Map
-
-  let demangle = ref (fun _ -> None)
-
-  let pp_demangled fs = function
-    | Reg {name} -> (
-      match !demangle name with
-      | Some demangled when not (String.equal name demangled) ->
-          Format.fprintf fs "“%s”" demangled
-      | _ -> () )
-    | _ -> ()
-    [@@warning "-9"]
-
   let invariant x =
     let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
     match x with Reg _ -> invariant x | _ -> assert false
@@ -297,7 +297,7 @@ module Reg = struct
   let name = function Reg x -> x.name | r -> violates invariant r
   let typ = function Reg x -> x.typ | r -> violates invariant r
   let is_global = function Reg x -> x.global | r -> violates invariant r
-  let of_ = function Reg _ as r -> r | _ -> invalid_arg "Reg.of_"
+  let pp_demangled ppf r = pp_demangled ppf (name r)
 
   let of_exp = function
     | Reg _ as e -> Some (e |> check invariant)
@@ -307,6 +307,28 @@ module Reg = struct
     Reg {name; global= Option.is_some global; typ} |> check invariant
 end
 
+(** Function names are the expressions constructed by [Function] *)
+module Function = struct
+  include T
+
+  let pp = pp
+  let name = function Function x -> x.name | r -> violates invariant r
+  let typ = function Function x -> x.typ | r -> violates invariant r
+
+  let invariant x =
+    let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
+    match x with Function _ -> invariant x | _ -> assert false
+
+  let of_exp = function
+    | Function _ as e -> Some (e |> check invariant)
+    | _ -> None
+
+  let mk typ name = Function {name; typ} |> check invariant
+
+  module Map = Map
+  module Tbl = Tbl
+end
+
 (** Construct *)
 
 (* registers *)
@@ -315,6 +337,7 @@ let reg x = x
 
 (* constants *)
 
+let function_ f = f
 let label ~parent ~name = Label {parent; name} |> check invariant
 let integer typ data = Integer {data; typ} |> check invariant
 let null = integer Typ.ptr Z.zero
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index 3e701d046..1f0b7a32c 100644
--- a/sledge/src/llair/exp.mli
+++ b/sledge/src/llair/exp.mli
@@ -73,6 +73,7 @@ type opN = Record  (** Record (array / struct) constant *)
 
 type t = private
   | Reg of {name: string; global: bool; typ: Typ.t}  (** Virtual register *)
+  | Function of {name: string; typ: Typ.t [@ignore]}  (** Function name *)
   | Label of {parent: string; name: string}
       (** Address of named code block within parent function *)
   | Integer of {data: Z.t; typ: Typ.t}  (** Integer constant *)
@@ -87,6 +88,8 @@ val pp : t pp
 
 include Invariant.S with type t := t
 
+val demangle : (string -> string option) ref
+
 (** Exp.Reg is re-exported as Reg *)
 module Reg : sig
   type exp := t
@@ -100,15 +103,11 @@ module Reg : sig
     val pp : t pp
   end
 
-  module Map : Map.S with type key := t
-
-  val demangle : (string -> string option) ref
   val pp : t pp
   val pp_demangled : t pp
 
   include Invariant.S with type t := t
 
-  val of_ : exp -> t
   val of_exp : exp -> t option
   val program : ?global:unit -> Typ.t -> string -> t
   val name : t -> string
@@ -116,12 +115,31 @@ module Reg : sig
   val is_global : t -> bool
 end
 
+(** Exp.Function is re-exported as Function *)
+module Function : sig
+  type exp := t
+  type t = private exp [@@deriving compare, equal, hash, sexp]
+
+  module Map : Map.S with type key := t
+  module Tbl : HashTable.S with type key := t
+
+  val pp : t pp
+
+  include Invariant.S with type t := t
+
+  val of_exp : exp -> t option
+  val mk : Typ.t -> string -> t
+  val name : t -> string
+  val typ : t -> Typ.t
+end
+
 (** Construct *)
 
 (* registers *)
 val reg : Reg.t -> t
 
 (* constants *)
+val function_ : Function.t -> t
 val label : parent:string -> name:string -> t
 val null : t
 val bool : bool -> t
diff --git a/sledge/src/llair/function.ml b/sledge/src/llair/function.ml
new file mode 100644
index 000000000..d6efda53a
--- /dev/null
+++ b/sledge/src/llair/function.ml
@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Function names *)
+
+include Exp.Function
diff --git a/sledge/src/llair/function.mli b/sledge/src/llair/function.mli
new file mode 100644
index 000000000..09c61ca99
--- /dev/null
+++ b/sledge/src/llair/function.mli
@@ -0,0 +1,12 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Function names *)
+
+include module type of struct
+  include Exp.Function
+end
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index 7be1ade09..0f13731cd 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -13,6 +13,7 @@ module Loc = Loc
 module Typ = Typ
 module Reg = Reg
 module Exp = Exp
+module Function = Function
 module Global = Global
 
 type inst =
@@ -59,12 +60,13 @@ and block =
   ; mutable sort_index: int }
 
 and func =
-  { name: Global.t
+  { name: Function.t
   ; formals: Reg.t list
   ; freturn: Reg.t option
   ; fthrow: Reg.t
   ; locals: Reg.Set.t
-  ; entry: block }
+  ; entry: block
+  ; loc: Loc.t }
 
 let sexp_cons (hd : Sexp.t) (tl : Sexp.t) =
   match tl with
@@ -104,23 +106,24 @@ let sexp_of_block {lbl; cmnd; term; parent; sort_index} =
     { lbl: label
     ; cmnd: cmnd
     ; term: term
-    ; parent: Reg.t = parent.name.reg
+    ; parent: Function.t = parent.name
     ; sort_index: int }]
 
-let sexp_of_func {name; formals; freturn; fthrow; locals; entry} =
+let sexp_of_func {name; formals; freturn; fthrow; locals; entry; loc} =
   [%sexp
-    { name: Global.t
+    { name: Function.t
     ; formals: Reg.t list
     ; freturn: Reg.t option
     ; fthrow: Reg.t
     ; locals: Reg.Set.t
-    ; entry: block }]
+    ; entry: block
+    ; loc: Loc.t }]
 
 (* blocks in a [t] are uniquely identified by [sort_index] *)
 let compare_block x y = Int.compare x.sort_index y.sort_index
 let equal_block x y = Int.equal x.sort_index y.sort_index
 
-type functions = func String.Map.t [@@deriving sexp_of]
+type functions = func Function.Map.t [@@deriving sexp_of]
 
 type program = {globals: Global.t iarray; functions: functions}
 [@@deriving sexp_of]
@@ -219,13 +222,16 @@ let rec dummy_block =
   ; sort_index= 0 }
 
 and dummy_func =
-  let dummy_reg = Reg.program ~global:() Typ.ptr "dummy" in
-  { name= Global.mk dummy_reg Loc.none
+  { name=
+      Function.mk
+        (Typ.pointer ~elt:(Typ.function_ ~args:IArray.empty ~return:None))
+        "dummy"
   ; formals= []
   ; freturn= None
-  ; fthrow= dummy_reg
+  ; fthrow= Reg.program Typ.ptr "dummy"
   ; locals= Reg.Set.empty
-  ; entry= dummy_block }
+  ; entry= dummy_block
+  ; loc= Loc.none }
 
 (** Instructions *)
 
@@ -387,14 +393,14 @@ module Block_label = struct
     type t = block [@@deriving sexp_of]
 
     let compare x y =
-      [%compare: string * Global.t] (x.lbl, x.parent.name)
+      [%compare: string * Function.t] (x.lbl, x.parent.name)
         (y.lbl, y.parent.name)
 
     let equal x y =
-      [%equal: string * Global.t] (x.lbl, x.parent.name)
+      [%equal: string * Function.t] (x.lbl, x.parent.name)
         (y.lbl, y.parent.name)
 
-    let hash b = [%hash: string * Global.t] (b.lbl, b.parent.name)
+    let hash b = [%hash: string * Function.t] (b.lbl, b.parent.name)
   end
 
   include T
@@ -403,7 +409,7 @@ end
 
 module BlockS = HashSet.Make (Block_label)
 module BlockQ = HashQueue.Make (Block_label)
-module FuncQ = HashQueue.Make (Reg)
+module FuncQ = HashQueue.Make (Function)
 
 (** Functions *)
 
@@ -437,16 +443,16 @@ module Func = struct
   let entry_cfg func = fold_cfg ~f:(fun blk cfg -> blk :: cfg) func []
 
   let pp fs func =
-    let {name; formals; freturn; entry; _} = func in
+    let {name; formals; freturn; entry; loc; _} = func in
     let {cmnd; term; sort_index; _} = entry in
     let pp_if cnd str fs = if cnd then Format.fprintf fs str in
     Format.fprintf fs "@[<v>@[<v>%a%a@[<2>%a%a@]%t@]"
       (Option.pp "%a " Typ.pp)
-      ( match Reg.typ name.reg with
+      ( match Function.typ name with
       | Pointer {elt= Function {return; _}} -> return
       | _ -> None )
       (Option.pp " %a := " Reg.pp)
-      freturn Global.pp name (pp_actuals pp_formal) formals
+      freturn Function.pp name (pp_actuals pp_formal) formals
       (fun fs ->
         if is_undefined func then Format.fprintf fs " #%i@]" sort_index
         else
@@ -454,7 +460,7 @@ module Func = struct
             List.sort ~cmp:Block.compare (List.tl_exn (entry_cfg func))
           in
           Format.fprintf fs " { #%i %a@;<1 4>@[<v>%a@ %a@]%t%a@]@ }"
-            sort_index Loc.pp name.loc pp_cmnd cmnd Term.pp term
+            sort_index Loc.pp loc pp_cmnd cmnd Term.pp term
             (pp_if (not (List.is_empty cfg)) "@ @   ")
             (List.pp "@\n@\n  " Block.pp)
             cfg )
@@ -462,7 +468,7 @@ module Func = struct
   let invariant func =
     assert (func == func.entry.parent) ;
     let@ () = Invariant.invariant [%here] func [%sexp_of: t] in
-    match Reg.typ func.name.reg with
+    match Function.typ func.name with
     | Pointer {elt= Function {return; _}; _} ->
         assert (
           not
@@ -475,9 +481,9 @@ module Func = struct
         iter_term func ~f:(fun term -> Term.invariant ~parent:func term)
     | _ -> assert false
 
-  let find functions name = String.Map.find functions name
+  let find functions name = Function.Map.find functions name
 
-  let mk ~(name : Global.t) ~formals ~freturn ~fthrow ~entry ~cfg =
+  let mk ~name ~formals ~freturn ~fthrow ~entry ~cfg ~loc =
     let locals =
       let locals_cmnd locals cmnd =
         IArray.fold_right ~f:Inst.union_locals cmnd locals
@@ -487,7 +493,7 @@ module Func = struct
       in
       IArray.fold ~f:locals_block cfg (locals_block entry Reg.Set.empty)
     in
-    let func = {name; formals; freturn; fthrow; locals; entry} in
+    let func = {name; formals; freturn; fthrow; locals; entry; loc} in
     let resolve_parent_and_jumps block =
       block.parent <- func ;
       let lookup cfg lbl : block =
@@ -522,13 +528,13 @@ end
 let set_derived_metadata functions =
   let compute_roots functions =
     let roots = FuncQ.create () in
-    String.Map.iter functions ~f:(fun func ->
-        FuncQ.enqueue_back_exn roots func.name.reg func ) ;
-    String.Map.iter functions ~f:(fun func ->
+    Function.Map.iter functions ~f:(fun func ->
+        FuncQ.enqueue_back_exn roots func.name func ) ;
+    Function.Map.iter functions ~f:(fun func ->
         Func.iter_term func ~f:(fun term ->
             match term with
             | Call {callee; _} -> (
-              match Reg.of_exp callee with
+              match Function.of_exp callee with
               | Some callee ->
                   FuncQ.remove roots callee |> (ignore : [> ] -> unit)
               | None -> () )
@@ -553,8 +559,8 @@ let set_derived_metadata functions =
         | Iswitch {tbl; _} -> IArray.iter tbl ~f:jump
         | Call ({callee; return; throw; _} as call) ->
             ( match
-                let* reg = Reg.of_exp callee in
-                Func.find (Reg.name reg) functions
+                let* name = Function.of_exp callee in
+                Func.find name functions
               with
             | Some func ->
                 if Block_label.Set.mem func.entry ancestors then
@@ -579,8 +585,8 @@ let set_derived_metadata functions =
         index := !index - 1 )
   in
   let functions =
-    List.fold functions String.Map.empty ~f:(fun func m ->
-        String.Map.add_exn ~key:(Reg.name func.name.reg) ~data:func m )
+    List.fold functions Function.Map.empty ~f:(fun func m ->
+        Function.Map.add_exn ~key:func.name ~data:func m )
   in
   let roots = compute_roots functions in
   let tips_to_roots = topsort functions roots in
@@ -607,7 +613,7 @@ module Program = struct
       (IArray.pp "@\n@\n" Global.pp_defn)
       globals
       (List.pp "@\n@\n" Func.pp)
-      ( String.Map.values functions
+      ( Function.Map.values functions
       |> Iter.to_list
       |> List.sort ~cmp:(fun x y -> compare_block x.entry y.entry) )
 end
diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli
index dad96f0da..640012fd1 100644
--- a/sledge/src/llair/llair.mli
+++ b/sledge/src/llair/llair.mli
@@ -12,6 +12,7 @@ module Loc = Loc
 module Typ = Typ
 module Reg = Reg
 module Exp = Exp
+module Function = Function
 module Global = Global
 
 (** Instructions for memory manipulation or other non-control effects. *)
@@ -92,12 +93,13 @@ and block = private
 (** A function is a control-flow graph with distinguished entry block, whose
     parameters are the function parameters. *)
 and func = private
-  { name: Global.t
+  { name: Function.t
   ; formals: Reg.t list  (** Formal parameters, first-param-last stack *)
   ; freturn: Reg.t option
   ; fthrow: Reg.t
   ; locals: Reg.Set.t  (** Local registers *)
-  ; entry: block }
+  ; entry: block
+  ; loc: Loc.t }
 
 type functions
 
@@ -180,25 +182,27 @@ module Func : sig
   include Invariant.S with type t := t
 
   val mk :
-       name:Global.t
+       name:Function.t
     -> formals:Reg.t list
     -> freturn:Reg.t option
     -> fthrow:Reg.t
     -> entry:block
     -> cfg:block iarray
-    -> func
+    -> loc:Loc.t
+    -> t
 
   val mk_undefined :
-       name:Global.t
+       name:Function.t
     -> formals:Reg.t list
     -> freturn:Reg.t option
     -> fthrow:Reg.t
+    -> loc:Loc.t
     -> t
 
-  val find : string -> functions -> func option
+  val find : Function.t -> functions -> t option
   (** Look up a function of the given name in the given functions. *)
 
-  val is_undefined : func -> bool
+  val is_undefined : t -> bool
   (** Holds of functions that are declared but not defined. *)
 end
 
diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml
index dd26b2375..a7de81324 100644
--- a/sledge/src/llair_to_Fol.ml
+++ b/sledge/src/llair_to_Fol.ml
@@ -9,6 +9,10 @@ open Fol
 module T = Term
 module F = Formula
 
+let func f =
+  let name = Llair.Function.name f in
+  Var.program ~name ~global:true
+
 let reg r =
   let name = Llair.Reg.name r in
   let global = Llair.Reg.is_global r in
@@ -64,6 +68,7 @@ and term : Llair.Exp.t -> T.t =
         (F.cond ~cnd:(formula cnd) ~pos:(formula pos) ~neg:(formula neg))
   (* terms *)
   | Reg {name; global; typ= _} -> T.var (Var.program ~name ~global)
+  | Function {name; typ= _} -> T.var (Var.program ~name ~global:true)
   | Label {parent; name} ->
       uap0 (Funsym.uninterp ("label_" ^ parent ^ "_" ^ name))
   | Integer {typ= _; data} -> T.integer data
diff --git a/sledge/src/llair_to_Fol.mli b/sledge/src/llair_to_Fol.mli
index cc501922d..8ca00887c 100644
--- a/sledge/src/llair_to_Fol.mli
+++ b/sledge/src/llair_to_Fol.mli
@@ -7,6 +7,7 @@
 
 open Fol
 
+val func : Llair.Function.t -> Var.t
 val reg : Llair.Reg.t -> Var.t
 val regs : Llair.Reg.Set.t -> Var.Set.t
 val term : Llair.Exp.t -> Term.t
diff --git a/sledge/src/report.ml b/sledge/src/report.ml
index 29f361021..b0760aa0e 100644
--- a/sledge/src/report.ml
+++ b/sledge/src/report.ml
@@ -14,12 +14,7 @@ let unknown_call call =
       (fun fs call -> Llair.Loc.pp fs (Llair.Term.loc call))
       call
       (fun fs (call : Llair.Term.t) ->
-        match call with
-        | Call {callee} -> (
-          match Llair.Reg.of_exp callee with
-          | Some reg -> Llair.Reg.pp_demangled fs reg
-          | None -> Llair.Exp.pp fs callee )
-        | _ -> () )
+        match call with Call {callee} -> Llair.Exp.pp fs callee | _ -> () )
       call Llair.Term.pp call]
 
 let invalid_access_count = ref 0