Skip to content
This repository was archived by the owner on May 22, 2023. It is now read-only.

Commit 8bcd451

Browse files
committed
add proof annotation
ref #80
1 parent 0b05cfe commit 8bcd451

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

Diff for: test/block_client/component.adb

+1
Original file line numberDiff line numberDiff line change
@@ -73,6 +73,7 @@ is
7373
begin
7474
if Block.Status (Request_Cache (R)) not in Block.Raw | Block.Error then
7575
D := (others => Character'Val (33 + Integer (Block.Start (Request_Cache (R)) mod 93)));
76+
-- PROOF: steps: 800, level: 2
7677
else
7778
if Componolit.Interfaces.Log.Initialized (Log) then
7879
Componolit.Interfaces.Log.Client.Warning (Log, "Failed to calculate content");

0 commit comments

Comments
 (0)