val debug : bool ref val verbose : bool ref val werror : bool ref val inv_sem : Jc_env.inv_sem ref val separation_sem : Jc_env.separation_sem ref