(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2013                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* --- Bool Library for Alt-Ergo                                          --- *)
(* -------------------------------------------------------------------------- *)

logic ite: bool,'a,'a -> 'a
axiom ite: forall p:bool. forall x,y:'a [ite(p,x,y)].
   ( p=true and ite(p,x,y)=x ) or
   ( p=false and ite(p,x,y)=y )

logic eqb: 'a,'a -> bool
axiom eqb: forall x,y:'a [eqb(x,y)]. if eqb(x,y) then x=y else x<>y

logic neqb: 'a,'a -> bool
axiom neqb: forall x,y:'a [neqb(x,y)]. if neqb(x,y) then x<>y else x=y

function xorb  (a:bool,b:bool):bool = neqb(a,b)
function notb  (a:bool):bool = if a then false else true
function orb   (a:bool,b:bool):bool = if a then true else b
function andb  (a:bool,b:bool):bool = if a then b else false
function implb (a:bool,b:bool):bool = if a then b else true

(* -------------------------------------------------------------------------- *)
(* --- Extension of Array Theory for Alt-Ergo                             --- *)
(* -------------------------------------------------------------------------- *)

axiom array: 
  forall k:'a. forall v:'b. forall m:('a,'b) farray [ m[k<-v] ]. m[k<-v][k]=v

(* -------------------------------------------------------------------------- *)
(* --- Arithmetic Library for Alt-Ergo                                    --- *)
(* -------------------------------------------------------------------------- *)

logic real_of_int : int -> real
logic int_of_real : real -> int

logic zlt :  int,int -> bool
axiom zlt :  forall x,y:int [zlt(x,y)]. if zlt(x,y) then x<y else x>=y

logic zleq : int,int -> bool
axiom zleq : forall x,y:int [zleq(x,y)]. if zleq(x,y) then x<=y else x>y

logic rlt :  real,real -> bool
axiom rlt :  forall x,y:real [rlt(x,y)]. if rlt(x,y) then x<y else x>=y

logic rleq : real,real -> bool
axiom rleq : forall x,y:real [rleq(x,y)]. if rleq(x,y) then x<=y else x>y

(* -------------------------------------------------------------------------- *)
(* --- Division   Library for Alt-Ergo                                    --- *)
(* -------------------------------------------------------------------------- *)

logic cdiv : int,int -> int
logic cmod : int,int -> int

axiom c_enclidian : forall n,d:int [cdiv(n,d),cmod(n,d)].
  n = cdiv(n,d) * d + cmod(n,d)

axiom cdiv_cases : forall n,d:int [cdiv(n,d)]. 
  ((n >= 0) -> (d > 0) -> cdiv(n,d) = n/d) and
  ((n <= 0) -> (d > 0) -> cdiv(n,d) = -((-n)/d)) and
  ((n >= 0) -> (d < 0) -> cdiv(n,d) = -(n/(-d))) and
  ((n <= 0) -> (d < 0) -> cdiv(n,d) = (-n)/(-d))

axiom cmod_cases : forall n,d:int [cmod(n,d)].
  ((n >= 0) -> (d > 0) -> cmod(n,d) = n % d) and
  ((n <= 0) -> (d > 0) -> cmod(n,d) = -((-n) % d)) and
  ((n >= 0) -> (d < 0) -> cmod(n,d) = (n % (-d))) and
  ((n <= 0) -> (d < 0) -> cmod(n,d) = -((-n) % (-d)))

axiom cmod_remainder : forall n,d:int [cmod(n,d)].
  ((n >= 0) -> (d > 0) ->  0 <= cmod(n,d) <  d) and
  ((n <= 0) -> (d > 0) -> -d <  cmod(n,d) <= 0) and
  ((n >= 0) -> (d < 0) ->  0 <= cmod(n,d) < -d) and
  ((n <= 0) -> (d < 0) ->  d <  cmod(n,d) <= 0)

axiom cdiv_neutral : forall a:int [cdiv(a,1)]. cdiv(a,1) = a
axiom cdiv_inv : forall a:int [cdiv(a,a)]. a<>0 -> cdiv(a,a) = 1
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2013                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* --- C-Integer Arithmetics for Alt-Ergo                                 --- *)
(* -------------------------------------------------------------------------- *)

(* C-Float Conversion *)

logic to_float32 : real -> real
logic to_float64 : real -> real
predicate is_float32(x : real) = to_float32(x)=x
predicate is_float64(x : real) = to_float64(x)=x

(* C-Float Rounding Modes *)

type rounding_mode = Up | Down | ToZero | NearestTiesToAway | NearestTiesToEven
logic round_double : rounding_mode,real -> real
logic round_float : rounding_mode,real -> real
logic is_finite32 : real -> prop
logic is_finite64 : real -> prop

axiom float_32:
  forall x:real [ round_float( NearestTiesToEven , x ) ].
  to_float32(x) = round_float( NearestTiesToEven , x )

axiom float_64:
  forall x:real [ round_double( NearestTiesToEven , x ) ].
  to_float64(x) = round_double( NearestTiesToEven , x )

axiom is_finite_to_float_32 : 
  forall x:real [is_finite32(to_float32(x))]. is_finite32(to_float32(x))

axiom is_finite_to_float_64 :
  forall x:real [is_finite64(to_float64(x))]. is_finite64(to_float64(x))

(* C-Float Rounded Arithmetics *)

function add_float32(x:real,y:real):real = to_float32(x+y)
function add_float64(x:real,y:real):real = to_float64(x+y)

function sub_float32(x:real,y:real):real = to_float32(x-y)
function sub_float64(x:real,y:real):real = to_float64(x-y)

function mul_float32(x:real,y:real):real = to_float32(x*y)
function mul_float64(x:real,y:real):real = to_float64(x*y)

function div_float32(x:real,y:real):real = to_float32(x/y)
function div_float64(x:real,y:real):real = to_float64(x/y)

(* Real Arithmetics *)

function ropp(x:real):real = -x
function radd(x:real,y:real):real = x+y
function rsub(x:real,y:real):real = x-y
function rmul(x:real,y:real):real = x*y
function rdiv(x:real,y:real):real = x/y
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2013                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(* ---------------------------------------------------------------------- *)
(* --- cint library: C-Integer Arithmetics for Alt-Ergo               --- *)
(* ---------------------------------------------------------------------- *)

(* C-Integer Ranges *)

logic is_uint8 : int -> prop
logic is_sint8 : int -> prop
logic is_uint16 : int -> prop
logic is_sint16 : int -> prop
logic is_uint32 : int -> prop
logic is_sint32 : int -> prop
logic is_uint64 : int -> prop
logic is_sint64 : int -> prop

(* C-Integer Ranges Definitions *)

axiom def_uint8 : forall x:int  [ is_uint8(x) ].
                0 <= x < 256 <-> is_uint8(x) 
axiom def_sint8 : forall x:int  [ is_sint8(x) ].
             -128 <= x < 128 <-> is_sint8(x) 
axiom def_uint16 : forall x:int [ is_uint16(x) ].
               0 <= x < 65536 <-> is_uint16(x) 
axiom def_sint16 : forall x:int [ is_sint16(x) ].
          -32768 <= x < 32768 <-> is_sint16(x) 
axiom def_uint32 : forall x:int [ is_uint32(x) ].
          0 <= x < 4294967296 <-> is_uint32(x) 
axiom def_sint32 : forall x:int [ is_sint32(x) ].
  -2147483648 <= x < 2147483648 <-> is_sint32(x) 
axiom def_uint64 : forall x:int [ is_uint64(x) ].
  0 <= x < 18446744073709551616 <-> is_uint64(x) 
axiom def_sint64 : forall x:int [ is_sint64(x) ].
  -9223372036854775808 <= x < 9223372036854775808 <-> is_sint64(x) 

(* C-Integer Conversion *)

logic to_uint8  : int -> int 
logic to_sint8  : int -> int 
logic to_uint16 : int -> int 
logic to_sint16 : int -> int 
logic to_uint32 : int -> int 
logic to_sint32 : int -> int 
logic to_uint64 : int -> int 
logic to_sint64 : int -> int 

(* C-Integer Conversions are in-range *)

axiom is_to_uint8 : forall x:int 
[ is_uint8(to_uint8(x)) ].
  is_uint8(to_uint8(x)) 
axiom is_to_sint8 : forall x:int 
[ is_sint8(to_sint8(x)) ].
  is_sint8(to_sint8(x)) 
axiom is_to_uint16 : forall x:int 
[ is_uint16(to_uint16(x)) ].
  is_uint16(to_uint16(x)) 
axiom is_to_sint16 : forall x:int 
[ is_sint16(to_sint16(x)) ].
  is_sint16(to_sint16(x)) 
axiom is_to_uint32 : forall x:int 
[ is_uint32(to_uint32(x)) ].
  is_uint32(to_uint32(x)) 
axiom is_to_sint32 : forall x:int 
[ is_sint32(to_sint32(x)) ].
  is_sint32(to_sint32(x)) 
axiom is_to_uint64 : forall x:int 
[ is_uint64(to_uint64(x)) ].
  is_uint64(to_uint64(x)) 
axiom is_to_sint64 : forall x:int 
[ is_sint64(to_sint64(x)) ].
  is_sint64(to_sint64(x)) 

(* C-Integer Conversions are identity when in-range *)

axiom id_uint8 : forall x:int [ to_uint8(x) ].
                0 <= x < 256 -> to_uint8(x) = x 
axiom id_sint8 : forall x:int [ to_sint8(x) ].
             -128 <= x < 128 -> to_sint8(x) = x 
axiom id_uint16 : forall x:int [ to_uint16(x) ].
               0 <= x < 65536 -> to_uint16(x) = x 
axiom id_sint16 : forall x:int [ to_sint16(x) ].
          -32768 <= x < 32768 -> to_sint16(x) = x 
axiom id_uint32 : forall x:int [ to_uint32(x) ].
          0 <= x < 4294967296 -> to_uint32(x) = x 
axiom id_sint32 : forall x:int   [ to_sint32(x) ].
  -2147483648 <= x < 2147483648 -> to_sint32(x) = x 
axiom id_uint64 : forall x:int   [ to_uint64(x) ].
  0 <= x < 18446744073709551616 -> to_uint64(x) = x 
axiom id_sint64 : forall x:int                     [ to_sint64(x) ].
  -9223372036854775808 <= x < 9223372036854775808 -> to_sint64(x) = x 
 
(* C-Integer Bits Signature *)

logic    lnot : int -> int
logic ac land : int,int -> int
logic ac lxor : int,int -> int
logic ac lor  : int,int -> int

logic lsl  : int,int -> int
logic lsr  : int,int -> int

logic bit_test : int,int -> bool

(* End of cint library *)
(* ---------------------------------------------------------- *)
(* --- Post-condition for 'basic' (file mApLAlmRaiser_frama.c, line 139) in 'mApLAlmRaiser' --- *)
(* ---------------------------------------------------------- *)

goal mApLAlmRaiser_basic_post:
  let r_0 = 60.0e0 / 0.0 : real in
  forall AP_AU_ALM_INT_0,F_MIN_RR_0,
    P_R_STATE_0,bApAlmCond_0,bRAp_0,bYAp_0,
    gbOxyAdvS_0,gbOxyMonS_0,gnApDStop_3,gnApDStop_2,
    gnApDStop_1,gnApDStop_0,mbApLRRange_0,
    mbApLYRange_0,mnPbreath_0,nApLRLimit_0,
    nApLYLimit_0,nOxyLRLimit_0,nOxyLYLimit_0,
    tenumRRMode_0 : int.
  forall fOxyValue_0,gfApYLineConst_0,gfApYLineSlope_0,
    mfNewAp_2,mfNewAp_1,mfNewAp_0 : real.
  let r_1 = real_of_int(F_MIN_RR_0) : real in
  let r_2 = real_of_int(P_R_STATE_0) : real in
  let r_3 = real_of_int(nApLYLimit_0) : real in
  let r_4 = real_of_int(nOxyLYLimit_0) : real in
  let r_5 = real_of_int(nApLRLimit_0) : real in
  let r_6 = real_of_int(nOxyLRLimit_0) : real in
  let r_7 = gfApYLineConst_0
      + (fOxyValue_0 * gfApYLineSlope_0) : real in
  is_float32(mfNewAp_2) ->
  is_float32(mfNewAp_1) ->
  is_float32(mfNewAp_0) ->
  is_uint32(tenumRRMode_0) ->
  (((0.0 <> 0.0) ->
    ((0 = tenumRRMode_0) and
     (((r_0 < r_1) -> (0 = bApAlmCond_0)) and
      ((r_1 <= r_0) ->
       (((1 <> gbOxyMonS_0) -> (0 = bApAlmCond_0)) and
        ((1 = gbOxyMonS_0) ->
         (((0 <> gbOxyAdvS_0) -> (0 = bApAlmCond_0)) and
          ((0 = gbOxyAdvS_0) -> (1 = bApAlmCond_0))))))) and
     ((1 <> bApAlmCond_0) or
      (((r_3 <= r_0) -> (gnApDStop_3 = gnApDStop_1)) and
       ((r_0 < r_3) ->
        ((gnApDStop_2 = gnApDStop_1) and
         ((gnApDStop_3 = gnApDStop_2) or
          (1 <> mbApLRRange_0) or (1 <> mbApLYRange_0) or
          (AP_AU_ALM_INT_0 < 2)) and
         (((fOxyValue_0 < r_4) -> (1 = mbApLYRange_0)) and
          ((r_4 <= fOxyValue_0) ->
           (((1 <> bYAp_0) -> (0 = mbApLYRange_0)) and
            ((1 = bYAp_0) ->
             (((1 <> gbOxyMonS_0) -> (0 = mbApLYRange_0)) and
              ((1 = gbOxyMonS_0) ->
               (((0 <> gbOxyAdvS_0) -> (0 = mbApLYRange_0)) and
                ((0 = gbOxyAdvS_0) -> (1 = mbApLYRange_0))))))))) and
         (((r_5 <= r_0) -> (1 = mbApLRRange_0)) and
          ((r_0 < r_5) ->
           (((fOxyValue_0 < r_6) -> (1 = mbApLRRange_0)) and
            ((r_6 <= fOxyValue_0) ->
             (((1 <> bRAp_0) -> (0 = mbApLRRange_0)) and
              ((1 = bRAp_0) ->
               (((1 <> gbOxyMonS_0) -> (0 = mbApLRRange_0)) and
                ((1 = gbOxyMonS_0) ->
                 (((0 <> gbOxyAdvS_0) -> (0 = mbApLRRange_0)) and
                  ((0 = gbOxyAdvS_0) -> (1 = mbApLRRange_0))))))))))) and
         (((fOxyValue_0 < r_6) -> (0 = bRAp_0)) and
          ((r_6 <= fOxyValue_0) ->
           (((-1.0) < mfNewAp_2) and (mfNewAp_2 < 65536.0) and
            (((r_0 < mfNewAp_2) -> (0 = bRAp_0)) and
             ((mfNewAp_2 <= r_0) -> (1 = bRAp_0)))))) and
         ((fOxyValue_0 <= r_4) or
          (((-1.0) < mfNewAp_1) and (mfNewAp_1 < 65536.0) and
           (mfNewAp_1 = r_7))) and
         (((fOxyValue_0 < r_4) -> (0 = bYAp_0)) and
          ((r_4 <= fOxyValue_0) ->
           (((-1.0) < mfNewAp_0) and (mfNewAp_0 < 65536.0) and
            (((r_0 < mfNewAp_0) -> (0 = bYAp_0)) and
             ((mfNewAp_0 <= r_0) -> (1 = bYAp_0))) and
            (mfNewAp_0 = r_7)))))))))) and
   ((0.0 = 0.0) ->
    (((1 <> mnPbreath_0) ->
      ((gnApDStop_3 = gnApDStop_2) or
       (1 <> mbApLYRange_0) or
       (AP_AU_ALM_INT_0 < 2))) and
     ((1 = mnPbreath_0) ->
      ((1 = tenumRRMode_0) and
       (((r_2 < r_1) -> (0 = bApAlmCond_0)) and
        ((r_1 <= r_2) ->
         (((1 <> gbOxyMonS_0) -> (0 = bApAlmCond_0)) and
          ((1 = gbOxyMonS_0) ->
           (((0 <> gbOxyAdvS_0) -> (0 = bApAlmCond_0)) and
            ((0 = gbOxyAdvS_0) -> (1 = bApAlmCond_0))))))) and
       (((1 <> bApAlmCond_0) -> (gnApDStop_3 = gnApDStop_0)) and
        ((1 = bApAlmCond_0) ->
         ((gnApDStop_1 = gnApDStop_0) and
          (((r_3 <= r_2) -> (gnApDStop_3 = gnApDStop_1)) and
           ((r_2 < r_3) ->
            ((gnApDStop_2 = gnApDStop_1) and
             ((gnApDStop_3 = gnApDStop_2) or
              (1 <> mbApLRRange_0) or
              (1 <> mbApLYRange_0) or
              (AP_AU_ALM_INT_0 < 2)) and
             (((fOxyValue_0 < r_4) -> (1 = mbApLYRange_0)) and
              ((r_4 <= fOxyValue_0) ->
               (((1 <> bYAp_0) -> (0 = mbApLYRange_0)) and
                ((1 = bYAp_0) ->
                 (((1 <> gbOxyMonS_0) -> (0 = mbApLYRange_0)) and
                  ((1 = gbOxyMonS_0) ->
                   (((0 <> gbOxyAdvS_0) ->
                     (0 = mbApLYRange_0)) and
                    ((0 = gbOxyAdvS_0) ->
                     (1 = mbApLYRange_0))))))))) and
             (((r_5 <= r_2) -> (1 = mbApLRRange_0)) and
              ((r_2 < r_5) ->
               (((fOxyValue_0 < r_6) -> (1 = mbApLRRange_0)) and
                ((r_6 <= fOxyValue_0) ->
                 (((1 <> bRAp_0) -> (0 = mbApLRRange_0)) and
                  ((1 = bRAp_0) ->
                   (((1 <> gbOxyMonS_0) -> (0 = mbApLRRange_0)) and
                    ((1 = gbOxyMonS_0) ->
                     (((0 <> gbOxyAdvS_0) ->
                       (0 = mbApLRRange_0)) and
                      ((0 = gbOxyAdvS_0) -> (1 = mbApLRRange_0))))))))))) and
             (((fOxyValue_0 < r_6) -> (0 = bRAp_0)) and
              ((r_6 <= fOxyValue_0) ->
               (((-1.0) < mfNewAp_2) and (mfNewAp_2 < 65536.0) and
                (((r_2 < mfNewAp_2) -> (0 = bRAp_0)) and
                 ((mfNewAp_2 <= r_2) -> (1 = bRAp_0)))))) and
             ((fOxyValue_0 <= r_4) or
              (((-1.0) < mfNewAp_1) and (mfNewAp_1 < 65536.0) and
               (mfNewAp_1 = r_7))) and
             (((fOxyValue_0 < r_4) -> (0 = bYAp_0)) and
              ((r_4 <= fOxyValue_0) ->
               (((-1.0) < mfNewAp_0) and (mfNewAp_0 < 65536.0) and
                (((r_2 < mfNewAp_0) -> (0 = bYAp_0)) and
                 ((mfNewAp_0 <= r_2) -> (1 = bYAp_0))) and
                (mfNewAp_0 = r_7))))))))))))))) ->
  (1 = tenumRRMode_0)