*****************************************************************************
                       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.Create_Response_DNSKEY




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

procedure_create_response_dnskey_1.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_2.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_3.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_4.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_5.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_6.
*** true .          /* all conclusions proved */


procedure_create_response_dnskey_7.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_8.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_9.
*** true .          /* all conclusions proved */


procedure_create_response_dnskey_10.
*** true .   /* contradiction within hypotheses. */



For path(s) from assertion of line 599 to precondition check associated with 
          statement of line 606:

procedure_create_response_dnskey_11.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_12.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_13.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_14.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_15.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 599 to precondition check associated with 
          statement of line 614:

procedure_create_response_dnskey_16.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_17.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_18.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_19.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_20.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_21.
*** true .          /* all conclusions proved */


procedure_create_response_dnskey_22.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_23.
*** true .          /* all conclusions proved */


procedure_create_response_dnskey_24.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_25.
*** true .          /* all conclusions proved */


procedure_create_response_dnskey_26.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_27.
*** true .          /* all conclusions proved */


procedure_create_response_dnskey_28.
*** true .          /* all conclusions proved */


For path(s) from start to finish:

procedure_create_response_dnskey_29.
*** true .          /* all conclusions proved */


procedure_create_response_dnskey_30.
*** true .          /* all conclusions proved */


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

procedure_create_response_dnskey_31.
*** true .          /* all conclusions proved */


procedure_create_response_dnskey_32.
*** true .          /* all conclusions proved */


