niekbouman

Dear Nim-devs, About two years ago I wrote a C++ constexpr bigint library (https://github.com/niekbouman/ctbignum) Recently, I gave Nim a try and translated a small part of the library to Nim....

I recently learned from Jonathan Protzenko (Microsoft Research) that one of his colleagues, Marina Polubelova, is working on an F* (formally verified) implementation of bignum arithmetic, which compiles to C....

> * much faster than GMP: https://bluescarni.github.io/mppp/integer_benchmarks.html BTW, those benchmarks are a bit cherry-picking; as it only shows 1 and 2-limb sizes. As it was already concluded in this discussion...

Hi Michael (and/or others), I managed to get rid of this error by adding a missing function declaration in `smack.h`: ```cpp void __SMACK_check_overflow(int); ``` Now I am facing another issue,...

Good idea, I've added it as [issue 353](https://github.com/smackers/smack/issues/353).

I've opened a new issue for this `exit` related problem; see [359](https://github.com/smackers/smack/issues/359)

### Regression test (test.cpp) ```cpp extern "C" { #include } int main() { int x = 10; __SMACK_value(x); return 0; } ``` compiling with clang++-3.9 -std=c++14 -c -emit-llvm -o test.bc...

In C++, one typically uses a template-function for taking an argument of arbitrary type ```cpp template void __SMACK_value(T x); // accepts 1 arg of arbitrary type ``` Not sure though...

As a workaround, I've had success with the following 'hack': ```cpp extern "C" { //... #ifdef __cplusplus smack_value_t __SMACK_value(unsigned int*, ...); #else smack_value_t __SMACK_value(); #endif //... } // end of...

FYI, my C++ variant of `ct-verif`'s Tiny Encryption Algorithm C++ example is as follows: (note that `ct-verif` uses `smack` internally) ### invoking ct-verif The entry point should now be the...