Skip to content

Commit 3efb52c

Browse files
committed
Remove method bodies as @y553546436 said the peers do the computation
1 parent 93d7ee2 commit 3efb52c

File tree

1 file changed

+9
-16
lines changed

1 file changed

+9
-16
lines changed

src/main/gov/nasa/jpf/vm/Verify.java

Lines changed: 9 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -353,70 +353,63 @@ public static void addObjectAttribute (Object o, int val) {}
353353
* note that the JPF does not execute the following getBitFlip methods, but execute their native methods
354354
*/
355355
public static long getBitFlip (long v, int nBit, int len) {
356-
assert (nBit <= len);
357-
int last = -1;
358-
for (int i = 0; i < nBit; ++i) {
359-
int p = getInt(last+1, len-nBit+i);
360-
v ^= (1l << p);
361-
last = p;
362-
}
363-
return v;
356+
return 0l;
364357
}
365358

366359
/**
367360
* flip nBit bits of a long variable
368361
*/
369362
public static long getBitFlip (long v, int nBit) {
370-
return getBitFlip(v, nBit, 64);
363+
return 0l;
371364
}
372365

373366
/**
374367
* flip nBit bits of an int variable
375368
*/
376369
public static int getBitFlip (int v, int nBit) {
377-
return (int) getBitFlip((long)v, nBit, 32);
370+
return 0;
378371
}
379372

380373
/**
381374
* flip nBit bits of a short variable
382375
*/
383376
public static short getBitFlip (short v, int nBit) {
384-
return (short) getBitFlip((long)v, nBit, 16);
377+
return (short) 0;
385378
}
386379

387380
/**
388381
* flip nBit bits of a char variable
389382
*/
390383
public static char getBitFlip (char v, int nBit) {
391-
return (char) getBitFlip((long)v, nBit, 16);
384+
return 0;
392385
}
393386

394387
/**
395388
* flip nBit bits of a byte variable
396389
*/
397390
public static byte getBitFlip (byte v, int nBit) {
398-
return (byte) getBitFlip((long)v, nBit, 8);
391+
return 0;
399392
}
400393

401394
/**
402395
* flip nBit bits of a double variable
403396
*/
404397
public static double getBitFlip (double v, int nBit) {
405-
return Double.longBitsToDouble(getBitFlip(Double.doubleToLongBits(v), nBit));
398+
return 0.0;
406399
}
407400

408401
/**
409402
* flip nBit bits of a float variable
410403
*/
411404
public static float getBitFlip (float v, int nBit) {
412-
return Float.intBitsToFloat(getBitFlip(Float.floatToIntBits(v), nBit));
405+
return 0.0f;
413406
}
414407

415408
/**
416409
* flip a boolean variable
417410
*/
418411
public static boolean getBitFlip (boolean v) {
419-
return !v;
412+
return true;
420413
}
421414

422415
/**

0 commit comments

Comments
 (0)