(* ---------------------------------------------------------- *)
(* --- Post-condition (file string.h, line 65) in 'strlen' --- *)
(* ---------------------------------------------------------- *)
theory VCstrlen_post_2

use import bool.Bool
use import int.Int
use import int.ComputerDivision
use import real.RealInfix
use import qed.Arith
use import map.Map
use import memory.Memory
use import cint.Cint
use import Axiomatic.Axiomatic
use import A_Length.A_Length

goal WP "expl:Post-condition (file string.h, line 65) in 'strlen'":
  forall i_1 i_0 : int.
  forall malloc_0 : map int int.
  forall mchar_0 : map addr int.
  forall s_0 ss_0 : addr.
  let x_0 = ss_0.offset in
  let x_1 = s_0.offset in
  let x_2 = s_0.base in
  (0 = mchar_0[ss_0]) ->
  ((linked malloc_0)) ->
  ((sconst mchar_0)) ->
  ((addr_le s_0 ss_0)) ->
  ((valid_rd malloc_0 ss_0 1)) ->
  ((is_sint32 (x_0 - x_1))) ->
  (exists i_2 : int. (p_Length_of_str_is mchar_0 malloc_0 s_0 i_2)) ->
  ((is_sint8 mchar_0[{ s_0 with offset = i_1 + x_1 }])) ->
  ((is_sint8 mchar_0[{ s_0 with offset = i_0 + x_1 }])) ->
  ((addr_le ss_0 ({ s_0 with offset = x_1 + ((l_Length mchar_0 s_0)) }))) ->
  (forall i_2 : int. let x_3 = i_2 + x_1 in (0 <= i_2) -> (x_3 < x_0) ->
   (0 <> mchar_0[{ s_0 with offset = x_3 }])) ->
  (exists i_2 : int. (x_0 = (i_2 + x_1)) /\
   ((p_Length_of_str_is mchar_0 malloc_0 s_0 i_2)))

end

(* ---------------------------------------------------------- *)
(* --- Preservation of Invariant (file strlen.c, line 9)  --- *)
(* ---------------------------------------------------------- *)
theory VCstrlen_loop_inv_4_preserved

use import bool.Bool
use import int.Int
use import int.ComputerDivision
use import real.RealInfix
use import qed.Arith
use import map.Map
use import memory.Memory
use import Axiomatic.Axiomatic
use import cint.Cint
use import A_Length.A_Length

goal WP "expl:Preservation of Invariant (file strlen.c, line 9)":
  forall i_2 i_1 i_0 : int.
  forall malloc_0 : map int int.
  forall mchar_0 : map addr int.
  forall s_0 ss_0 : addr.
  let x_0 = s_0.base in
  let x_1 = s_0.offset in
  let a_0 = { s_0 with offset = x_1 + ((l_Length mchar_0 s_0)) } in
  let x_2 = ss_0.offset in
  let a_1 = { ss_0 with offset = 1 + x_2 } in
  (0 <> mchar_0[ss_0]) ->
  ((linked malloc_0)) ->
  ((sconst mchar_0)) ->
  ((addr_le s_0 ss_0)) ->
  ((valid_rd malloc_0 ss_0 1)) ->
  (exists i_3 : int. (p_Length_of_str_is mchar_0 malloc_0 s_0 i_3)) ->
  ((is_sint8 mchar_0[{ s_0 with offset = i_2 + x_1 }])) ->
  ((is_sint8 mchar_0[{ s_0 with offset = i_1 + x_1 }])) ->
  ((is_sint8 mchar_0[{ s_0 with offset = i_0 + x_1 }])) ->
  ((addr_le ss_0 a_0)) ->
  (forall i_3 : int. let x_3 = i_3 + x_1 in (0 <= i_3) -> (x_3 < x_2) ->
   (0 <> mchar_0[{ s_0 with offset = x_3 }])) ->
  (((addr_le s_0 a_1)) /\ ((addr_le a_1 a_0)))

end

(* ---------------------------------------------------------- *)
(* --- Establishment of Invariant (file strlen.c, line 9) --- *)
(* ---------------------------------------------------------- *)
theory VCstrlen_loop_inv_4_established

use import bool.Bool
use import int.Int
use import int.ComputerDivision
use import real.RealInfix
use import qed.Arith
use import map.Map
use import memory.Memory
use import Axiomatic.Axiomatic
use import cint.Cint
use import A_Length.A_Length

goal WP "expl:Establishment of Invariant (file strlen.c, line 9)":
  forall i_1 i_0 : int.
  forall malloc_0 : map int int.
  forall mchar_0 : map addr int.
  forall s_0 : addr.
  let x_0 = s_0.base in
  let x_1 = s_0.offset in
  ((linked malloc_0)) ->
  ((sconst mchar_0)) ->
  (exists i_2 : int. (p_Length_of_str_is mchar_0 malloc_0 s_0 i_2)) ->
  ((is_sint8 mchar_0[{ s_0 with offset = i_1 + x_1 }])) ->
  ((is_sint8 mchar_0[{ s_0 with offset = i_0 + x_1 }])) ->
  (((addr_le s_0 s_0)) /\
   ((addr_le s_0 ({ s_0 with offset = x_1 + ((l_Length mchar_0 s_0)) }))))

end

(* ---------------------------------------------------------- *)
(* --- Preservation of Invariant (file strlen.c, line 10) --- *)
(* ---------------------------------------------------------- *)
theory VCstrlen_loop_inv_5_preserved

use import bool.Bool
use import int.Int
use import int.ComputerDivision
use import real.RealInfix
use import qed.Arith
use import map.Map
use import memory.Memory
use import Axiomatic.Axiomatic
use import cint.Cint
use import A_Length.A_Length

goal WP "expl:Preservation of Invariant (file strlen.c, line 10)":
  forall i_2 i_1 i_0 : int.
  forall malloc_0 : map int int.
  forall mchar_0 : map addr int.
  forall s_0 ss_0 : addr.
  let x_0 = s_0.offset in
  let x_1 = i_2 + x_0 in
  let x_2 = ss_0.offset in
  let x_3 = s_0.base in
  let x_4 = mchar_0[{ s_0 with offset = x_1 }] in
  (0 <= i_2) ->
  (0 <> mchar_0[ss_0]) ->
  ((linked malloc_0)) ->
  ((sconst mchar_0)) ->
  ((addr_le s_0 ss_0)) ->
  ((valid_rd malloc_0 ss_0 1)) ->
  (x_1 <= x_2) ->
  (exists i_3 : int. (p_Length_of_str_is mchar_0 malloc_0 s_0 i_3)) ->
  ((is_sint8 x_4)) ->
  ((is_sint8 mchar_0[{ s_0 with offset = i_1 + x_0 }])) ->
  ((is_sint8 mchar_0[{ s_0 with offset = i_0 + x_0 }])) ->
  ((addr_le ss_0 ({ s_0 with offset = x_0 + ((l_Length mchar_0 s_0)) }))) ->
  (forall i_3 : int. let x_5 = i_3 + x_0 in (0 <= i_3) -> (x_5 < x_2) ->
   (0 <> mchar_0[{ s_0 with offset = x_5 }])) ->
  (0 <> x_4)

end

(* ---------------------------------------------------------- *)
(* --- Assertion 'rte,mem_access' (file strlen.c, line 14) --- *)
(* ---------------------------------------------------------- *)
theory VCstrlen_assert_rte_mem_access_2

use import bool.Bool
use import int.Int
use import int.ComputerDivision
use import real.RealInfix
use import qed.Arith
use import map.Map
use import memory.Memory
use import Axiomatic.Axiomatic
use import cint.Cint
use import A_Length.A_Length

goal WP "expl:Assertion 'rte,mem_access' (file strlen.c, line 14)":
  forall i_1 i_0 : int.
  forall malloc_0 : map int int.
  forall mchar_0 : map addr int.
  forall s_0 ss_0 : addr.
  let x_0 = s_0.base in
  let x_1 = s_0.offset in
  ((linked malloc_0)) ->
  ((sconst mchar_0)) ->
  ((addr_le s_0 ss_0)) ->
  (exists i_2 : int. (p_Length_of_str_is mchar_0 malloc_0 s_0 i_2)) ->
  ((is_sint8 mchar_0[{ s_0 with offset = i_1 + x_1 }])) ->
  ((is_sint8 mchar_0[{ s_0 with offset = i_0 + x_1 }])) ->
  ((addr_le ss_0 ({ s_0 with offset = x_1 + ((l_Length mchar_0 s_0)) }))) ->
  (forall i_2 : int. let x_2 = i_2 + x_1 in (0 <= i_2) ->
   (x_2 < (ss_0.offset)) -> (0 <> mchar_0[{ s_0 with offset = x_2 }])) ->
  ((valid_rd malloc_0 ss_0 1))

end

(* ---------------------------------------------------------- *)
(* --- Positivity of Loop variant at loop (file strlen.c, line 14) --- *)
(* ---------------------------------------------------------- *)
theory VCstrlen_loop_term_2_positive

use import bool.Bool
use import int.Int
use import int.ComputerDivision
use import real.RealInfix
use import qed.Arith
use import map.Map
use import memory.Memory
use import Axiomatic.Axiomatic
use import cint.Cint
use import A_Length.A_Length

goal WP "expl:Positivity of Loop variant at loop (file strlen.c, line 14)":
  forall i_2 i_1 i_0 : int.
  forall malloc_0 : map int int.
  forall mchar_0 : map addr int.
  forall s_1 s_0 ss_0 : addr.
  let x_0 = s_0.base in
  let x_1 = s_0.offset in
  let x_2 = x_1 + ((l_Length mchar_0 s_0)) in
  let x_3 = ss_0.offset in
  (0 <> mchar_0[ss_0]) ->
  ((linked malloc_0)) ->
  ((sconst mchar_0)) ->
  ((addr_le s_0 ss_0)) ->
  ((valid_rd malloc_0 ss_0 1)) ->
  (exists i_3 : int. (p_Length_of_str_is mchar_0 malloc_0 s_0 i_3)) ->
  ((is_sint8 mchar_0[{ s_1 with offset = i_2 + (s_1.offset) }])) ->
  ((is_sint8 mchar_0[{ s_0 with offset = i_1 + x_1 }])) ->
  ((is_sint8 mchar_0[{ s_0 with offset = i_0 + x_1 }])) ->
  ((addr_le ss_0 ({ s_0 with offset = x_2 }))) ->
  (forall i_3 : int. let x_4 = i_3 + x_1 in (0 <= i_3) -> (x_4 < x_3) ->
   (0 <> mchar_0[{ s_0 with offset = x_4 }])) ->
  (x_3 <= x_2)

end