441 lines
10 KiB
Sieve
441 lines
10 KiB
Sieve
*****************************************************************************
|
|
Semantic Analysis of SPARK Text
|
|
Examiner GPL Edition
|
|
|
|
*****************************************************************************
|
|
|
|
|
|
|
|
SPARK Simplifier GPL 2011
|
|
Copyright (C) 2011 Altran Praxis Limited, Bath, U.K.
|
|
|
|
procedure Parser_Utilities.AddToKeyR
|
|
|
|
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 734:
|
|
|
|
procedure_addtokeyr_1.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 735:
|
|
|
|
procedure_addtokeyr_2.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 736 to run-time check associated with
|
|
statement of line 735:
|
|
|
|
procedure_addtokeyr_3.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to assertion of line 736:
|
|
|
|
procedure_addtokeyr_4.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 736 to assertion of line 736:
|
|
|
|
procedure_addtokeyr_5.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 736 to run-time check associated with
|
|
statement of line 737:
|
|
|
|
procedure_addtokeyr_6.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 741:
|
|
|
|
procedure_addtokeyr_7.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 736 to run-time check associated with
|
|
statement of line 741:
|
|
|
|
procedure_addtokeyr_8.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 742:
|
|
|
|
procedure_addtokeyr_9.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 736 to run-time check associated with
|
|
statement of line 742:
|
|
|
|
procedure_addtokeyr_10.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 743 to run-time check associated with
|
|
statement of line 742:
|
|
|
|
procedure_addtokeyr_11.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to assertion of line 743:
|
|
|
|
procedure_addtokeyr_12.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 736 to assertion of line 743:
|
|
|
|
procedure_addtokeyr_13.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 743 to assertion of line 743:
|
|
|
|
procedure_addtokeyr_14.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 743 to run-time check associated with
|
|
statement of line 744:
|
|
|
|
procedure_addtokeyr_15.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 748:
|
|
|
|
procedure_addtokeyr_16.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 736 to run-time check associated with
|
|
statement of line 748:
|
|
|
|
procedure_addtokeyr_17.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 743 to run-time check associated with
|
|
statement of line 748:
|
|
|
|
procedure_addtokeyr_18.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 752:
|
|
|
|
procedure_addtokeyr_19.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 736 to run-time check associated with
|
|
statement of line 752:
|
|
|
|
procedure_addtokeyr_20.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 743 to run-time check associated with
|
|
statement of line 752:
|
|
|
|
procedure_addtokeyr_21.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 752:
|
|
|
|
procedure_addtokeyr_22.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 736 to run-time check associated with
|
|
statement of line 752:
|
|
|
|
procedure_addtokeyr_23.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 743 to run-time check associated with
|
|
statement of line 752:
|
|
|
|
procedure_addtokeyr_24.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to assertion of line 753:
|
|
|
|
procedure_addtokeyr_25.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 736 to assertion of line 753:
|
|
|
|
procedure_addtokeyr_26.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 743 to assertion of line 753:
|
|
|
|
procedure_addtokeyr_27.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 753 to assertion of line 753:
|
|
|
|
procedure_addtokeyr_28.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 753 to run-time check associated with
|
|
statement of line 756:
|
|
|
|
procedure_addtokeyr_29.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 759:
|
|
|
|
procedure_addtokeyr_30.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 736 to run-time check associated with
|
|
statement of line 759:
|
|
|
|
procedure_addtokeyr_31.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 743 to run-time check associated with
|
|
statement of line 759:
|
|
|
|
procedure_addtokeyr_32.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 753 to run-time check associated with
|
|
statement of line 759:
|
|
|
|
procedure_addtokeyr_33.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 765:
|
|
|
|
procedure_addtokeyr_34.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_35.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 736 to run-time check associated with
|
|
statement of line 765:
|
|
|
|
procedure_addtokeyr_36.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_37.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 743 to run-time check associated with
|
|
statement of line 765:
|
|
|
|
procedure_addtokeyr_38.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_39.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 753 to run-time check associated with
|
|
statement of line 765:
|
|
|
|
procedure_addtokeyr_40.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to precondition check associated with statement of line
|
|
766:
|
|
|
|
procedure_addtokeyr_41.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_42.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 736 to precondition check associated with
|
|
statement of line 766:
|
|
|
|
procedure_addtokeyr_43.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_44.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 743 to precondition check associated with
|
|
statement of line 766:
|
|
|
|
procedure_addtokeyr_45.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_46.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 753 to precondition check associated with
|
|
statement of line 766:
|
|
|
|
procedure_addtokeyr_47.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 766:
|
|
|
|
procedure_addtokeyr_48.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_49.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 736 to run-time check associated with
|
|
statement of line 766:
|
|
|
|
procedure_addtokeyr_50.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_51.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 743 to run-time check associated with
|
|
statement of line 766:
|
|
|
|
procedure_addtokeyr_52.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_53.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 753 to run-time check associated with
|
|
statement of line 766:
|
|
|
|
procedure_addtokeyr_54.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to finish:
|
|
|
|
procedure_addtokeyr_55.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_56.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_57.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_58.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_59.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_60.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 736 to finish:
|
|
|
|
procedure_addtokeyr_61.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_62.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_63.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_64.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_65.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_66.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 743 to finish:
|
|
|
|
procedure_addtokeyr_67.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_68.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_69.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_70.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_71.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_72.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 753 to finish:
|
|
|
|
procedure_addtokeyr_73.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_74.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_addtokeyr_75.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|