(* ---------------------------------------------------------- *)
(* --- Post-condition (file string.h, line 65) in 'strlen' --- *)
(* ---------------------------------------------------------- *)
theory VCstrlen_post
  
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 = 8 * x_1 in
  let x_3 = s_0.base in
  let x_4 = 8 * x_0 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 (((-8) * x_0) + x_2))) ->
  (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. (0 <= i_2) -> ((i_2 + x_4) < x_2) ->
   (0 <> mchar_0[{ s_0 with offset = i_2 + x_1 }])) ->
  (exists i_2 : int. ((p_Length_of_str_is mchar_0 malloc_0 s_0 i_2)) /\
   (x_2 = (i_2 + x_4)))

end

(* ---------------------------------------------------------- *)
(* --- Preservation of Invariant (file strlen.c, line 9)  --- *)
(* ---------------------------------------------------------- *)
theory VCstrlen_loop_inv_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. (0 <= i_3) -> ((i_3 + (8 * x_2)) < (8 * x_1)) ->
   (0 <> mchar_0[{ s_0 with offset = i_3 + x_1 }])) ->
  (((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_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_2_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 = 8 * (ss_0.offset) in
  let x_1 = s_0.offset in
  let x_2 = 8 * x_1 in
  let x_3 = s_0.base in
  let x_4 = mchar_0[{ s_0 with offset = i_2 + 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)) ->
  ((9 + i_2 + x_0) <= 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_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_3 : int. (0 <= i_3) -> ((i_3 + x_0) < x_2) ->
   (0 <> mchar_0[{ s_0 with offset = i_3 + x_1 }])) ->
  (0 <> x_4)

end

(* ---------------------------------------------------------- *)
(* --- Assertion 'rte,mem_access' (file strlen.c, line 14) --- *)
(* ---------------------------------------------------------- *)
theory VCstrlen_assert_rte_mem_access
  
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. (0 <= i_2) ->
   ((i_2 + (8 * (ss_0.offset))) < (8 * x_1)) ->
   (0 <> mchar_0[{ s_0 with offset = i_2 + x_1 }])) ->
  ((valid_rd malloc_0 ss_0 1))

end

(* ---------------------------------------------------------- *)
(* --- Decreasing of Loop variant at loop (file strlen.c, line 14) --- *)
(* ---------------------------------------------------------- *)
theory VCstrlen_loop_term_decrease
  
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:Decreasing 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_0 ss_0 : addr.
  let x_0 = s_0.base in
  let x_1 = s_0.offset in
  (0 = mchar_0[ss_0]) \/
  (not((linked malloc_0))) \/
  (not((sconst mchar_0))) \/
  (not((addr_le s_0 ss_0))) \/
  (not((valid_rd malloc_0 ss_0 1))) \/
  (not(exists i_3 : int. (p_Length_of_str_is mchar_0 malloc_0 s_0 i_3))) \/
  (not((is_sint8 mchar_0[{ s_0 with offset = i_2 + x_1 }]))) \/
  (not((is_sint8 mchar_0[{ s_0 with offset = i_1 + x_1 }]))) \/
  (not((is_sint8 mchar_0[{ s_0 with offset = i_0 + x_1 }]))) \/
  (not((addr_le ss_0 ({ s_0 with offset = x_1 + ((l_Length mchar_0 s_0)) })))) \/
  (not(forall i_3 : int. (0 <= i_3) ->
       ((i_3 + (8 * (ss_0.offset))) < (8 * x_1)) ->
       (0 <> mchar_0[{ s_0 with offset = i_3 + x_1 }])))

end

(* ---------------------------------------------------------- *)
(* --- Positivity of Loop variant at loop (file strlen.c, line 14) --- *)
(* ---------------------------------------------------------- *)
theory VCstrlen_loop_term_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 = (l_Length mchar_0 s_0) in
  let x_3 = 8 * (ss_0.offset) in
  let x_4 = 8 * x_1 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_1 + x_2 }))) ->
  (forall i_3 : int. (0 <= i_3) -> ((i_3 + x_3) < x_4) ->
   (0 <> mchar_0[{ s_0 with offset = i_3 + x_1 }])) ->
  (x_4 <= (x_3 + x_2))

end