53 lines
1.3 KiB
Sieve
53 lines
1.3 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.CheckAndAppendOrigin
|
|
|
|
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 301:
|
|
|
|
procedure_checkandappendorigin_1.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 303:
|
|
|
|
procedure_checkandappendorigin_2.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to run-time check associated with statement of line 307:
|
|
|
|
procedure_checkandappendorigin_3.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from start to finish:
|
|
|
|
procedure_checkandappendorigin_4.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_checkandappendorigin_5.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_checkandappendorigin_6.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
procedure_checkandappendorigin_7.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|