begriffs open source - acsl-example/blob - test/test_frama_c_single.sh

   1 #!/bin/bash
   2
   3 # Test script to verify ACSL contracts using Frama-C for a single file
   4 # Usage: ./test_frama_c_single.sh <filename>
   5
   6 if [ $# -ne 1 ]; then
   7     echo "Usage: $0 <filename>"
   8     echo "Example: $0 find1.c"
   9     exit 1
  10 fi
  11
  12 FILENAME=$1
  13 BASENAME=$(basename "$FILENAME" .c)
  14
  15 echo "Running Frama-C verification on $FILENAME..."
  16
  17 # Set opam environment for proper tool paths
  18 eval $(opam env)
  19
  20 # Run frama-c with WP (weakest precondition) plugin to prove contracts using Coq
  21 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)
  22 FRAMA_EXIT=$?
  23
  24 echo "$FRAMA_OUTPUT"
  25
  26 # Check for complete verification (no failures, timeouts, or unknowns)
  27 if [ $FRAMA_EXIT -ne 0 ]; then
  28     echo "✗ Frama-C execution failed for $BASENAME"
  29     exit 1
  30 elif echo "$FRAMA_OUTPUT" | grep -q "\[Failure\]"; then
  31     echo "✗ Frama-C verification incomplete - some proof goals failed for $BASENAME"
  32     exit 1
  33 elif echo "$FRAMA_OUTPUT" | grep -q "\[Timeout\]"; then
  34     echo "✗ Frama-C verification incomplete - some proof goals timed out for $BASENAME"
  35     exit 1
  36 elif echo "$FRAMA_OUTPUT" | grep -q "Unknown:"; then
  37     echo "✗ Frama-C verification incomplete - some proof goals remain unknown for $BASENAME"
  38     exit 1
  39 else
  40     echo "✓ All ACSL contracts verified successfully for $BASENAME"
  41     exit 0
  42 fi