public inbox for gcc-bugs@sourceware.org
help / color / mirror / Atom feed
* [Bug analyzer/109063] New: GCC Static Analyzer evaluates `e == &d + 1` to be UNKNOWN with the fact that `e == &d`
@ 2023-03-08  8:41 geoffreydgr at icloud dot com
  2023-05-04 14:12 ` [Bug analyzer/109063] " geoffreydgr at icloud dot com
  0 siblings, 1 reply; 2+ messages in thread
From: geoffreydgr at icloud dot com @ 2023-03-08  8:41 UTC (permalink / raw)
  To: gcc-bugs

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

            Bug ID: 109063
           Summary: GCC Static Analyzer evaluates `e == &d + 1` to be
                    UNKNOWN with the fact that `e == &d`
           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: ---

Hi, David. I found a problem that GCC Static Analyzer evaluates `e == &d + 1`
to be UNKNOWN with the fact that `e == &d`.  
Maybe GCC Static Analyzer should have the ability to evaluates `e == &d + 1` to
be FALSE ?

See it live: https://godbolt.org/z/Wcd4T1jGa.

Input:
```c
void __analyzer_eval();
void __analyzer_describe();

void c()
{
    int d = 42;
    int *e = &d;

    if (e == &d)
    {
        __analyzer_describe(0, e);
        __analyzer_describe(0, &d + 1);

        __analyzer_eval(e == &d + 1);
        __analyzer_eval(e + 1 == &d + 1);
    }
}
```

Output:
```bash
<source>: In function 'c':
<source>:11:9: warning: svalue: '&d'
   11 |         __analyzer_describe(0, e);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~
<source>:12:9: warning: svalue: '(&d+(sizetype)4)'
   12 |         __analyzer_describe(0, &d + 1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:14:9: warning: UNKNOWN
   14 |         __analyzer_eval(e == &d + 1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:15:9: warning: TRUE
   15 |         __analyzer_eval(e + 1 == &d + 1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Compiler returned: 0

```

^ permalink raw reply	[flat|nested] 2+ messages in thread

* [Bug analyzer/109063] GCC Static Analyzer evaluates `e == &d + 1` to be UNKNOWN with the fact that `e == &d`
  2023-03-08  8:41 [Bug analyzer/109063] New: GCC Static Analyzer evaluates `e == &d + 1` to be UNKNOWN with the fact that `e == &d` geoffreydgr at icloud dot com
@ 2023-05-04 14:12 ` geoffreydgr at icloud dot com
  0 siblings, 0 replies; 2+ messages in thread
From: geoffreydgr at icloud dot com @ 2023-05-04 14:12 UTC (permalink / raw)
  To: gcc-bugs

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

Geoffrey <geoffreydgr at icloud dot com> changed:

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

--- Comment #1 from Geoffrey <geoffreydgr at icloud dot com> ---
invalid case because of UB

^ permalink raw reply	[flat|nested] 2+ messages in thread

end of thread, other threads:[~2023-05-04 14:12 UTC | newest]

Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-03-08  8:41 [Bug analyzer/109063] New: GCC Static Analyzer evaluates `e == &d + 1` to be UNKNOWN with the fact that `e == &d` geoffreydgr at icloud dot com
2023-05-04 14:12 ` [Bug analyzer/109063] " geoffreydgr at icloud dot com

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).