Skip to content

Commit 4428ed4

Browse files
author
thk123
committed
Add reference to documentation about arrays
1 parent e51b182 commit 4428ed4

File tree

1 file changed

+11
-4
lines changed

1 file changed

+11
-4
lines changed

jbmc/src/java_bytecode/README.md

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,10 @@ This module provides a front end for Java.
77

88
To be documented.
99

10+
\section java-bytecode-array-representation How are Java arrays represented in GOTO
11+
12+
To be documented.
13+
1014
\section java-bytecode-object-factory Object Factory
1115

1216
To be documented.
@@ -86,10 +90,13 @@ operation.
8690
8791
These are converted by \ref remove_java_newt::lower_java_new_array
8892
89-
See TODO: DOC-20: for details on how arrays are represented in codet. It first
90-
allocates the array object as with a regular Java object. Then the size
91-
component is set to be the size of the array and the data component is also
92-
initialized.
93+
See \ref java-bytecode-array-representation for details on how arrays are
94+
represented in codet.
95+
96+
A `newarray` is represented as:
97+
- an allocation of the array object (the same as with a regular Java object).
98+
- Initialize the size component
99+
- Initialize the data component
93100
94101
For example the following Java:
95102

0 commit comments

Comments
 (0)