[Bug analyzer/109365] New: Double delete yields -Wanalyzer-use-after-free instead of -Wanalyzer-double-free

["priour.be at gmail dot com" <gcc-bugzilla@gcc.gnu.org>]

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

            Bug ID: 109365
           Summary: Double delete yields -Wanalyzer-use-after-free instead
                    of -Wanalyzer-double-free
           Product: gcc
           Version: 13.0
            Status: UNCONFIRMED
          Severity: normal
          Priority: P3
         Component: analyzer
          Assignee: dmalcolm at gcc dot gnu.org
          Reporter: priour.be at gmail dot com
  Target Milestone: ---
            Target: x86_64-pc-linux-gnu
             Build: 13.0.1 20230328 (experimental)

Double delete does not result in a -Wanalyzer-double-free warning as expected,
but rather into -Wanalyzer-use-after-free warning. 

Using the following reproducer:
// file ../../double_delete_test.cpp
struct A {int a; int b;};
int main () {
    A* a = new A();
    delete a;
    delete a;
    return 0;
}

Then compiling with 
./xg++ -B. -S -fanalyzer -Wanalyzer-double-free ../../double_delete_test.cpp
../../double_delete_test.cpp: In function ‘int main()’:
../../double_delete_test.cpp:9:1: warning: use after ‘delete’ of ‘a’ [CWE-416]
[-Wanalyzer-use-after-free]
    9 | }
      | ^
  ‘int main()’: events 1-7
    |
    |    5 |     A* a = new A();
    |      |                  ^
    |      |                  |
    |      |                  (1) state of ‘&HEAP_ALLOCATED_REGION(10)’:
‘start’ -> ‘nonnull’ (NULL origin)
    |    6 |     delete a;
    |      |     ~~~~~~~~      
    |      |     |      |
    |      |     |      (3) ...to here
    |      |     |      (4) deleted here
    |      |     (2) following ‘true’ branch...
    |    7 |     delete a;
    |      |     ~~~~~~~~      
    |      |     |      |
    |      |     |      (6) ...to here
    |      |     (5) following ‘true’ branch...
    |    8 |     return 0;
    |    9 | }
    |      | ~                 
    |      | |
    |      | (7) use after ‘delete’ of ‘a’; deleted at (4)
    |

I also attempted with -fno-exception, but no impact was observer on the graphs
nor the output.
With the addition of -fanalyzer-fine-grained, I observed than each delete
statement is actually split into two:
delete a;
becomes in the ipa form
<bb 3> :
  *a.0_9 ={v} {CLOBBER};
  operator delete (a.0_9, 8);

The exploded-graph shows that the second '*a.1_12 ={v} {CLOBBER};' dereference
is responsible for the -Wanalyzer-use-after-free, and changes the state of the
allocated region from 'freed' to 'stop', which causes the actual following
'operator delete' to not be detected as a double free.

I am still familiarizing myself with the gimplification and ssa passes, so I'm
yet unsure as to how to tackle this.
I'm still looking into this though, and would gladly receive your pointers. 

(Note: sorry David, I've binged through bugzilla doc and gcc bugs page yet I
cannot seem to find the way to add this to the 'analyzer-c++' block, nor do I
see the option in the advanced fields.)