Add missing coverage properties to tasks

Thomas Lembergerrequested to merge
update-coverage-properties-2025 into main

Tasks were selected based on the following criteria:

  • Compiles, if __VERIFIER_X method definitions are provided,
  • No termination property or expected verdict for termination is true, and
  • Some _VERIFIER_nondet* method exists that is not only declared, but used in at least one other location

Compliance is checked and properties are added with the scripts found at https://gist.github.com/lembergerth/1a1bf782931fb16af0d9e4bc1085a737 .

To check compilation, I used PRTest 6b191d1 with this patch (to not use optimizations and to include -lm)

diff --git a/bin/prtest b/bin/prtest
index 5e713ab..a3cce52 100755
--- a/bin/prtest
+++ b/bin/prtest
@@ -39,7 +39,7 @@ done

 PROJECT_DIR=$(readlink -f "$(dirname "$0")"/..)

-clang -O3 -fsanitize-coverage=trace-pc-guard -I"$PROJECT_DIR"/include
-o output/generator "$PROJECT_DIR"/src/random_tester.c
"$PROJECT_DIR"/src/test-comp-defs.c "${args[@]}"
+clang -lm -I"$PROJECT_DIR"/include -o output/generator
"$PROJECT_DIR"/src/random_tester.c "$PROJECT_DIR"/src/test-comp-defs.c
"${args[@]}"
 if [[ $COMPILE_ONLY == 1 ]]; then
   exit
 fi

Merge request reports