Lines Matching full:env
47 void initNegative(Value &Val, Environment &Env) { in initNegative() argument
48 Val.setProperty("neg", Env.getBoolLiteralValue(true)); in initNegative()
49 Val.setProperty("zero", Env.getBoolLiteralValue(false)); in initNegative()
50 Val.setProperty("pos", Env.getBoolLiteralValue(false)); in initNegative()
52 void initPositive(Value &Val, Environment &Env) { in initPositive() argument
53 Val.setProperty("neg", Env.getBoolLiteralValue(false)); in initPositive()
54 Val.setProperty("zero", Env.getBoolLiteralValue(false)); in initPositive()
55 Val.setProperty("pos", Env.getBoolLiteralValue(true)); in initPositive()
57 void initZero(Value &Val, Environment &Env) { in initZero() argument
58 Val.setProperty("neg", Env.getBoolLiteralValue(false)); in initZero()
59 Val.setProperty("zero", Env.getBoolLiteralValue(true)); in initZero()
60 Val.setProperty("pos", Env.getBoolLiteralValue(false)); in initZero()
74 SignProperties initUnknown(Value &Val, Environment &Env) { in initUnknown() argument
75 SignProperties Ps{&Env.makeAtomicBoolValue(), &Env.makeAtomicBoolValue(), in initUnknown()
76 &Env.makeAtomicBoolValue()}; in initUnknown()
80 SignProperties getSignProperties(const Value &Val, const Environment &Env) { in getSignProperties() argument
91 const StorageLocation *Loc = State.Env.getStorageLocation(*Var); in transferUninitializedInt()
92 Value *Val = State.Env.getValue(*Loc); in transferUninitializedInt()
93 initUnknown(*Val, State.Env); in transferUninitializedInt()
112 const auto *OperandValue = State.Env.getValue(*OperandVar); in getValueAndSignProperties()
117 auto *UnaryOpValue = State.Env.getValue(*UO); in getValueAndSignProperties()
119 UnaryOpValue = &State.Env.makeAtomicBoolValue(); in getValueAndSignProperties()
120 State.Env.setValue(*UO, *UnaryOpValue); in getValueAndSignProperties()
124 SignProperties OperandProps = getSignProperties(*OperandValue, State.Env); in getValueAndSignProperties()
128 SignProperties UnaryOpProps = initUnknown(*UnaryOpValue, State.Env); in getValueAndSignProperties()
134 auto &A = State.Env.arena(); in transferBinary()
136 if (BoolValue *V = State.Env.get<BoolValue>(*BO)) { in transferBinary()
140 State.Env.setValue(*BO, A.makeBoolValue(*Comp)); in transferBinary()
144 // auto *NegatedComp = &State.Env.makeNot(*Comp); in transferBinary()
146 auto *LHS = State.Env.getValue(*BO->getLHS()); in transferBinary()
147 auto *RHS = State.Env.getValue(*BO->getRHS()); in transferBinary()
152 SignProperties LHSProps = getSignProperties(*LHS, State.Env); in transferBinary()
153 SignProperties RHSProps = getSignProperties(*RHS, State.Env); in transferBinary()
160 State.Env.assume( in transferBinary()
164 State.Env.assume( in transferBinary()
170 State.Env.assume( in transferBinary()
174 State.Env.assume( in transferBinary()
180 State.Env.assume( in transferBinary()
186 State.Env.assume( in transferBinary()
191 State.Env.assume( in transferBinary()
194 State.Env.assume( in transferBinary()
197 State.Env.assume( in transferBinary()
211 auto &A = State.Env.arena(); in transferUnaryMinus()
218 State.Env.assume( in transferUnaryMinus()
221 State.Env.assume( in transferUnaryMinus()
224 State.Env.assume(A.makeImplies(OperandProps.Zero->formula(), in transferUnaryMinus()
231 auto &A = State.Env.arena(); in transferUnaryNot()
238 State.Env.assume(A.makeImplies( in transferUnaryNot()
246 State.Env.assume( in transferUnaryNot()
249 State.Env.assume(A.makeEquals(UOBoolVal->formula(), in transferUnaryNot()
260 Value *getOrCreateValue(const Expr *E, Environment &Env) { in getOrCreateValue() argument
263 StorageLocation *Loc = Env.getStorageLocation(*E); in getOrCreateValue()
265 Loc = &Env.createStorageLocation(*E); in getOrCreateValue()
266 Env.setStorageLocation(*E, *Loc); in getOrCreateValue()
268 Val = Env.getValue(*Loc); in getOrCreateValue()
270 Val = Env.createValue(E->getType()); in getOrCreateValue()
271 Env.setValue(*Loc, *Val); in getOrCreateValue()
274 Val = Env.getValue(*E); in getOrCreateValue()
276 Val = Env.createValue(E->getType()); in getOrCreateValue()
277 Env.setValue(*E, *Val); in getOrCreateValue()
289 Value *Val = getOrCreateValue(E, State.Env); in transferExpr()
298 initUnknown(*Val, State.Env); in transferExpr()
305 initNegative(*Val, State.Env); in transferExpr()
308 initZero(*Val, State.Env); in transferExpr()
311 initPositive(*Val, State.Env); in transferExpr()
363 void transfer(const CFGElement &Elt, NoopLattice &L, Environment &Env) { in transfer() argument
364 LatticeTransferState State(L, Env); in transfer()
457 getProperty(const Environment &Env, ASTContext &ASTCtx, const Node *N, in getProperty() argument
461 const StorageLocation *Loc = Env.getStorageLocation(*N); in getProperty()
464 const Value *Val = Env.getValue(*Loc); in getProperty()
477 testing::AssertionResult isPropertyImplied(const Environment &Env, in isPropertyImplied() argument
480 auto [Result, Prop] = getProperty(Env, ASTCtx, N, Property); in isPropertyImplied()
484 if (Env.proves(BVProp->formula()) != Implies) in isPropertyImplied()
493 const Environment &Env) { in isNegative() argument
494 testing::AssertionResult R = isPropertyImplied(Env, ASTCtx, N, "neg", true); in isNegative()
497 R = isPropertyImplied(Env, ASTCtx, N, "zero", false); in isNegative()
500 return isPropertyImplied(Env, ASTCtx, N, "pos", false); in isNegative()
504 const Environment &Env) { in isPositive() argument
505 testing::AssertionResult R = isPropertyImplied(Env, ASTCtx, N, "pos", true); in isPositive()
508 R = isPropertyImplied(Env, ASTCtx, N, "zero", false); in isPositive()
511 return isPropertyImplied(Env, ASTCtx, N, "neg", false); in isPositive()
515 const Environment &Env) { in isZero() argument
516 testing::AssertionResult R = isPropertyImplied(Env, ASTCtx, N, "zero", true); in isZero()
519 R = isPropertyImplied(Env, ASTCtx, N, "pos", false); in isZero()
522 return isPropertyImplied(Env, ASTCtx, N, "neg", false); in isZero()
526 const Environment &Env) { in isTop() argument
527 testing::AssertionResult R = isPropertyImplied(Env, ASTCtx, N, "zero", false); in isTop()
530 R = isPropertyImplied(Env, ASTCtx, N, "pos", false); in isTop()
533 return isPropertyImplied(Env, ASTCtx, N, "neg", false); in isTop()
555 const Environment &Env = getEnvironmentAtAnnotation(Results, "p"); in TEST() local
564 EXPECT_TRUE(isNegative(A, ASTCtx, Env)); in TEST()
565 EXPECT_TRUE(isZero(B, ASTCtx, Env)); in TEST()
566 EXPECT_TRUE(isPositive(C, ASTCtx, Env)); in TEST()
567 EXPECT_TRUE(isTop(D, ASTCtx, Env)); in TEST()
568 EXPECT_TRUE(isTop(E, ASTCtx, Env)); in TEST()
569 EXPECT_TRUE(isPositive(F, ASTCtx, Env)); in TEST()
587 const Environment &Env = getEnvironmentAtAnnotation(Results, "p"); in TEST() local
591 EXPECT_TRUE(isPositive(A, ASTCtx, Env)); in TEST()
592 EXPECT_TRUE(isNegative(B, ASTCtx, Env)); in TEST()
610 const Environment &Env = getEnvironmentAtAnnotation(Results, "p"); in TEST() local
614 EXPECT_TRUE(isPositive(A, ASTCtx, Env)); in TEST()
615 EXPECT_TRUE(isZero(B, ASTCtx, Env)); in TEST()
912 const Environment &Env = getEnvironmentAtAnnotation(Results, "p"); in TEST() local
917 EXPECT_TRUE(isPositive(A, ASTCtx, Env)); in TEST()
918 EXPECT_TRUE(isPositive(B, ASTCtx, Env)); in TEST()