59 lines
2.4 KiB
Bash
Executable file
59 lines
2.4 KiB
Bash
Executable file
#!/bin/sh
|
|
|
|
# To use PVS with frama-c without the NASA Langley PVS library:
|
|
# frama-c -jessie -jessie-atp pvs FILE.c # Generates PVS files
|
|
# cd FILE.jessie/pvs
|
|
# patch_jessie_pvs # Patch jessie_why.pvs to not need NASA Langley library.
|
|
# You can then run PVS to prove the generated theorems with:
|
|
# pvs-sbcl FILE_why.pvs
|
|
#
|
|
# Copyright (c) 2010 David A. Wheeler
|
|
#
|
|
# Permission is hereby granted, free of charge, to any person obtaining a copy
|
|
# of this software and associated documentation files (the "Software"), to deal
|
|
# in the Software without restriction, including without limitation the rights
|
|
# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
|
# copies of the Software, and to permit persons to whom the Software is
|
|
# furnished to do so, subject to the following conditions:
|
|
#
|
|
# The above copyright notice and this permission notice shall be included in
|
|
# all copies or substantial portions of the Software.
|
|
#
|
|
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
|
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
|
# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
|
# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
|
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
|
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
|
|
# THE SOFTWARE.
|
|
|
|
|
|
if [ ! -f jessie_why.pvs ] ; then
|
|
echo "Did not find file jessie_why.pvs in current directory"
|
|
exit 1
|
|
fi
|
|
|
|
patch -p0 -N << END_OF_PATCH
|
|
--- jessie_why.pvs.ORIGINAL 2010-10-05 14:41:58.965970651 -0400
|
|
+++ jessie_why.pvs 2010-10-06 14:28:39.250971269 -0400
|
|
@@ -169,14 +169,14 @@
|
|
(FORALL (x: real): (FORALL (y: real): min(x, y) = x OR min(x, y) = y))
|
|
|
|
%% Why axiom sqrt_pos
|
|
- sqrt_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x) >= 0.0))
|
|
+ % sqrt_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x) >= 0.0))
|
|
|
|
%% Why axiom sqrt_sqr
|
|
- sqrt_sqr: AXIOM
|
|
- (FORALL (x: real): (x >= 0.0 IMPLIES sqr_real(sqrt(x)) = x))
|
|
+ % sqrt_sqr: AXIOM
|
|
+ % (FORALL (x: real): (x >= 0.0 IMPLIES sqr_real(sqrt(x)) = x))
|
|
|
|
%% Why axiom sqr_sqrt
|
|
- sqr_sqrt: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x * x) = x))
|
|
+ % sqr_sqrt: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES sqrt(x * x) = x))
|
|
|
|
%% Why axiom abs_real_pos
|
|
abs_real_pos: AXIOM (FORALL (x: real): (x >= 0.0 IMPLIES abs(x) = x))
|
|
END_OF_PATCH
|
|
|