[Bug analyzer/109193] New: GCC Static Analyzer does not know 1-a > 0-b" in the true branch of "if (a < b && 0 < a) "

[Bug analyzer/109193] New: GCC Static Analyzer does not know 1-a > 0-b" in the true branch of "if (a < b && 0 < a) "

[geoffreydgr at icloud dot com]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=109193

            Bug ID: 109193
           Summary: GCC Static Analyzer does not know 1-a > 0-b" in the
                    true branch of "if (a < b && 0 < a) "
           Product: gcc
           Version: 13.0
            Status: UNCONFIRMED
          Severity: normal
          Priority: P3
         Component: analyzer
          Assignee: dmalcolm at gcc dot gnu.org
          Reporter: geoffreydgr at icloud dot com
  Target Milestone: ---

I found a problem that GCC Static Analyzer does not know 1-a > 0-b" (line 12)
in the true branch of "if (a < b && 0 < a) ", but it knows “0-a > 0-b" (line
11) .

I run gcc (trunk) with options -fanalyzer -O0.

See it live: https://godbolt.org/z/6MjobMqnM

Input:
```
#include <stdint.h>
#include <stdbool.h>

int foo(int a, int b) {
    if ((a<b) && (0 < a)){
        //Negation
        __analyzer_eval(!(a<b) == false); 
        __analyzer_eval(-a > -b);

        // Add a positive number after the negation
        __analyzer_eval(0-a > 0-b);
        __analyzer_eval(1-a > 0-b);
        __analyzer_eval(1-a > 1-b);
        __analyzer_eval(2-a > 0-b);
        __analyzer_eval(2-a > 1-b);
        __analyzer_eval(2-a > 2-b);

    }
}
```


Output:
```
<source>: In function 'foo':
<source>:7:9: warning: implicit declaration of function '__analyzer_eval'
[-Wimplicit-function-declaration]
    7 |         __analyzer_eval(!(a<b) == false);
      |         ^~~~~~~~~~~~~~~
<source>:7:9: warning: TRUE
    7 |         __analyzer_eval(!(a<b) == false);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:8:9: warning: TRUE
    8 |         __analyzer_eval(-a > -b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~
<source>:11:9: warning: TRUE
   11 |         __analyzer_eval(0-a > 0-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:12:9: warning: UNKNOWN
   12 |         __analyzer_eval(1-a > 0-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:13:9: warning: TRUE
   13 |         __analyzer_eval(1-a > 1-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:14:9: warning: UNKNOWN
   14 |         __analyzer_eval(2-a > 0-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:15:9: warning: UNKNOWN
   15 |         __analyzer_eval(2-a > 1-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:16:9: warning: TRUE
   16 |         __analyzer_eval(2-a > 2-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
Compiler returned: 0
```

[Bug analyzer/109193] GCC Static Analyzer does not know "1-a > 0-b" in the true branch of "if (a < b && 0 < a) "

[geoffreydgr at icloud dot com]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=109193

--- Comment #1 from Geoffrey <geoffreydgr at icloud dot com> ---
It does not know "b > 0" under the if condition that "a>0 && b > a" either.

See it live: https://godbolt.org/z/1aGds8aTq

[Bug analyzer/109193] GCC Static Analyzer does not know "1-a > 0-b" in the true branch of "if (a < b && 0 < a) "

[dmalcolm at gcc dot gnu.org]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=109193

David Malcolm <dmalcolm at gcc dot gnu.org> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|UNCONFIRMED                 |RESOLVED
         Resolution|---                         |DUPLICATE

--- Comment #2 from David Malcolm <dmalcolm at gcc dot gnu.org> ---
As per bug 109194, I'm not convinced all of these definitely hold e.g. when a
or b are INT_MAX or INT_MIN.

The constraint_manager has some heuristics to try to handle common cases, but
ultimately we're probably going to want to hand this off to an SMT solver (PR
104940)

*** This bug has been marked as a duplicate of bug 104940 ***