goto-harness C output emits a spurious const on the typedef for const-qualified pointer parameters, producing non-compilable harness code

[Kacha345]

Summary

When a function takes a pointer to a const variable as a parameter (e.g. const uint8_t *h), goto-harness handles it incorrectly in its C output. The generated C source puts a const in the typedef of the pointed-to type — typedef const unsigned char uint8_t; — rather than leaving it on the parameter. goto-harness then declares its own scratch variable with that typedef and assigns a nondet value to it, which is now a write to a const object, so goto-cc refuses to compile the harness.

Steps to reproduce

bug.c:

#include <stdint.h>
unsigned f(const uint8_t *h) { return h[0]; }

$ goto-cc bug.c -o bug.gb
$ goto-harness bug.gb harness.c --harness-type call-function --function f --harness-function-name main
$ goto-cc harness.c bug.c -o out.gb
harness.c: In function 'type_constructor_uint':
harness.c:64:1: error: '*result_uint' is constant
   *result_uint = nondet;
CONVERSION ERROR

Cause

typedef const unsigned char uint8_t;          /* spurious 'const' on the typedef */

void type_constructor_uint(signed int depth_uint, uint8_t *result_uint)
{
  uint8_t nondet;
  *result_uint = nondet;                      /* assignment to a const object */
}

The const belongs to the parameter (const uint8_t *h), not to the type uint8_t (which is unsigned char). The C output has fused the parameter's qualifier into the typedef, so uint8_t now means const unsigned char everywhere in the file — including the harness's own writable scratch storage.

Full generated harness attached: goto-harness-const-repro.txt

Expected

The generated C should compile. The typedef should be typedef unsigned char uint8_t; — the const should stay at the explicit use site (const uint8_t *h, which goto-harness already emits correctly), so the harness can write to its own scratch storage while f still receives a const pointer.

Versions

• CBMC / goto-harness: 6.10.0 (latest release) — also reproduces on 6.9.0
• OS: Ubuntu 24.04, x86_64