*****************************************************************************
                       Semantic Analysis of SPARK Text
                             Examiner GPL Edition

*****************************************************************************



SPARK Simplifier GPL 2012
Copyright (C) 2012 Altran Praxis Limited, Bath, U.K.

procedure Process_Dns_Request.Process_Response_Cname




For path(s) from start to run-time check associated with statement of line 983:

procedure_process_response_cname_1.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 984:

procedure_process_response_cname_2.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 985:

procedure_process_response_cname_3.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 985:

procedure_process_response_cname_4.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 986:

procedure_process_response_cname_5.
*** true .          /* all conclusions proved */


For path(s) from start to precondition check associated with statement of line 
          988:

procedure_process_response_cname_6.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 990:

procedure_process_response_cname_7.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 991:

procedure_process_response_cname_8.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 993:

procedure_process_response_cname_9.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 994:

procedure_process_response_cname_10.
*** true .          /* all conclusions proved */


For path(s) from start to precondition check associated with statement of line 
          996:

procedure_process_response_cname_11.
*** true .          /* all conclusions proved */


For path(s) from start to precondition check associated with statement of line 
          997:

procedure_process_response_cname_12.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 998:

procedure_process_response_cname_13.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 1000:

procedure_process_response_cname_14.
*** true .          /* all conclusions proved */


procedure_process_response_cname_15.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 1002:

procedure_process_response_cname_16.
*** true .          /* all conclusions proved */


procedure_process_response_cname_17.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 1003:

procedure_process_response_cname_18.
*** true .          /* all conclusions proved */


procedure_process_response_cname_19.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 1005 to run-time check associated with 
          statement of line 1003:

procedure_process_response_cname_20.
*** true .          /* all conclusions proved */


For path(s) from start to assertion of line 1005:

procedure_process_response_cname_21.
*** true .          /* all conclusions proved */


procedure_process_response_cname_22.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 1005 to assertion of line 1005:

procedure_process_response_cname_23.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 1005 to run-time check associated with 
          statement of line 1010:

procedure_process_response_cname_24.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 1005 to run-time check associated with 
          statement of line 1011:

procedure_process_response_cname_25.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 1005 to run-time check associated with 
          statement of line 1012:

procedure_process_response_cname_26.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 1014:

procedure_process_response_cname_27.
*** true .          /* all conclusions proved */


procedure_process_response_cname_28.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 1005 to run-time check associated with 
          statement of line 1014:

procedure_process_response_cname_29.
*** true .          /* all conclusions proved */


For path(s) from start to run-time check associated with statement of line 1015:

procedure_process_response_cname_30.
*** true .   /* contradiction within hypotheses. */



procedure_process_response_cname_31.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 1005 to run-time check associated with 
          statement of line 1015:

procedure_process_response_cname_32.
*** true .          /* all conclusions proved */


For path(s) from start to finish:

procedure_process_response_cname_33.
*** true .   /* contradiction within hypotheses. */



procedure_process_response_cname_34.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 1005 to finish:

procedure_process_response_cname_35.
*** true .          /* all conclusions proved */


