cpp2v error in arm68v8/debian : getCallingConv: FunctionDecl type is not a FunctionType

[aa755]

# ../../_build/default/fmdeps/cpp2v-core/rocq-bluerock-cpp2v/build-dune/cpp2v demo.cpp -- -stdlib=libc++
# ../../_build/default/fmdeps/cpp2v-core/rocq-bluerock-cpp2v/build-dune/cpp2v demo.cpp -o demo.v -- -stdlib=libc++
</usr/include/c++/v1/__memory/addressof.h:22:1, line:24:1> (Atomic _Atomic(bool)): warning: unsupported type
</usr/include/c++/v1/__memory/addressof.h:56:1, col:29> (Atomic _Atomic(bool)): warning: unsupported type
</usr/include/aarch64-linux-gnu/bits/math-vector.h:118:1 <Spelling=line:116:18>, line:118:56> (Vector __attribute__((neon_vector_type(4))) float): warning: unsupported type
float): warning: unsupported type
/usr/include/aarch64-linux-gnu/bits/math-vector.h:118:1 <Spelling=/usr/include/aarch64-linux-gnu/bits/math-vector.h:116:18> (Function _ZGVnN4vv_atan2f(__f32x4_t, __f32x4_t)): error: getCallingConv: FunctionDecl type is not a FunctionType

Steps to reproduce:

docker pull arm64v8/ubuntu

create a docker container from that image and inside it, set up fm-workspace. at its root, create setupDebian.sh containing the following and run it from there.

#!/bin/bash

export DEBIAN_FRONTEND=noninteractive

apt update -y
apt install -y software-properties-common
apt-add-repository -y ppa:swi-prolog/stable

apt install -y git emacs opam swi-prolog pkg-config cmake build-essential gzip gpg

wget -q https://apt.llvm.org/llvm.sh
chmod +x llvm.sh
./llvm.sh 18 all
# ^ llvm.sh suggests adding LFLAGS/CPPFLAGS. consider adding ghem

opam init --disable-sandboxing --yes
echo "eval \$(opam env)" >> ~/.bashrc
eval $(opam env) # without this, opam-installed binaries cannot be found
chown -R root:root . # needed when running in a debian docker image and this directory was copied to the docker container via docker cp

echo export PATH=/usr/lib/llvm-18/bin/:\$PATH >> ~/.bashrc

Then, do ./setup-fmdeps.sh as usual and put demo.cpp somewhere (e.g. cpp2v/tests) and run cpp2v to it as in the above error message

[aa755]

contents of demo.cpp:

#include <thread>
//#include <utility>
//#include <iostream>

using uint = unsigned int;

uint x = 0;
uint y;

void foo() {
    y=0;
    y=x+1;
}

int a = 0;
int b = 0;
void sfoo() {
    b=a+1;
}

int *ptr;

void fooptr () {
    ptr = &a;
}

/*
 pre |-- loopinv 
 loopinv ** [| loopcond |] {loopbody} loopinv
 loopinv ** [| ~loopcondition |] => postcondition (a'=gcd av ab) */

uint gcd(uint a, uint b) {
    while (b != 0) {
        uint temp = b;
        b = a % b;
        a = temp;
    }
    return a;
}

void gcd(const uint &a, const uint &b, uint &result) {
    result=gcd(a,b);
}


template<typename LambdaStruct>
class Thread {
    const LambdaStruct lambda;
    std::thread worker;

public:
    void start() {
        worker = std::thread([this]() {
            lambda();
        });
    }

    void join() {
        if(worker.joinable())
            worker.join();
    }

    ~Thread() {
        if(worker.joinable())
            worker.join();
    }

    Thread(const Thread&) = delete;
    Thread& operator=(const Thread&) = delete;

    Thread(Thread&& other)
        : lambda(std::move(other.lambda)), worker(std::move(other.worker)) {}

    Thread& operator=(Thread&& other) {
        if (this != &other)
        {
            lambda = std::move(other.lambda);
            worker = std::move(other.worker);
        }
        return *this;
    }

    Thread(const LambdaStruct &lambda) : lambda(lambda) {}
};

void parallel_gcd_lcm(const uint &a, const uint &b, uint &gcd_result, uint &lcm_result) {
    Thread t1([&gcd_result, &a, &b]() {
           gcd(a, b, gcd_result);
       });
    t1.start();
    uint product=a*b;// pretend this is expensive, e.g. 1000 bit numbers
    t1.join();
    lcm_result=product/gcd_result;
}
/*
Just Before `t1.start()`:
┌───────────────────────────────────────────────────────────────┐
│  Main Thread owns:                                            │
│  gcd_result |-> anyR "unsigned int" 1                         │
│  lcm_result |-> anyR "unsigned int" 1                         │
│  a |-> primR "unsigned int" qa av                             │
│  b |-> primR "unsigned int" qb bv                             │
└───────────────────────────────────────────────────────────────┘

Just after t1.start:
┌───────────────────────────────────────────┬───────────────────────────────────────────┐
│  Child Thread (t1)                        │  Main Thread (parent)                     │
│  ──────────────────────────────────────   │  ──────────────────────────────────────   │
│  gcd_result |-> anyR "unsigned int" 1     │  lcm_result |-> anyR "unsigned int" 1     │
│  a |-> primR "unsigned int" (qa/2) av     │  a |-> primR "unsigned int" (qa/2) av     │
│  b |-> primR "unsigned int" (qb/2) bv     │  b |-> primR "unsigned int" (qb/2) bv     │
└───────────────────────────────────────────┴───────────────────────────────────────────┘

 */

void parallel_gcd_lcm_wrong(const uint &a, const uint &b, uint &gcd_result, uint &lcm_result) {
    Thread t1([&gcd_result, &a, &b]() {
        gcd(a,b, gcd_result);
    });
    t1.start();
    uint product=a*b;
    lcm_result=product/gcd_result;
    t1.join();
}

uint parallel_gcd_lcm2(uint a, uint b, uint &gcd_result) {
    Thread t1([&gcd_result, a, b]() {
          gcd_result=gcd(a,b);
       });
    t1.start();
    uint product=a*b;// pretend this is expensive, e.g. 1000 bit numbers
    t1.join();
    return product/gcd_result;
}

[aa755]

No such error with libstdc++ (when -stdlib=libc++ is dropped from the cpp2v invocation, after apt install libstdc++-14-dev)