#!/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..."

# Set opam environment for proper tool paths
eval $(opam env)

# Run frama-c with WP (weakest precondition) plugin to prove contracts using Coq
FRAMA_OUTPUT=$(frama-c -wp -wp-rte -wp-prover coq -wp-timeout 30 -wp-cache rebuild -verbose 2 -wp-verbose 3 -wp-debug 1 -wp-proof-trace -cpp-extra-args="-I../inc" "../src/$FILENAME" 2>&1)
FRAMA_EXIT=$?

echo "$FRAMA_OUTPUT"

# Check for complete verification (no failures, timeouts, or unknowns)
if [ $FRAMA_EXIT -ne 0 ]; then
    echo "✗ Frama-C execution failed for $BASENAME"
    exit 1
elif echo "$FRAMA_OUTPUT" | grep -q "\[Failure\]"; then
    echo "✗ Frama-C verification incomplete - some proof goals failed for $BASENAME"
    exit 1
elif echo "$FRAMA_OUTPUT" | grep -q "\[Timeout\]"; then
    echo "✗ Frama-C verification incomplete - some proof goals timed out for $BASENAME"
    exit 1
elif echo "$FRAMA_OUTPUT" | grep -q "Unknown:"; then
    echo "✗ Frama-C verification incomplete - some proof goals remain unknown for $BASENAME"
    exit 1
else
    echo "✓ All ACSL contracts verified successfully for $BASENAME"
    exit 0
fi