section ‹LLVM Verification Condition Generator› theory LLVM_VCG_Main imports LLVM_Shallow_RS begin text ‹Entrypoint to the LLVM VCG, with minimal setup› end