liquidjava/liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufferRefinements.java at 9c5cad933f35d068bdb50260d838c2c9ddaf26f0 · liquid-java/liquidjava · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
package testSuite.classes.bytebuf_error;

import liquidjava.specification.ExternalRefinementsFor;
import liquidjava.specification.Ghost;
import liquidjava.specification.Refinement;
import liquidjava.specification.StateRefinement;

import java.nio.ByteBuffer;


@Ghost("boolean arrayBacked")
@ExternalRefinementsFor("java.nio.ByteBuffer")
public interface ByteBufferRefinements {

    // ---- Backing array access ----

    @StateRefinement(to="_ ? arrayBacked() : !arrayBacked()")
    boolean hasArray();

    @StateRefinement(from="arrayBacked()")
    byte[] array();

    @StateRefinement(from="arrayBacked()")
    int arrayOffset();

    @Refinement("arrayBacked(_)")
    ByteBuffer wrap(byte[] array, int offset, int length);

    @Refinement("arrayBacked(_)")
    ByteBuffer wrap(byte[] array);

  }