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