CODEWITHSUNDEEP
cverification
Dan
Dan

Reputation: 1547

How to verify a VCC generated Boogie program with Boogie?

I'm trying to run VCC in order to verify C programs. I'm interested in the intermediate Boogie program that is produced by VCC (as I want to insert stuff there). To this end, VCC offers the option /t. However, when I try to run Boogie on the generated Boogie program, Boogie exists and complains about a lot of errors, which fall into three categories (the following are examples from my C code):

The C program I want to verify is trivial (see below). VCC verifies it without a problem.

#include <vcc.h>

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

What am I doing wrong? Are there Boogie options I'm missing?

Upvotes: 1

Views: 116

Answers (1)

Dan
Dan

Reputation: 1547

The solution is to call Boggie with the additional file Vcc3Prelude.bpl.

Upvotes: 1

Related Questions