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 # Run frama-c with WP (weakest precondition) plugin to prove contracts
  18 frama-c -wp -wp-rte -wp-prover cvc4 -verbose 2 -wp-verbose 3 -wp-debug 1 -wp-proof-trace -time "../timing_$BASENAME.log" -cpp-extra-args="-I../inc" "../src/$FILENAME"
  19
  20 # Check the exit code
  21 if [ $? -eq 0 ]; then
  22     echo "✓ All ACSL contracts verified successfully for $BASENAME"
  23     exit 0
  24 else
  25     echo "✗ Frama-C verification failed for $BASENAME"
  26     exit 1
  27 fi