#!/bin/bash

# Test script to verify ACSL contracts using Frama-C for a single file
# Usage: ./test_frama_c_single.sh <filename>

if [ $# -ne 1 ]; then
    echo "Usage: $0 <filename>"
    echo "Example: $0 find1.c"
    exit 1
fi

FILENAME=$1
BASENAME=$(basename "$FILENAME" .c)

echo "Running Frama-C verification on $FILENAME..."

# Run frama-c with WP (weakest precondition) plugin to prove contracts
frama-c -wp -wp-rte -wp-prover cvc4 -wp-timeout 5 -wp-cache update -verbose 2 -wp-verbose 3 -wp-debug 1 -wp-proof-trace -cpp-extra-args="-I../inc" "../src/$FILENAME"

# Check the exit code
if [ $? -eq 0 ]; then
    echo "✓ All ACSL contracts verified successfully for $BASENAME"
    exit 0
else
    echo "✗ Frama-C verification failed for $BASENAME"
    exit 1
fi