search for: frama_c

...+set -e +set -x + +requires frama-c -version +requires frama-c -wp-h + +sources="tvdiff.h" + +# For how to get Frama-C to exit with an error if the proof fails, +# see: https://git.frama-c.com/pub/frama-c/-/issues/34 +frama-c -wp -wp-rte $sources \ + -cpp-extra-args="-I../.. -DFRAMA_C=1" \ + -wp-par=`nproc` \ + -then -report-classify -report-status -report-unclassified-unknown ERROR diff --git a/common/include/test-tvdiff.c b/common/include/test-tvdiff.c index abefb2e7..1bf6523b 100644 --- a/common/include/test-tvdiff.c +++ b/common/include/test-tvdiff.c @@ -4...