Automatic MOD clause

[QinshiWang]

The MOD clause is a part of a func spec that specifies what local variables and extern objects can be modified by a function, so function calls can be handled modularly. Currently, the MOD clause is automatically verified but not automatically generated, so the user still needs to manually write it. It is pretty long sometime, e.g.

Definition tbl_set_win_query_spec : func_spec :=
  WITH (* p *),
    PATH p
    MOD (Some [["ds_md"];
               ["act_set_clear_win_1"; "api_1"];
               ["act_set_clear_win_1"; "api_2"];
               ["act_set_clear_win_1"; "api_3"];
               ["act_set_clear_win_1"; "api_4"];
               ["act_set_clear_win_2"; "api_1"];
               ["act_set_clear_win_2"; "api_2"];
               ["act_set_clear_win_2"; "api_3"];
               ["act_set_clear_win_2"; "api_4"];
               ["act_set_clear_win_3"; "api_1"];
               ["act_set_clear_win_3"; "api_2"];
               ["act_set_clear_win_3"; "api_3"];
               ["act_set_clear_win_3"; "api_4"];
               ["act_set_clear_win_2"; "api_1"];
               ["act_set_clear_win_4"; "api_1"];
               ["act_set_clear_win_4"; "api_2"];
               ["act_set_clear_win_4"; "api_3"];
               ["act_set_clear_win_4"; "api_4"]]) []
               ...

because the local variables inside functions are exposed in the MOD clause. Since the MOD clause can be verified, it should also be able to be generated, unless the user wants better control.