Skip to content

Commit

Permalink
More test cases
Browse files Browse the repository at this point in the history
Signed-off-by: Alan Jowett <[email protected]>
  • Loading branch information
Alan Jowett committed Nov 5, 2024
1 parent 7589b6a commit 5390b2b
Showing 1 changed file with 26 additions and 0 deletions.
26 changes: 26 additions & 0 deletions test-data/loop.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -414,3 +414,29 @@ post:

messages:
- "0: Loop counter is too large (pc[0] < 100000)"

---
# Check for case where the verifier incorrectly assumes that an instruction is the head of a loop
# when it is not. Verify that it still computes the correct post-state.
test-case: non-loop backwards jump
options: ["termination"]

pre: [r0.type=number]
code:
<start>: |
r0 = 1
goto <two>
<one>: |
r0 += 1
exit
<two>: |
r0 += 1
goto <one>
post:
- "r0.svalue=3"
- "r0.uvalue=3"
- "r0.type=number"
- pc[2]=1

messages:

0 comments on commit 5390b2b

Please sign in to comment.