/* Commandline execution: * civl verify bundleSize.cvl * */ #include #include int N=5; $input double a[N]; void main() { $bundle bun; int size; bun = $bundle_pack(&a[0], N*sizeof(double)); size = $bundle_size(bun); $assert((size == N*sizeof(double))); $assert((size / sizeof(double) == N)); }