[neeraj9]

Building on isolated alpine linux container indicated missing header during compilation from source

After patch

~/git/cbmc# ./build/bin/cbmc --version
6.11.0 (cbmc-6.11.0-41-g03bd0722c6-dirty)

Build Steps

apk add --no-cache \
    build-base \
    cmake \
    ninja \
    git \
    flex \
    bison \
    curl \
    patch \
    python3 \
    linux-headers

git clone https://github.com/diffblue/cbmc.git
cd cbmc

git submodule update --init

cmake -S . -B build \
    -G Ninja \
    -DCMAKE_BUILD_TYPE=Release \
    -DWITH_JBMC=OFF

cmake --build build --target cbmc -j 4

Short error

error: 'int64_t' does not name a type
note: 'int64_t' is defined in header '<cstdint>'

Detailed error:

[133/793] Building CXX object src/solvers/CMakeFiles/solvers.dir/strings/string_format_builtin_function.cpp.o
ninja: job failed: /usr/bin/ccache /usr/bin/c++ -DHAVE_MINISAT2 -DSATCHECK_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -I/root/git/cbmc/build/src -I/root/git/cbmc/src -I/root/git/cbmc/build/src/solvers -I/root/git/cbmc/src/solvers -I/root/git/cbmc/build/minisat2-src -I/root/git/cbmc/build/src/util -I/root/git/cbmc/src/util -I/root/git/cbmc/build/src/big-int -I/root/git/cbmc/src/big-int -I/root/git/cbmc/build/src/langapi -I/root/git/cbmc/src/langapi -Wall -Wpedantic -Werror -Wswitch-enum          -Wno-deprecated-declarations -Wno-maybe-uninitialized -O2 -std=c++17 -MD -MT src/solvers/CMakeFiles/solvers.dir/strings/string_format_builtin_function.cpp.o -MF src/solvers/CMakeFiles/solvers.dir/strings/string_format_builtin_function.cpp.o.d -o src/solvers/CMakeFiles/solvers.dir/strings/string_format_builtin_function.cpp.o -c /root/git/cbmc/src/solvers/strings/string_format_builtin_function.cpp
/root/git/cbmc/src/solvers/strings/string_format_builtin_function.cpp: In function 'std::vector<BigInt> deserialize_constant_int_arg(std::vector<BigInt>, unsigned int)':
/root/git/cbmc/src/solvers/strings/string_format_builtin_function.cpp:414:9: error: 'int64_t' does not name a type
  414 |   const int64_t int64_value =
      |         ^~~~~~~
/root/git/cbmc/src/solvers/strings/string_format_builtin_function.cpp:23:1: note: 'int64_t' is defined in header '<cstdint>'; this is probably fixable by adding '#include <cstdint>'
   22 | #include <util/simplify_expr.h>
  +++ |+#include <cstdint>
   23 |
/root/git/cbmc/src/solvers/strings/string_format_builtin_function.cpp:417:37: error: 'int64_value' was not declared in this scope
  417 |   const mp_integer mp_integer_value{int64_value};
      |                                     ^~~~~~~~~~~
/root/git/cbmc/src/solvers/strings/string_format_builtin_function.cpp:417:48: error: no matching function for call to 'BigInt::BigInt(<brace-enclosed initializer list>)'
  417 |   const mp_integer mp_integer_value{int64_value};
      |                                                ^
/root/git/cbmc/src/solvers/strings/string_format_builtin_function.cpp:417:48: note: there are 11 candidates
In file included from /root/git/cbmc/src/util/mp_arith.h:16,
                 from /root/git/cbmc/src/util/arith_tools.h:14,
                 from /root/git/cbmc/src/util/string_expr.h:15,
                 from /root/git/cbmc/src/solvers/strings/string_constraint.h:24,
                 from /root/git/cbmc/src/solvers/strings/string_constraint_generator.h:24,
                 from /root/git/cbmc/src/solvers/strings/string_builtin_function.h:7,
                 from /root/git/cbmc/src/solvers/strings/string_format_builtin_function.h:15,
                 from /root/git/cbmc/src/solvers/strings/string_format_builtin_function.cpp:16:
/root/git/cbmc/src/big-int/bigint.hh:172:3: note: candidate 1: 'BigInt::BigInt(const char*, onedig_t)'
  172 |   BigInt (char const *, onedig_t = 10) _fast;

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.