#!/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