[QUESTION] Conversion Error

[MJJ-Shuai]

PS E:\C++Project\Test2\Test2> cbmc --no-propagation --cvc5 --outfile Test2.smt2 Test2.cpp
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 windows
Parsing Test2.cpp
Test2.cpp
Converting
Type-checking Test2
file C:\Program Files (x86)\Windows Kits\10\include\10.0.22621.0\ucrt\stddef.h line 25: symbol '__nullptr' is unknown
CONVERSION ERROR

The above is the ERROR I encountered, while the below is my source program. As you can see, I want to use CBMC to generate the SMT formula corresponding to my C code, but I encounter CONVERSION ERROR, I want to know the specific reason?

#include <stdio.h>
#include <stdint.h>
#include <stdlib.h>
#include <assert.h>

#define Fr_N64 4
#define Fr_SHORT           0x00000000
#define Fr_MONTGOMERY      0x40000000
#define Fr_SHORTMONTGOMERY 0x40000000
#define Fr_LONG            0x80000000
#define Fr_LONGMONTGOMERY  0xC0000000

typedef uint64_t FrRawElement[Fr_N64];
typedef unsigned long long u64;
typedef uint32_t u32;
typedef uint8_t u8;

#pragma pack(push, 1)
struct FrElement {
    int32_t shortVal;
    uint32_t type;
    FrRawElement longVal;
};
#pragma pack(pop)

typedef struct FrElement FrElement;
typedef FrElement* PFrElement;

void Fr_copy(PFrElement r, const PFrElement a) {
    *r = *a;
    assert(r->shortVal = a->shortVal);
    //printf("shortVal: %d\n", r->shortVal);
    //printf("type: %u\n", r->type);
    //printf("longVal: ");
    //for (int i = 0; i < Fr_N64; ++i) {
    //    printf("%llu ", r->longVal[i]);
    //}
    //printf("\n");
}

int main() {
    FrElement Fr_q = { 0, 0x80000000, {0x43e1f593f0000001, 0x2833e84879b97091, 0xb85045b68181585d, 0x30644e72e131a029} };
    FrElement Fr_R2 = { 0, 0x80000000, {0x1bb8e645ae216da7, 0x53fe3ab1e35c59e3, 0x8c49833d53bb8085, 0x0216d0b17f4e44a5} };
    FrElement Fr_R3 = { 0, 0x80000000, {0x5e94d8e1b4bf0040, 0x2a489cbe1cfbb6b8, 0x893cc664a19fcfed, 0x0cf8594b7fcc657c} };

    size_t arrayLength = 10; // Example length
    FrElement* signalValues = (FrElement*)malloc(arrayLength * sizeof(FrElement));
    //if (signalValues == NULL) {
    //    fprintf(stderr, "Memory allocation failed\n");
    //    return 1;
    //}

    // Initialize the array elements as needed
    for (size_t i = 0; i < arrayLength; ++i) {
        signalValues[i].shortVal = i;
        signalValues[i].type = i * 10;
        // Initialize longVal as needed
    }

    u64 mySignalStart = 1ULL;
    PFrElement aux_dest = &signalValues[mySignalStart + 0];
    Fr_copy(aux_dest, &signalValues[mySignalStart + 2]);

    // Clean up
    free(signalValues);
    return 0;
}

[kroening]

We currently only recognise __nullptr in clang and g++ mode, but Visual Studio appears to have it too: https://learn.microsoft.com/en-us/cpp/extensions/nullptr-cpp-component-extensions?view=msvc-170

[kroening]

In the meantime, as a workaround, may I suggest you write the code as plain C code, as opposed to C++ code. Your program doesn't have any C++ in it, and it will avoid triggering the error.

[MJJ-Shuai]

@kroening Thank you for your reply. In addition, I have another question: Does CBMC support gmp large number arithmetic library？

[kroening]

No, but it has its own built-in unbounded integer, arbitrary-width integer, fixed-point and floating-point types.