What are the different properties( well formedness of the intermediate code, or other),if any that are verified by the verification phase in the LLVM.