xref: /llvm-project/clang/test/Analysis/constraint-assignor.c (revision 0dd49a5628bbe01cecf6516017da59ae44863ab3)
15f8dca02SGabor Marton // RUN: %clang_analyze_cc1 %s \
25f8dca02SGabor Marton // RUN:   -analyzer-checker=core \
35f8dca02SGabor Marton // RUN:   -analyzer-checker=debug.ExprInspection \
45f8dca02SGabor Marton // RUN:   -verify
55f8dca02SGabor Marton 
6*0dd49a56SAaron Ballman void clang_analyzer_warnIfReached(void);
7a8297ed9SGabor Marton void clang_analyzer_eval(int);
85f8dca02SGabor Marton 
rem_constant_rhs_ne_zero(int x,int y)95f8dca02SGabor Marton void rem_constant_rhs_ne_zero(int x, int y) {
105f8dca02SGabor Marton   if (x % 3 == 0) // x % 3 != 0 -> x != 0
115f8dca02SGabor Marton     return;
125f8dca02SGabor Marton   if (x * y != 0) // x * y == 0
135f8dca02SGabor Marton     return;
145f8dca02SGabor Marton   if (y != 1)     // y == 1     -> x == 0
155f8dca02SGabor Marton     return;
165f8dca02SGabor Marton   clang_analyzer_warnIfReached(); // no-warning
175f8dca02SGabor Marton   (void)x; // keep the constraints alive.
185f8dca02SGabor Marton }
195f8dca02SGabor Marton 
rem_symbolic_rhs_ne_zero(int x,int y,int z)205f8dca02SGabor Marton void rem_symbolic_rhs_ne_zero(int x, int y, int z) {
215f8dca02SGabor Marton   if (x % z == 0) // x % z != 0 -> x != 0
225f8dca02SGabor Marton     return;
235f8dca02SGabor Marton   if (x * y != 0) // x * y == 0
245f8dca02SGabor Marton     return;
255f8dca02SGabor Marton   if (y != 1)     // y == 1     -> x == 0
265f8dca02SGabor Marton     return;
275f8dca02SGabor Marton   clang_analyzer_warnIfReached(); // no-warning
285f8dca02SGabor Marton   (void)x; // keep the constraints alive.
295f8dca02SGabor Marton }
305f8dca02SGabor Marton 
rem_symbolic_rhs_ne_zero_nested(int w,int x,int y,int z)315f8dca02SGabor Marton void rem_symbolic_rhs_ne_zero_nested(int w, int x, int y, int z) {
325f8dca02SGabor Marton   if (w % x % z == 0) // w % x % z != 0 -> w % x != 0
335f8dca02SGabor Marton     return;
345f8dca02SGabor Marton   if (w % x * y != 0) // w % x * y == 0
355f8dca02SGabor Marton     return;
365f8dca02SGabor Marton   if (y != 1)         // y == 1         -> w % x == 0
375f8dca02SGabor Marton     return;
385f8dca02SGabor Marton   clang_analyzer_warnIfReached(); // no-warning
395f8dca02SGabor Marton   (void)(w * x); // keep the constraints alive.
405f8dca02SGabor Marton }
415f8dca02SGabor Marton 
rem_constant_rhs_ne_zero_early_contradiction(int x,int y)425f8dca02SGabor Marton void rem_constant_rhs_ne_zero_early_contradiction(int x, int y) {
435f8dca02SGabor Marton   if ((x + y) != 0)     // (x + y) == 0
445f8dca02SGabor Marton     return;
455f8dca02SGabor Marton   if ((x + y) % 3 == 0) // (x + y) % 3 != 0 -> (x + y) != 0 -> contradiction
465f8dca02SGabor Marton     return;
475f8dca02SGabor Marton   clang_analyzer_warnIfReached(); // no-warning
485f8dca02SGabor Marton   (void)x; // keep the constraints alive.
495f8dca02SGabor Marton }
505f8dca02SGabor Marton 
rem_symbolic_rhs_ne_zero_early_contradiction(int x,int y,int z)515f8dca02SGabor Marton void rem_symbolic_rhs_ne_zero_early_contradiction(int x, int y, int z) {
525f8dca02SGabor Marton   if ((x + y) != 0)     // (x + y) == 0
535f8dca02SGabor Marton     return;
545f8dca02SGabor Marton   if ((x + y) % z == 0) // (x + y) % z != 0 -> (x + y) != 0 -> contradiction
555f8dca02SGabor Marton     return;
565f8dca02SGabor Marton   clang_analyzer_warnIfReached(); // no-warning
575f8dca02SGabor Marton   (void)x; // keep the constraints alive.
585f8dca02SGabor Marton }
595f8dca02SGabor Marton 
internal_unsigned_signed_mismatch(unsigned a)605f8dca02SGabor Marton void internal_unsigned_signed_mismatch(unsigned a) {
615f8dca02SGabor Marton   int d = a;
625f8dca02SGabor Marton   // Implicit casts are not handled, thus the analyzer models `d % 2` as
635f8dca02SGabor Marton   // `(reg_$0<unsigned int a>) % 2`
645f8dca02SGabor Marton   // However, this should not result in internal signedness mismatch error when
655f8dca02SGabor Marton   // we assign new constraints below.
665f8dca02SGabor Marton   if (d % 2 != 0)
675f8dca02SGabor Marton     return;
685f8dca02SGabor Marton }
69a8297ed9SGabor Marton 
remainder_with_adjustment(int x)70a8297ed9SGabor Marton void remainder_with_adjustment(int x) {
71a8297ed9SGabor Marton   if ((x + 1) % 3 == 0) // (x + 1) % 3 != 0 -> x + 1 != 0 -> x != -1
72a8297ed9SGabor Marton     return;
73a8297ed9SGabor Marton   clang_analyzer_eval(x + 1 != 0); // expected-warning{{TRUE}}
74a8297ed9SGabor Marton   clang_analyzer_eval(x != -1);    // expected-warning{{TRUE}}
75a8297ed9SGabor Marton   (void)x; // keep the constraints alive.
76a8297ed9SGabor Marton }
77a8297ed9SGabor Marton 
remainder_with_adjustment_of_composit_lhs(int x,int y)78a8297ed9SGabor Marton void remainder_with_adjustment_of_composit_lhs(int x, int y) {
79a8297ed9SGabor Marton   if ((x + y + 1) % 3 == 0) // (x + 1) % 3 != 0 -> x + 1 != 0 -> x != -1
80a8297ed9SGabor Marton     return;
81a8297ed9SGabor Marton   clang_analyzer_eval(x + y + 1 != 0); // expected-warning{{TRUE}}
82a8297ed9SGabor Marton   clang_analyzer_eval(x + y != -1);    // expected-warning{{TRUE}}
83a8297ed9SGabor Marton   (void)(x * y); // keep the constraints alive.
84a8297ed9SGabor Marton }
85