Unsoundness: const declared objects are writable

[docprofsky]

VeriFast produces unit-fraction heap chunks for const-qualified variables, allowing them to be written to. This is inconsistent with C11 §6.7.3 paragraph 6 and creates an unsoundness with both GCC and Clang.

Below is a demonstration of the problem and a link to Compiler Explorer showing the output of GCC and Clang.
https://godbolt.org/z/5j74EPMrG

#include <assert.h>

void char_set(char *a)
//@ requires character(a, _);
//@ ensures character(a, 'b');
{
  a[0] = 'b';
}

int main(void)
//@ requires true;
//@ ensures true;
{
  const char z = 0;
  char_set((char *)&z);
  assert(z == 'b');

  return 0;
}

Output of verification, compilation, and execution:

$ ~/verifast-21.04-152-g6ba67172/bin/verifast const2.c && gcc -std=c11 -O3 -Wall -Wextra -Wpedantic -Werror const2.c && ./a.out
const2.c
0 errors found (4 statements verified)
Linking...
Program linked successfully.
a.out: const2.c:16: main: Assertion `z == 'b'' failed.
Aborted (core dumped)