Unsupported definition of pointer assignment in assigns clause

[LangInteger]

See the below code:

#include "stdint.h"
#include <limits.h>

uint32_t x;
uint32_t pointer;

/*@ requires x > INT_MIN;
    requires x + 5 < INT_MAX;
    assigns x \from x;
    ensures x == \old(x) + 5;
*/
void func1(void)
{
  x = x + 5;
}

/*@ requires *(uint32_t *)pointer > INT_MIN;
    requires *(uint32_t *)pointer + 5 < INT_MAX;
    assigns *(uint32_t *)pointer \from *(uint32_t *)pointer;
    ensures *(uint32_t *)pointer == \old(*(uint32_t *)pointer) + 5;
*/
void func2(void)
{
  *((uint32_t*) pointer) = *((uint32_t*) pointer) + 5;
}

/*@ relational 
  \callset(\call(func1, id1),\call(func2, id2)) 
    ==> \at(x, Pre_id1)== \at(*(uint32_t *)pointer, Pre_id2)
    ==> \at(x,Post_id1) == \at(*(uint32_t *)pointer,Post_id2);
*/

The code can work with frama-c -wp, the output:

[kernel] Parsing test_1.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] Proved goals:    4 / 4
  Qed:             2  (0.25ms-1ms)
  Alt-Ergo :       2  (4ms-6ms) (41)
[wp] test_1.c:22: Warning: 
  Memory model hypotheses for function 'func2':
  /*@ behavior wp_typed:
        requires \separated((uint32_t *)pointer, &pointer); */
  void func2(void);

But as I want to prove the relational property, when running withframa-c -rpp -rpp-pro, it will complain:

[kernel] Parsing test_1.c (with preprocessing)
[rpp] ***************************************
[rpp] Rpp start
[rpp] ***************************************
[rpp] test_1.c:28: User Error: 
  Unsupported definition of pointer assignment in assigns clause:
   *((uint32_t *)pointer)
[kernel] Plug-in rpp aborted: invalid user input.

Will this be supported in RPP. Highly appreciate it if there is any workaround for this (without modifying the global variable declaration).

[lyonel2017]

Sorry for the late reply.

This example will not be supported by RPP in the near future, due to limitations of the theory currently used in the tool. Unfortunately, I can't see a workaround for your example without changing the declaration of the global variable.

Work is in progress on a new approach that will support such examples. But I can't say whether it will be available in RPP.

[LangInteger]

Thanks!