achiever.adb:19:18: info: add a contract to analyze it separately from calling contexts
achiever.adb:19:18: info: local subprogram "Do_Something" only analyzed in the context of calls
achiever.adb:19:18: warning: subprogram "Do_Something" has no effect
achiever.ads:24:31: warning: unused variable "St"
achiever.ads:25:31: warning: unused variable "Op"
achiever.ads:26:31: warning: unused variable "Before"
achiever.ads:27:31: warning: unused variable "After"
achiever.ads:30:27: warning: unused variable "St"
achiever.ads:31:27: warning: unused variable "Before"
achiever.ads:32:27: warning: unused variable "After"
achiever.ads:35:06: info: complete contract cases proved (CVC4: 1 VC)
achiever.ads:35:06: info: disjoint contract cases proved (CVC4: 1 VC)
achiever.ads:36:49: medium: contract case might fail
achiever.ads:44:45: info: contract case proved (CVC4: 1 VC; Trivial: 1 VC)
achiever.ads:47:08: info: postcondition proved (CVC4: 1 VC)
fault_manager.ads:3:14: warning: subprogram "Log_Direct_Failure" has no effect
main.adb:11:12: medium: "My_Internal_State" might not be initialized after elaboration of main program "Main"
main.adb:11:12: medium: "achiever.state_item" might not be initialized after elaboration of main program "Main"
sc_status_type.adb:18:07: info: initialization of "Result" proved
sc_status_type.ads:48:22: info: initialization of "This" proved
