Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- (* ---------------------------------------------------------- *)
- (* --- 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
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement