语法解析为goto-model → CBMC Intermediate representation GOTO program 执行postprocessing，其中包括remove_asm，和label_properties等。 label_properties 为每个函数中的每类属性都进行了编号，在这之后，每个assertion都带有property_id。