Как проверить VCC сгенерированную программу Boogie с Boogie?

Question

Я пытаюсь запустить VCC, чтобы проверить программы C. Меня интересует промежуточная программа Boogie, созданная VCC (так как я хочу вставить туда материал). С этой целью VCC предлагает вариант /t. Однако, когда я пытаюсь запустить Boogie на сгенерированной программе буги, буги существует и жалуется много ошибок, которые делятся на три категории (следующие примеры из моего кода C):

• Error: undeclared identifier: $arch_ptr_size
• Error: undeclared type: $ctype
• Error: use of undeclared function: $in_range_i4

программа C Я хочу, чтобы проверить, является тривиальным (см. ниже) VCC проверяет его без проблем.

#include <vcc.h> 

int main() { 
    int i = 0; 
    _(assert i == 0) 
} 

Что я делаю неправильно? Есть ли варианты Boogie, которые мне не хватает?

Answer 1

Решение вызывает вызов Boggie с дополнительным файлом Vcc3Prelude.bpl.