Skip to content

Commit a492935

Browse files
committed
Add a smaller jsr test
This one is build from raw assembly and checks that the generated cfg (or at least, its nodes) matches expectations.
1 parent c90295b commit a492935

File tree

3 files changed

+41
-0
lines changed

3 files changed

+41
-0
lines changed

regression/cbmc-java/jsr2/test.class

199 Bytes
Binary file not shown.

regression/cbmc-java/jsr2/test.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
test.class
3+
--show-goto-functions
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
Labels: pc3
7+
Labels: pc6
8+
Labels: pc9
9+
Labels: pc12
10+
Labels: pc13
11+
--
12+
\\"statement\\" (\\"jsr\\")
13+
\\"statement\\" (\\"ret\\")

regression/cbmc-java/jsr2/test.j

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
; This is Jasmin assembler syntax-- see http://jasmin.sourceforge.net/guide.html or apt-get install jasmin-sable
2+
3+
.class public test
4+
.super java/lang/Object
5+
6+
; standard initializer
7+
.method public <init>()V
8+
aload_0
9+
invokenonvirtual java/lang/Object/<init>()V
10+
return
11+
.end method
12+
13+
.method public static main()V
14+
.limit locals 4
15+
.limit stack 1
16+
goto runsrs
17+
sr1:
18+
astore_0
19+
ret 0
20+
runsrs:
21+
jsr sr1
22+
jsr sr2
23+
return
24+
sr2:
25+
astore_3
26+
ret 3
27+
.end method
28+

0 commit comments

Comments
 (0)