35 lines
816 B
Sieve
35 lines
816 B
Sieve
*****************************************************************************
|
|
Semantic Analysis of SPARK Text
|
|
Examiner GPL Edition
|
|
|
|
*****************************************************************************
|
|
|
|
|
|
|
|
SPARK Simplifier GPL 2011
|
|
Copyright (C) 2011 Altran Praxis Limited, Bath, U.K.
|
|
|
|
task_type Tcp_Dns_Package.Tcp_Dns_Task
|
|
|
|
|
|
|
|
|
|
For path(s) from start to assertion of line 40:
|
|
|
|
task_type_tcp_dns_task_1.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 40 to assertion of line 40:
|
|
|
|
task_type_tcp_dns_task_2.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|
|
For path(s) from assertion of line 40 to finish:
|
|
|
|
task_type_tcp_dns_task_3.
|
|
*** true . /* all conclusions proved */
|
|
|
|
|