Function check_contract 

pub fn check_contract<'tcx>(
    contract: &Contract<'tcx>,
    abstate_item: &AbstractStateItem<'tcx>,
) -> bool