cbmc/specgen/testfiles/simple_test_with_assertions.c

#include <stdio.h>

/**
 * Simple function to calculate the sum of an array
 * @param arr Pointer to the array
 * @param size Size of the array
 * @return Sum of array elements
 */
int array_sum(int* arr, int size) {
    // Precondition: array pointer is valid and size is non-negative
    __CPROVER_assume(arr != NULL);
    __CPROVER_assume(size >= 0);
    
    int sum = 0;
    for (int i = 0; i < size; i++) {
        // Loop invariant: sum equals the sum of arr[0] to arr[i-1]
        __CPROVER_assert(i >= 0 && i < size, "Array bounds check in array_sum loop");
        __CPROVER_assert(__CPROVER_POINTER_OBJECT(arr + i) == __CPROVER_POINTER_OBJECT(arr), "Pointer validity in array_sum");
        
        // Overflow check for addition
        __CPROVER_assert(!__CPROVER_overflow_plus(sum, arr[i]), "No overflow in array_sum addition");
        
        sum += arr[i];
    }
    return sum;
}

/**
 * Function to find the maximum value in an array
 * @param arr Pointer to the array
 * @param size Size of the array
 * @return Maximum value in the array
 */
int find_max(int* arr, int size) {
    // Precondition: array pointer is valid if size > 0
    __CPROVER_assume(size <= 0 || arr != NULL);
    __CPROVER_assume(size >= 0);
    
    if (size <= 0) {
        return 0;
    }

    // Precondition: array is accessible when size > 0
    __CPROVER_assert(arr != NULL, "Array pointer not NULL in find_max");
    __CPROVER_assert(size > 0, "Size positive in find_max");
    
    int max = arr[0];
    for (int i = 1; i < size; i++) {
        // Loop invariant: max is the maximum of arr[0] to arr[i-1]
        __CPROVER_assert(i >= 1 && i < size, "Array bounds check in find_max loop");
        __CPROVER_assert(__CPROVER_POINTER_OBJECT(arr + i) == __CPROVER_POINTER_OBJECT(arr), "Pointer validity in find_max");
        
        if (arr[i] > max) {
            max = arr[i];
        }
    }
    return max;
}

/**
 * Simple arithmetic operations function
 * @param a First operand
 * @param b Second operand
 * @return Result of a * b + a
 */
int arithmetic_ops(int a, int b) {
    // Overflow checks for arithmetic operations
    __CPROVER_assert(!__CPROVER_overflow_mult(a, b), "No overflow in multiplication");
    
    int product = a * b;
    
    __CPROVER_assert(!__CPROVER_overflow_plus(product, a), "No overflow in addition");
    
    int result = product + a;
    return result;
}

/**
 * Pointer manipulation function
 * @param ptr Pointer to integer
 * @param value Value to set
 * @return The value that was set
 */
int pointer_ops(int* ptr, int value) {
    // Precondition: if ptr is not NULL, it points to valid memory
    __CPROVER_assume(ptr == NULL || __CPROVER_r_ok(ptr, sizeof(int)));
    
    if (ptr != NULL) {
        // Pointer dereference safety
        __CPROVER_assert(__CPROVER_r_ok(ptr, sizeof(int)), "Pointer readable in pointer_ops");
        __CPROVER_assert(__CPROVER_w_ok(ptr, sizeof(int)), "Pointer writable in pointer_ops");
        *ptr = value;
    }
    return value;
}

int main() {
    int test_array[] = {1, 2, 3, 4, 5};
    int size = 5;

    // Precondition: test_array is valid and size matches
    __CPROVER_assume(size == 5);
    __CPROVER_assume(__CPROVER_r_ok(test_array, size * sizeof(int)));
    
    int sum = array_sum(test_array, size);
    int max = find_max(test_array, size);
    int result = arithmetic_ops(2, 3);

    int x = 0;
    pointer_ops(&x, 42);

    // Postconditions
    __CPROVER_assert(sum == 15, "Sum of 1+2+3+4+5 equals 15");
    __CPROVER_assert(max == 5, "Maximum of {1,2,3,4,5} equals 5");
    __CPROVER_assert(result == 2*3+2, "arithmetic_ops(2,3) equals 8");
    __CPROVER_assert(x == 42, "x should be set to 42");

    printf("Sum: %d, Max: %d, Result: %d, X: %d\n", sum, max, result, x);

    return 0;
}