You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: key.ui/src/main/resources/de/uka/ilkd/key/gui/help/functionExplanations.xml
+13-13Lines changed: 13 additions & 13 deletions
Original file line number
Diff line number
Diff line change
@@ -21,16 +21,16 @@ Java has the peculiarity of covariant array types. They allow an array assignmen
21
21
22
22
Integers are used to access the entries of entries within arrays stored on the heap. This function provides the injection of the integer domain into that of the type Field. It is ensured that this image of arr is disjoint from any defined field constant.
23
23
24
-
The array access a[i], for instance for an int-array a, becomes select<[int]>(heap, a, arr(i)).</entry>
24
+
The array access a[i], for instance for an int-array a, becomes select<[int]>(heap, a, arr(i)).</entry>
<entrykey="heap/heap">This program variable holds to the current heap state. Its type is Heap. Any assignment statement in a modality modifies the value of this program variable and any expression reading from the heap within a Java modality refers to the heap stored in this program variable.</entry>
36
36
@@ -48,13 +48,13 @@ It takes four arguments:
48
48
4. The value v which is to be written in the designated location.
49
49
The result is a heap which coincides with h in all locations but in (o,f), where v is stored.
50
50
In the theory of arrays, store is somtimes called "write".
51
-
The field java.lang.Object::$created cannot be updated using store; use "create".</entry>
51
+
The field java.lang.Object::#$created cannot be updated using store; use "create".</entry>
52
52
53
53
<entrykey="heap/create">This function modifies a heap by changing the createdness of one object.
54
54
It takes two arguments:
55
55
1. The heap h which is to be modified
56
56
2. The object reference o for the object which is to be set created.
57
-
The result is a heap which coincides with h in all locations but in (o,java.lang.Object::$created), which has been set to true.
57
+
The result is a heap which coincides with h in all locations but in (o,java.lang.Object::#$created), which has been set to true.
58
58
There is no means to modify a heap by setting the createdness of an object to false.</entry>
59
59
60
60
<entrykey="heap/anon">tbd</entry>
@@ -65,9 +65,9 @@ It takes three arguments:
65
65
2. The location set s whose locations are to be modified
66
66
4. The value v which is to be written in the designated locations.
67
67
The result is a heap which coincides with h in all locations but in the locations in s where v is stored.
68
-
The field java.lang.Object::$created> cannot be updated using memset; use "create".</entry>
68
+
The field java.lang.Object::#$created cannot be updated using memset; use "create".</entry>
0 commit comments