502 lines
12 KiB
Sieve
502 lines
12 KiB
Sieve
*****************************************************************************
|
|
Semantic Analysis of SPARK Text
|
|
Examiner GPL Edition
|
|
|
|
*****************************************************************************
|
|
|
|
|
|
|
|
SPARK Simplifier GPL 2011
|
|
Copyright (C) 2011 Altran Praxis Limited, Bath, U.K.
|
|
|
|
function Parser_Utilities.convertIpv6
|
|
|
|
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 857:
|
|
|
|
function_convertipv6_1.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 858:
|
|
|
|
function_convertipv6_2.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 859:
|
|
|
|
function_convertipv6_3.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 860:
|
|
|
|
function_convertipv6_4.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to assertion of line 863:
|
|
|
|
function_convertipv6_5.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to assertion of line 863:
|
|
|
|
function_convertipv6_6.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_7.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_8.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 864:
|
|
|
|
function_convertipv6_9.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 865:
|
|
|
|
function_convertipv6_10.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 866:
|
|
|
|
function_convertipv6_11.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 867:
|
|
|
|
function_convertipv6_12.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 868:
|
|
|
|
function_convertipv6_13.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 868:
|
|
|
|
function_convertipv6_14.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 869:
|
|
|
|
function_convertipv6_15.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 871:
|
|
|
|
function_convertipv6_16.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 872:
|
|
|
|
function_convertipv6_17.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 873:
|
|
|
|
function_convertipv6_18.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 874:
|
|
|
|
function_convertipv6_19.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 875:
|
|
|
|
function_convertipv6_20.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 877:
|
|
|
|
function_convertipv6_21.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_22.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_23.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 881:
|
|
|
|
function_convertipv6_24.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 881:
|
|
|
|
function_convertipv6_25.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_26.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_27.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 882:
|
|
|
|
function_convertipv6_28.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 882:
|
|
|
|
function_convertipv6_29.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_30.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_31.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 883:
|
|
|
|
function_convertipv6_32.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 883:
|
|
|
|
function_convertipv6_33.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_34.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_35.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 884:
|
|
|
|
function_convertipv6_36.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 884:
|
|
|
|
function_convertipv6_37.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_38.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_39.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 885:
|
|
|
|
function_convertipv6_40.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 885:
|
|
|
|
function_convertipv6_41.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_42.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_43.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 886:
|
|
|
|
function_convertipv6_44.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 886:
|
|
|
|
function_convertipv6_45.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_46.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_47.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 886:
|
|
|
|
function_convertipv6_48.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 886:
|
|
|
|
function_convertipv6_49.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_50.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_51.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 887:
|
|
|
|
function_convertipv6_52.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 887:
|
|
|
|
function_convertipv6_53.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_54.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_55.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 888:
|
|
|
|
function_convertipv6_56.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 888:
|
|
|
|
function_convertipv6_57.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_58.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_59.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 890:
|
|
|
|
function_convertipv6_60.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to run-time check associated with
|
|
statement of line 890:
|
|
|
|
function_convertipv6_61.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_62.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_63.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to finish:
|
|
|
|
function_convertipv6_64.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_65.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_66.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_67.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_68.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_69.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_70.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_71.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 863 to finish:
|
|
|
|
function_convertipv6_72.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_73.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_74.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_75.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_76.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_77.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_78.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_79.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_80.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_81.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_82.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_83.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_84.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_85.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_86.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_87.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_88.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_89.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_90.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_91.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_92.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_93.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_94.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
function_convertipv6_95.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|