CIVL prgamas

• assumption

#pragma CIVL $assume EXPRESSION;

e.g. #pragma CIVL $assume NPROCS > 1 && NPROCS < 6;

• input variable

#pragma CIVL $input TYPE NAME;

e.g:

#pragma CIVL $input int NBLOCKS;
int NBLOCKS = 5;

The pragma tells the transformer to make NBLOCKS an input variable and ignore the initialization expression 5