lookup_sub_handler error case

[ccasin]

let lookup_sub_handler (tid: Bap.Std.Tid.t) (env: Env.t) (post: Constr.t)
    (jmp : Jmp.t) : Constr.t * Env.t =
  if is_intrinsic_call jmp then
    intrinsic_call tid env post jmp
  else
    match Env.get_sub_handler env tid with
    | Some (Summary compute_func) -> compute_func env post tid
    | Some Inline -> !inline_func post env tid
    | None -> post, env

The None case at the end seems scary. Does this ever happen? Should we be using a default summary here, or throwing an error, rather than silently dropping the function call?

[codyroux]

My understanding is that there should always be (at least) a "default" spec for every possible subroutine tid created here: https://github.com/draperlaboratory/cbat_tools/blob/8e747275c628d9568ef14d0fe4ab81f848608499/wp/lib/bap_wp/src/environment.ml#L165

So tentatively I would indeed throw an error at that place.