Skip to content

Commit fa6ed33

Browse files
author
thk123
committed
Add reference to documentation about arrays
1 parent 33c5d51 commit fa6ed33

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.
@@ -167,10 +171,13 @@ operation.
167171
168172
These are converted by \ref remove_java_newt::lower_java_new_array
169173
170-
See TODO: DOC-20: for details on how arrays are represented in codet. It first
171-
allocates the array object as with a regular Java object. Then the size
172-
component is set to be the size of the array and the data component is also
173-
initialized.
174+
See \ref java-bytecode-array-representation for details on how arrays are
175+
represented in codet.
176+
177+
A `newarray` is represented as:
178+
- an allocation of the array object (the same as with a regular Java object).
179+
- Initialize the size component
180+
- Initialize the data component
174181
175182
For example the following Java:
176183

0 commit comments

Comments
 (0)