*****************************************************************************
                       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_RRSIG




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

procedure_create_response_rrsig_1.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_2.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_3.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_4.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_5.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_6.
*** true .          /* all conclusions proved */


procedure_create_response_rrsig_7.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_8.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_9.
*** true .          /* all conclusions proved */


procedure_create_response_rrsig_10.
*** true .   /* contradiction within hypotheses. */



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

procedure_create_response_rrsig_11.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_12.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_13.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_14.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_15.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_16.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_17.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_18.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_19.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_20.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_21.
*** true .          /* all conclusions proved */


procedure_create_response_rrsig_22.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_23.
*** true .          /* all conclusions proved */


procedure_create_response_rrsig_24.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_25.
*** true .          /* all conclusions proved */


procedure_create_response_rrsig_26.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_27.
*** true .          /* all conclusions proved */


procedure_create_response_rrsig_28.
*** true .          /* all conclusions proved */


For path(s) from start to finish:

procedure_create_response_rrsig_29.
*** true .          /* all conclusions proved */


procedure_create_response_rrsig_30.
*** true .          /* all conclusions proved */


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

procedure_create_response_rrsig_31.
*** true .          /* all conclusions proved */


procedure_create_response_rrsig_32.
*** true .          /* all conclusions proved */


