• 如果您觉得本站非常有看点，那么赶紧使用Ctrl+D 收藏吧
> java > Java BitvectorExpression类的典型用法和代码示例

Java BitvectorExpression类的典型用法和代码示例

java 2次浏览

本文整理汇总了Java中gov.nasa.jpf.constraints.expressions.BitvectorExpression类的典型用法代码示例。如果您正苦于以下问题：Java BitvectorExpression类的具体用法？Java BitvectorExpression怎么用？Java BitvectorExpression使用的例子？那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。

BitvectorExpression类属于gov.nasa.jpf.constraints.expressions包，在下文中一共展示了BitvectorExpression类的21个代码示例，这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞，您的评价将有助于我们的系统推荐出更棒的Java代码示例。

示例1: execute

​ 点赞 3 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
 public Instruction execute (ThreadInfo ti) {
	StackFrame sf = ti.getTopFrame();

   if (sf.getOperandAttr(1) == null && sf.getOperandAttr(3) == null) {
     return super.execute(ti);
   }
   
  ConcolicUtil.Pair<Long> right = ConcolicUtil.popLong(sf);
  ConcolicUtil.Pair<Long> left = ConcolicUtil.popLong(sf);

  BitvectorExpression<Long> symb = BitvectorExpression.create(
           left.symb, BitvectorOperator.XOR, right.symb);    
   
   long conc = left.conc ^ right.conc;    
   
   ConcolicUtil.Pair<Long> result = new ConcolicUtil.Pair<Long>(conc, symb);
   ConcolicUtil.pushLong(result, sf);

   if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute LXOR: " + result);		
   return getNext(ti);
}

开发者ID:psycopaths，
项目名称:jdart，
代码行数:23，
代码来源:LXOR.java

示例2: execute

​ 点赞 3 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
public Instruction execute (ThreadInfo ti) {
StackFrame sf = ti.getTopFrame();

if(sf.getOperandAttr(0) ==null && sf.getOperandAttr(1)==null) {
	return super.execute(ti); 
  } 
  
 ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
 ConcolicUtil.Pair<Integer> left = ConcolicUtil.popInt(sf);

 BitvectorExpression<Integer> symb = BitvectorExpression.create(
          left.symb, BitvectorOperator.SHIFTUR, right.symb);    
  
  int conc = left.conc >>> right.conc;    
  
  ConcolicUtil.Pair<Integer> result = new ConcolicUtil.Pair<Integer>(conc, symb);
  ConcolicUtil.pushInt(result, sf);

  if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute IUSHR: " + result);		
  return getNext(ti);
}

开发者ID:psycopaths，
项目名称:jdart，
代码行数:23，
代码来源:IUSHR.java

示例3: execute

​ 点赞 3 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
 public Instruction execute (ThreadInfo ti) {
	StackFrame sf = ti.getTopFrame();

   if (sf.getOperandAttr(1) == null && sf.getOperandAttr(3) == null) {
     return super.execute(ti);
   }
   
  ConcolicUtil.Pair<Long> right = ConcolicUtil.popLong(sf);
  ConcolicUtil.Pair<Long> left = ConcolicUtil.popLong(sf);

  BitvectorExpression<Long> symb = BitvectorExpression.create(
           left.symb, BitvectorOperator.OR, right.symb);    
   
   long conc = left.conc | right.conc;    
   
   ConcolicUtil.Pair<Long> result = new ConcolicUtil.Pair<Long>(conc, symb);
   ConcolicUtil.pushLong(result, sf);

   if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute LOR: " + result);		
   return getNext(ti);
}

开发者ID:psycopaths，
项目名称:jdart，
代码行数:23，
代码来源:LOR.java

示例4: execute

​ 点赞 3 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
public Instruction execute (ThreadInfo ti) {
StackFrame sf = ti.getTopFrame();

if(sf.getOperandAttr(0) ==null && sf.getOperandAttr(1)==null) {
	return super.execute(ti); 
  } 
  
 ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
 ConcolicUtil.Pair<Integer> left = ConcolicUtil.popInt(sf);

  BitvectorExpression<Integer> symb = BitvectorExpression.create(
          left.symb, BitvectorOperator.OR, right.symb);    
  
  int conc = left.conc | right.conc;    
  
  ConcolicUtil.Pair<Integer> result = new ConcolicUtil.Pair<Integer>(conc, symb);
  ConcolicUtil.pushInt(result, sf);

  if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute IOR: " + result);		
  return getNext(ti);
}

开发者ID:psycopaths，
项目名称:jdart，
代码行数:23，
代码来源:IOR.java

示例5: execute

​ 点赞 3 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
 public Instruction execute (ThreadInfo ti) {
	StackFrame sf = ti.getTopFrame();

   if (sf.getOperandAttr(1) == null && sf.getOperandAttr(3) == null) {
     return super.execute(ti);
   }
   
  ConcolicUtil.Pair<Long> right = ConcolicUtil.popLong(sf);
  ConcolicUtil.Pair<Long> left = ConcolicUtil.popLong(sf);

  BitvectorExpression<Long> symb = BitvectorExpression.create(
           left.symb, BitvectorOperator.AND, right.symb);    
   
   long conc = left.conc & right.conc;    
   
   ConcolicUtil.Pair<Long> result = new ConcolicUtil.Pair<Long>(conc, symb);
   ConcolicUtil.pushLong(result, sf);

   if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute LAND: " + result);		
   return getNext(ti);
}

开发者ID:psycopaths，
项目名称:jdart，
代码行数:23，
代码来源:LAND.java

示例6: execute

​ 点赞 3 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
 public Instruction execute (ThreadInfo ti) {
	StackFrame sf = ti.getTopFrame();

   if (sf.getOperandAttr(0) == null && sf.getOperandAttr(2) == null) {
     return super.execute(ti);
   }
   
  ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
  ConcolicUtil.Pair<Long> left = ConcolicUtil.popLong(sf);

  BitvectorExpression<Long> symb = BitvectorExpression.create(
           left.symb, BitvectorOperator.SHIFTUR, new CastExpression<>(right.symb, BuiltinTypes.SINT64, NumericCastOperation.TO_SINT64));    
   
   long conc = left.conc >>> right.conc;    
   
   ConcolicUtil.Pair<Long> result = new ConcolicUtil.Pair<Long>(conc, symb);
   ConcolicUtil.pushLong(result, sf);

   if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute LUSHR: " + result);		
   return getNext(ti);
}

开发者ID:psycopaths，
项目名称:jdart，
代码行数:23，
代码来源:LUSHR.java

示例7: execute

​ 点赞 3 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
public Instruction execute (ThreadInfo ti) {
StackFrame sf = ti.getTopFrame();

if(sf.getOperandAttr(0) ==null && sf.getOperandAttr(1)==null) {
	return super.execute(ti); 
  } 
  
 ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
 ConcolicUtil.Pair<Integer> left = ConcolicUtil.popInt(sf);

 BitvectorExpression<Integer> symb = BitvectorExpression.create(
          left.symb, BitvectorOperator.SHIFTL, right.symb);    
  
  int conc = left.conc << right.conc;    
  
  ConcolicUtil.Pair<Integer> result = new ConcolicUtil.Pair<Integer>(conc, symb);
  ConcolicUtil.pushInt(result, sf);

  if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute ISHL: " + result);		
  return getNext(ti);
}

开发者ID:psycopaths，
项目名称:jdart，
代码行数:23，
代码来源:ISHL.java

示例8: execute

​ 点赞 3 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
public Instruction execute (ThreadInfo ti) {
StackFrame sf = ti.getTopFrame();

if(sf.getOperandAttr(0) ==null && sf.getOperandAttr(1)==null) {
	return super.execute(ti); 
  } 
  
 ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
 ConcolicUtil.Pair<Integer> left = ConcolicUtil.popInt(sf);

 BitvectorExpression<Integer> symb = BitvectorExpression.create(
          left.symb, BitvectorOperator.SHIFTR, right.symb);    
  
  int conc = left.conc >> right.conc;    
  
  ConcolicUtil.Pair<Integer> result = new ConcolicUtil.Pair<Integer>(conc, symb);
  ConcolicUtil.pushInt(result, sf);

  if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute ISHR: " + result);		
  return getNext(ti);
}

开发者ID:psycopaths，
项目名称:jdart，
代码行数:23，
代码来源:ISHR.java

示例9: execute

​ 点赞 3 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
public Instruction execute (ThreadInfo ti) {
StackFrame sf = ti.getTopFrame();

if(sf.getOperandAttr(0) ==null && sf.getOperandAttr(1)==null) {
	return super.execute(ti); 
  } 
  
 ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
 ConcolicUtil.Pair<Integer> left = ConcolicUtil.popInt(sf);

 BitvectorExpression<Integer> symb = BitvectorExpression.create(
          left.symb, BitvectorOperator.XOR, right.symb);    
  
  int conc = left.conc ^ right.conc;    
  
  ConcolicUtil.Pair<Integer> result = new ConcolicUtil.Pair<Integer>(conc, symb);
  ConcolicUtil.pushInt(result, sf);

  if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute IXOR: " + result);		
  return getNext(ti);
}

开发者ID:psycopaths，
项目名称:jdart，
代码行数:23，
代码来源:IXOR.java

示例10: execute

​ 点赞 3 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
 public Instruction execute (ThreadInfo ti) {
	StackFrame sf = ti.getTopFrame();

   if (sf.getOperandAttr(0) == null && sf.getOperandAttr(2) == null) {
     return super.execute(ti);
   }
   
  ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
  ConcolicUtil.Pair<Long> left = ConcolicUtil.popLong(sf);

  BitvectorExpression<Long> symb = BitvectorExpression.create(
           left.symb, BitvectorOperator.SHIFTL, new CastExpression<>(right.symb, BuiltinTypes.SINT64, NumericCastOperation.TO_SINT64));    
   
   long conc = left.conc << right.conc;    
   
   ConcolicUtil.Pair<Long> result = new ConcolicUtil.Pair<Long>(conc, symb);
   ConcolicUtil.pushLong(result, sf);

   if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute LSHL: " + result);		
   return getNext(ti);
}

开发者ID:psycopaths，
项目名称:jdart，
代码行数:23，
代码来源:LSHL.java

示例11: execute

​ 点赞 3 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
public Instruction execute (ThreadInfo ti) {
StackFrame sf = ti.getTopFrame();

if(sf.getOperandAttr(0) ==null && sf.getOperandAttr(1)==null) {
	return super.execute(ti); 
  } 
  
 ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
 ConcolicUtil.Pair<Integer> left = ConcolicUtil.popInt(sf);

  BitvectorExpression<Integer> symb = BitvectorExpression.create(
          left.symb, BitvectorOperator.AND, right.symb);    
  
  int conc = left.conc & right.conc;    
  
  ConcolicUtil.Pair<Integer> result = new ConcolicUtil.Pair<Integer>(conc, symb);
  ConcolicUtil.pushInt(result, sf);

  if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute IAND: " + result);		
  return getNext(ti);
}

开发者ID:psycopaths，
项目名称:jdart，
代码行数:23，
代码来源:IAND.java

示例12: execute

​ 点赞 3 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
 public Instruction execute (ThreadInfo ti) {
	StackFrame sf = ti.getTopFrame();

   if (sf.getOperandAttr(0) == null && sf.getOperandAttr(2) == null) {
     return super.execute(ti);
   }
   
  ConcolicUtil.Pair<Integer> right = ConcolicUtil.popInt(sf);
  ConcolicUtil.Pair<Long> left = ConcolicUtil.popLong(sf);

  BitvectorExpression<Long> symb = BitvectorExpression.create(
           left.symb, BitvectorOperator.SHIFTR, new CastExpression<>(right.symb, BuiltinTypes.SINT64, NumericCastOperation.TO_SINT64));    
   
   long conc = left.conc >> right.conc;    
   
   ConcolicUtil.Pair<Long> result = new ConcolicUtil.Pair<Long>(conc, symb);
   ConcolicUtil.pushLong(result, sf);

   if (ConcolicInstructionFactory.DEBUG) ConcolicInstructionFactory.logger.finest("Execute LSHR: " + result);		
   return getNext(ti);
}

开发者ID:psycopaths，
项目名称:jdart，
代码行数:23，
代码来源:LSHR.java

示例13: parseBitVectorExpression

​ 点赞 3 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
private BitvectorExpression parseBitVectorExpression() {
  currentLine = currentLine.substring(2);
  Expression left = parseNextExpression();
  currentLine = currentLine.substring(1);
  BitvectorOperator operator;
  if (nextTokenIs(TransitionEncoding.bitVectorOperator)) {
    currentLine = currentLine.substring(1);
    int operatorEnde = currentLine.indexOf(";");
    String readOperator = currentLine.substring(0, operatorEnde);
    operator = BitvectorOperator.valueOf(readOperator);
    currentLine = currentLine.substring(operatorEnde + 1);
  } else {
    throw new IllegalStateException(
            "The next token must be an BitVectorOperator");
  }
  currentLine = currentLine.substring(1);
  Expression right = parseNextExpression();
  return new BitvectorExpression(left, operator, right);
}

开发者ID:psycopaths，
项目名称:psyco，
代码行数:20，
代码来源:TransitionSystemLoader.java

示例14: visit

​ 点赞 2 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
public <E> String visit(
        BitvectorExpression<E> bv, HashMap<Class, String> data) {
  String left = visit(bv.getLeft(), data);
  String right = visit(bv.getRight(), data);
  String operator = convert(bv.getOperator());
  return TransitionEncoding.bitVector + ":" + left + ":" + operator
          + ":" + right + ";";

}

开发者ID:psycopaths，
项目名称:psyco，
代码行数:11，
代码来源:ExpressionConverterVisitor.java

示例15: parseBitVector

​ 点赞 2 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
private Expression<Boolean> parseBitVector(Expr z3Expr, ArrayList<Expression<Boolean>> arguments) throws Exception {
  if (z3Expr.isBVAND()) {
    return new BitvectorExpression<>(arguments.get(0),
            BitvectorOperator.AND, arguments.get(1));
  }
  if (z3Expr.isBVSLT()) {
    return new NumericBooleanExpression(arguments.get(0),
            NumericComparator.LT, arguments.get(1));
  }
  if (z3Expr instanceof BitVecExpr) {
    if (z3Expr.isInt()) {
      return new Variable(BuiltinTypes.INTEGER, z3Expr.toString());
    }
    switch (z3Expr.getSort().getSortKind()) {
      case Z3_BOOL_SORT:
        return new Variable(BuiltinTypes.BOOL, z3Expr.toString());
      case Z3_INT_SORT:
        return new Variable(BuiltinTypes.INTEGER, z3Expr.toString());
      case Z3_REAL_SORT:
        return new Variable(BuiltinTypes.DECIMAL, z3Expr.toString());
      case Z3_BV_SORT:
        return new Variable(BuiltinTypes.INTEGER, z3Expr.toString());
      default:
        throw new Exception("Unknown Sort");
    }
  }
  return null;
}

开发者ID:psycopaths，
项目名称:jconstraints-z3，
代码行数:29，
代码来源:NativeZ3TojConstraintConverter.java

示例16: visit

​ 点赞 2 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
public <E> Expr visit(
    BitvectorExpression<E> bv, Void data) {
  BitVecExpr left = null, right = null;
  
  try {
    left = (BitVecExpr)visit(bv.getLeft());
    right = (BitVecExpr)visit(bv.getRight());
    
    switch(bv.getOperator()) {
    case AND:
      return ctx.mkBVAND(left, right);
    case OR:
      return ctx.mkBVOR(left, right);
    case SHIFTL:
      return ctx.mkBVSHL(left, right);
    case SHIFTR:
      return ctx.mkBVASHR(left, right);
    case SHIFTUR:
      return ctx.mkBVLSHR(left, right);
    case XOR:
      return ctx.mkBVXOR(left, right);
    default:
      throw new IllegalArgumentException("Cannot handle bitvector operator " + bv.getOperator());
    }
  }
  catch(Z3Exception ex) {
    throw new RuntimeException(ex);
  }
  finally {
    safeDispose(left, right);
  }
}

开发者ID:psycopaths，
项目名称:jconstraints-z3，
代码行数:34，
代码来源:NativeZ3ExpressionGenerator.java

示例17: translateBitvectorOperator

​ 点赞 2 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
public Expression<?> translateBitvectorOperator(Tree n) {
  BitvectorOperator op;
  switch(n.getType()) {
  case BVOR:
    op = BitvectorOperator.OR;
    break;
  case BVXOR:
    op = BitvectorOperator.XOR;
    break;
  case BVAND:
    op = BitvectorOperator.AND;
    break;
  case BVSHL:
    op = BitvectorOperator.SHIFTL;
    break;
  case BVSHR:
    op = BitvectorOperator.SHIFTR;
    break;
  case BVSHUR:
    op = BitvectorOperator.SHIFTUR;
    break;
  default:
    throw new UnexpectedTokenException(n, BVOR, BVXOR, BVAND, BVSHL, BVSHR, BVSHUR);
  }
  
  Expression<?> left = translateArithmeticExpression(n.getChild(0));
  Expression<?> right = translateArithmeticExpression(n.getChild(1));
  
  return BitvectorExpression.createCompatible(left, op, right, types);
}

开发者ID:psycopaths，
项目名称:jconstraints，
代码行数:31，
代码来源:ASTTranslator.java

示例18: visit

​ 点赞 2 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
public <E> Boolean visit(BitvectorExpression<E> bv,Void data) {
  return visit(bv.getLeft()) && visit(bv.getRight()); 
}

开发者ID:psycopaths，
项目名称:jdart，
代码行数:5，
代码来源:FunctionFilter.java

示例19: visit

​ 点赞 2 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
public <E> BitvectorExpression<E> visit(BitvectorExpression<E> bv,Collection<FunctionExpression> data) {
  Expression left = visit(bv.getLeft(), data);
  Expression right = visit(bv.getRight(), data); 
  return new BitvectorExpression(left, bv.getOperator(), right);
}

开发者ID:psycopaths，
项目名称:jdart，
代码行数:7，
代码来源:FunctionFinder.java

示例20: visit

​ 点赞 2 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
@Override
public <E> Object visit(BitvectorExpression<E> bv, Void data) {
	//int: xor, or, and, usr, sr, sl, cmp
	//long: xor, or, and, arithmeticshiftleft, arithmeticshiftright, logicalshiftright
	
	//TODO: Missing:
	//int: cmp
	//long: logicalshiftright
	
	Object left = visit(bv.getLeft());
	Object right = visit(bv.getRight());
	
	//Type checking
	if(!(left instanceof SymInt) && !(left instanceof SymLong))
		throw new IllegalArgumentException("First operand must be of type " + SymInt.class.getName() + " or " + SymLong.class.getName());				

	BitvectorOperator op = bv.getOperator();
	switch(op) {
	case AND:
		if(left instanceof SymInt) {
			if(right instanceof SymInt)
				return Util.and((SymInt)left, (SymInt)right);
			else
				throw new IllegalArgumentException("Second operand must be of type " + SymInt.class);
		} else if(left instanceof SymLong) {
			if(right instanceof SymLong)
				return Util.and((SymLong)left, (SymLong)right);
			else
				throw new IllegalArgumentException("Second operand must be of type " + SymLong.class);
		}
	case OR:
		if(left instanceof SymInt) {
			if(right instanceof SymInt)
				return Util.or((SymInt)left, (SymInt)right);
			else
				throw new IllegalArgumentException("Second operand must be of type " + SymInt.class);
		} else if(left instanceof SymLong) {
			if(right instanceof SymLong)
				return Util.or((SymLong)left, (SymLong)right);
			else
				throw new IllegalArgumentException("Second operand must be of type " + SymLong.class);
		}
	case XOR:
		if(left instanceof SymInt) {
			if(right instanceof SymInt)
				return Util.xor((SymInt)left, (SymInt)right);
			else
				throw new IllegalArgumentException("Second operand must be of type " + SymInt.class);
		} else if(left instanceof SymLong) {
			if(right instanceof SymLong)
				return Util.xor((SymLong)left, (SymLong)right);
			else
				throw new IllegalArgumentException("Second operand must be of type " + SymLong.class);
		}
	case SHIFTL:
		if((left instanceof SymLong) && (right instanceof SymInt))
			return Util.arithmeticShiftLeft((SymLong)left, (SymInt)right);
		else if((left instanceof SymInt) && (right instanceof SymInt))
			return Util.sl((SymInt)left, (SymInt)right);
		else
			throw new IllegalArgumentException("Incompatible types for " + BitvectorOperator.SHIFTL);
	case SHIFTR:
		if((left instanceof SymLong) && (right instanceof SymInt))
			return Util.arithmeticShiftRight((SymLong)left, (SymInt)right);
		else if((left instanceof SymInt) && (right instanceof SymInt))
			return Util.sr((SymInt)left, (SymInt)right);
		else
			throw new IllegalArgumentException("Incompatible types for " + BitvectorOperator.SHIFTR);
	case SHIFTUR:
		if((left instanceof SymInt) && (right instanceof SymInt))
			return Util.usr((SymInt)left, (SymInt)right);
		else
			throw new IllegalArgumentException("Incompatible types for " + BitvectorOperator.SHIFTUR);
	default:
		throw new UnsupportedOperationException(op.name() + " operator not supported");
	}
}

开发者ID:psycopaths，
项目名称:jconstraints-coral，
代码行数:78，
代码来源:CoralExpressionGenerator.java

示例21: visit

​ 点赞 2 ​ 

import gov.nasa.jpf.constraints.expressions.BitvectorExpression; //导入依赖的package包/类
public <E> R visit(
BitvectorExpression<E> bv, D data);

开发者ID:psycopaths，
项目名称:jconstraints，
代码行数:3，
代码来源:ExpressionVisitor.java

版权声明：本文转自网络文章，转载此文章仅为分享知识，如有侵权，请联系管理员进行删除。
喜欢 (0)