mirror of
https://github.com/AdaCore/spark2014.git
synced 2026-02-12 12:39:11 -08:00
a004cf8435
A useful pattern to protect a multiplication against overflow can now be proved automatically by using the lemma Lemma_Mult_Protect from the SPARK lemma library. * include/proof/Coq/spark-integer_arithmetic_lemmas/*.v * include/proof/Coq/spark-long_integer_arithmetic_lemmas/*.v Proofs of new lemma in 32bits and 64bits cases. * include/proof/sessions/spark-integer_arithmetic_lemmas/why3session.xml * include/proof/sessions/spark-integer_arithmetic_lemmas/why3shapes * include/proof/sessions/spark-long_integer_arithmetic_lemmas/why3session * include/proof/sessions/spark-long_integer_arithmetic_lemmas/why3shapes Update to session and shape files. * include/spark-arithmetic_lemmas.adb * include/spark-arithmetic_lemmas.ads New lemma Lemma_Mult_Protect. * include/spark_lemmas.gpr Add new env variable for easier development setup. * include/setup.sh Script to source for development setup. * testsuite/gnatprove/tests/P405-006__arithmetic_lemmas/test.out * testsuite/gnatprove/tests/P405-006__arithmetic_lemmas/test_arith.adb Update test.
5 lines
167 B
Bash
Executable File
5 lines
167 B
Bash
Executable File
# use "source setup.sh" before opening spark_lemmas.gpr in GPS
|
|
export SPARK_LEMMAS_OBJECT_DIR=obj
|
|
export SPARK_LEMMAS_INSTALLED=False
|
|
export SPARK_LEMMAS_BODY_MODE=On
|