jMoped 2.0


	jMoped 2.0 - FAQs

Question 1: What is jMoped annotations?

Answer: Because jMoped is slow with integers that have many bits, jMoped annotations give you more control to tell which variables should have which bits apart from the default value on the plug-in view. See What is the annotation @Bits?.

top

Question 2: How can I use jMoped annotaions?

Answer: You need to include jmoped-translator.jar into your classpath. Goto Project -> Properties, select Java Build Path on the left, and then the tab Libraries in the middle. Click Add External JARs... and add the file jmoped-translator.jar.

top

Question 3: What is the annotation @Bits?

Answer: The annotaion @Bits is used for specifying bits of fields, parameters, local variables, and array elements. You will have to add jmoped-translator.jar into your classpath, and import the class Bits.

    import de.tum.in.jmoped.annotation.Bits;

Usage:

Fields: put @Bits just before field declarations. For example,
```
    @Bits({"2"})
    int a;
```
the field a will have two bits.
Parameters: put @Bits just before method declarations. There are two possibilities to refer to parameters: (1) by sequence (2) by name. To refer by sequence you need to give the bits in the same order as they appear in the method. For example,
```
    @Bits({"1", "2"})
    void m(int x, int y)
```
x and y will have 1 and 2 bits, repectively. Alternatively, you can refer to variables by names, e.g.
```
    @Bits({"y=2", "x=1"})
    void m(int x, int y)
```
which yields the same result as above.
Local variables: put @Bits just before method declarations and refer to the variables by their names, as in the case of parameters. For example,
```
    @Bits({"z=1"})
    void m() {
      int z;
    }
```
z will have 1 bit.
Array elements: put @Bits just before method or field declarations and refer to the variables by their names followed by []. For example,
```
    @Bits({"u[]=1", "v[]=2"})
    void m(int[] u) {
      int[] v;
    }
```
each element of the arrays u and v will have 1 and 2 bit, respectively.

Remark:

@Bits always takes an array of Strings as the only argument, and has no comma at the end.
If the bits of a variable are given twice, jMoped always takes the last one.
If w is an array, @Bits({"w=3", "w[]=1") means that the length of w has 3 bits (i.e. at most 7 elements), and each element of w has 1 bit.
The bits set by @Bits cannot be greater than the default bit in the progress view.
@Bits narrows down the scope of the analysis, which will make jMoped runs faster.

top

Question 4: What is the annotation @ArrayBits?

Answer: The annotaion @ArrayBits is used for specifying bits of array elements at class or method level. You will have to add pds.jar into your classpath, and import the class ArrayBits.

    import de.tum.in.jmoped.annotation.ArrayBits;

For example, by inserting

    @ArrayBits(1)

just before a class (or method) declaration means that the array elements will have just 1 bit for every array created in this class (or method).
Remark:

If both scopes are specified, the one at method level takes the priority.

top

Question 5: How to specify the bit sizes of a field?

Answer: See What is the annotation @Bits?. Alternatively, jMoped offers the annotations @FieldBits exclusively for this purpose. You will have to add pds.jar into your classpath, and import the class FieldBits.

    import de.tum.in.jmoped.annotation.FieldBits;

It works as in the case of @Bits, but @FieldBits takes an integer as the only argument. For example,

    @FieldBits(2)
    int a;

the field a will have two bits.
Remark:

@FieldBits always takes an integer as the only argument, and has no comma at the end.
If both @Bits and @FieldBits are specified for the same field, @FieldBits takes the priority.

top

Question 6: How to specify the bit sizes of a parameter?

Answer: See What is the annotation @Bits?. Alternatively, jMoped offers the annotations @ParameterBits exclusively for this purpose. You will have to add pds.jar into your classpath, and import the class ParameterBits.

    import de.tum.in.jmoped.annotation.ParameterBits;

It works as in the case of specifying parameter bits by sequence, i.e. put @ParameterBits just before method declarations and the sequence of integers tells which parameter has which bit.

    @ParameterBits({2, 3})
    void m(int x, int y)

The parameters x and y will have 2 and 3 bits, respectively.
Remark:

@Bits always takes an array of integers as the only argument, and has no comma at the end.
If both @Bits and @ParameterBits are specified for the same variable, @ParameterBits takes the priority.

top

Question 7: How to specify the bit sizes of a local variable?

Answer: See What is the annotation @Bits?.
Remark:

For technical reason, there is no @LocalVariableBits, and it is not possible to write @Bits in front of a local variable.

top

Question 8: How does jMoped simulate Java heaps?

Answer: jMoped simulates the heap similar to the way JVM does. The simulation is achieved via a global array variable and a pointer. Every time a new object is created, it occupies some parts of the array. The pointer is always updated to the next available block of the array, which is determined by the size of the objects. For example, if the the heap size is 7, jMoped will declare

    int heap[7];
    int ptr;

top