make_func_ptr, or evaluating a global name, without GLOBALS(gv)

[andrew-appel]

Trying to execute the tactic make_func_ptr _foo for extern function foo, without a GLOBALS(gv) in the current funspec, leads to a not-very-useful error message.

Same for evaluating &_foo or _foo without GLOBALS(gv).

TODO: detect this and improve the error message.

[andrew-appel]

Implementation of the first improvement:

Ltac make_func_ptr id ::=  
  eapply (make_func_ptr id);
  [ (reflexivity || fail 99  "Local variable " id " is shadowing the global variable" id)
  | (reflexivity || fail 99 "No specification of function " id " in Delta.  If the current function is a leaf function, you may need to invoke the [function_pointers] tactic before [start_function].  If that doesn't work, make sure you have not done clear_Delta_specs or [clearbody Delta_specs].")
  | (reflexivity || fail 99 "No global variable " id " in Delta, i.e., in your extern declarations")
(* BEGINNING OF NEW PART *)
  | split; [ reflexivity || fail 99 "Cannot find 'gvars gv' in your LOCAL list; did you forget GLOBALS(gv) in your funspec?"
             | reflexivity || fail 99 "It is inconceivable that make_func_ptr would fail this way."
             ]
(* END OF NEW PART *)
  | ].

Implementation of the second improvement:

Ltac diagnose_solve_msubst_eval_expr :=
 solve_msubst_eval_expr
  || match goal with |- msubst_eval_expr ?Delta ?T1 ?T2 ?GV ?e = _ =>
      match e with
      | context [Eaddrof (Evar ?id ?t) ?t'] => 
           let e1 := constr:(msubst_eval_expr Delta T1 T2 GV (Eaddrof (Evar id t) t')) in
           let e1 := eval compute in e1 in
           match e1 with None => 
               tryif unify GV None
              then fail 1000 "Cannot find the address of" id "as either a local or global variable; sometimes this is caused by a missing lvar clause in the LOCALs"
              else 
                  fail 1000 "Cannot find the address of" id "as either a local or global variable; sometimes this is caused by a missing lvar or gvar clause in the LOCALs; missing gvar clause can be caused by omitting GLOBALS(gv) in the funspec precondition"
           end
      | _ =>  fail 1000 "Cannot evaluate right-hand-side expression (sometimes this is caused by missing LOCALs in your precondition)"
      end
     end.

Replace each of the lines in sc_set_load_store.v that calls (solve_msubst_eval_expr || fail 1000 "...") with diagnose_solve_msubst_eval_expr.