STL support

[Arjya Das]

Hi,

    

    Does the current version of CBMC support vectors and list? I have set the cpp standard to c++11 (as both c++98, c++03 standard results in "unimplemented" error for vectors). I am getting the following parsing error for the regression test regression/cbmc-cpp/Vector1/main.cpp:

CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Parsing regression/cbmc-cpp/Vector1/main.cpp
file /usr/include/c++/12/type_traits line 67: parse error before 'constexpr operator value_type ('
file /usr/include/c++/12/type_traits line 74: parse error before '} ; template <'
file /usr/include/c++/12/type_traits line 2091: parse error before 'struct __attribute__ ( ('
file /usr/include/c++/12/type_traits line 2093: parse error before '} ; template <'
file /usr/include/c++/12/type_traits line 2112: parse error before 'struct __attribute__ ( ('
file /usr/include/c++/12/type_traits line 2114: parse error before '} ; template <'
file /usr/include/c++/12/type_traits line 2306: parse error before '> struct __common_type_impl {'
file /usr/include/c++/12/type_traits line 2312: parse error before '} ; template <'
file /usr/include/c++/12/type_traits line 2524: parse error before '> struct __inv_unwrap {'
file /usr/include/c++/12/type_traits line 2528: parse error before '} ; template <'
PARSING ERROR

Arjya

[Nyx Brain, Martin]

On Fri, 2024-03-08 at 22:17 -0800, 'Arjya Das' via CProver Support
wrote:

>
> Hi,
>
>     Does the current version of CBMC support vectors and list?

Maybe. It depends which implementation of the STL you are using.

> I have set the cpp standard to c++11 (as both c++98, c++03 standard
> results in "unimplemented" error for vectors). I am getting the
> following parsing error for the regression test regression/cbmc-
> cpp/Vector1/main.cpp:
>
> CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
> Parsing regression/cbmc-cpp/Vector1/main.cpp
> file /usr/include/c++/12/type_traits line 67: parse error before
> 'constexpr operator value_type ('

<snip>

The problem is that most implementations of the STL use a lot of
template meta-programming. This means that to support even the most
basic code that #include <vector> with a modern, mainstream STL
implementation, you have to support a very large amount of template
code that is not really used anywhere but the internals of the STL and
maybe Boost and is completely irrelevant for what you are trying to
verify. This is a *huge* amount of work and so far no-one has been
willing to commit either the time or the funding to do it.

So what can you do?

A. Use a different STL implementation. An older one or one designed
for simpler targets might work.

B. You can write your own versions of the STL headers that you need,
maybe using the modelling features in CBMC
https://diffblue.github.io/cbmc/cprover-manual/index.html
This will likely perform much better than using a real STL.

C. At points there have been tools that translate C++ into C.

HTH

Cheers,
- Martin

--
Martin's office hours are Wednesday 14:00--16:00 in A309C or online.
They are first-come, first-served and there is no need to book.

[Mandayam Srivas]

What are the options and features that CBMC has to control the verbosity or to ellide specific parts of an error trace.  Specifically, can I ask it to suppress display of error trace at function/procedure invocation boundaries?

Thanks in advance for your information and help.

Srivas

PS

Does using CBMC in Visual Sudio Interface help matters?

[Mandayam Srivas]

To clarify, what I mean by "elliding" is I want to hide or suppress parts of error trace form being displayed for example at function invocation boundaries.  Thanks.

---

From: Mandayam Srivas <mksr...@hotmail.com>
Sent: Friday, April 18, 2025 9:28 AM
To: cprover...@googlegroups.com <cprover...@googlegroups.com>
Cc: Akhoury Shauryam <akh...@cmi.ac.in>; shobhits.mcs2023 <shobhits...@cmi.ac.in>
Subject: Elliding lines in display of error trace

 

[Peter Schrammel]

Srivas, you could use the XML (--xml-ui) or JSON (--json-ui) output options.

You could then pass the output through a postprocessor which gives you full control over what to retain (and is easier to handle than the plain text output).

Depending on what you want to do, also CBMC-Viewer could be useful: https://github.com/model-checking/cbmc-viewer

Peter

--

---
You received this message because you are subscribed to the Google Groups "CProver Support" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cprover-suppo...@googlegroups.com.
To view this discussion, visit https://groups.google.com/d/msgid/cprover-support/PNXP287MB40193DAF58D1E584B0073433C5BF2%40PNXP287MB4019.INDP287.PROD.OUTLOOK.COM.

[Mandayam Srivas]

Consider the following program stored in file powerOfNondet.c:

I expected unwinding assertions failure when I did the following, but it doesn't.  Can you provide an explanation why my expectation is wrong?

What exactly does CBMC do with recursion and unwinding-assertions check?

cbmc powerOfNondet.c --property main.assertion.2 --unwind 1 --unwinding-assertions

CBMC version 5.6 64-bit x86_64 macos

       //Unwinding Recursion

       unsigned int fib(unsigned int n) {

         if (n <= 1) return n;

         return (fib(n-1) + fib(n-2));

       } 

int main() {

  unsigned int i,j,k,x,z;

  int y,m,n;

    __CPROVER_assume(i <= 8);

       __CPROVER_assert(fib(i) < 10, "??");

}

[Peter Schrammel]

Srivas,

--unwind 1 means that unwinding is stopped after the first iteration/recursion. Conjecture: That means that you stop before reaching the unwinding assertion (as expected).

What happens if you use --unwind 2?

Peter

--

---
You received this message because you are subscribed to the Google Groups "CProver Support" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cprover-suppo...@googlegroups.com.

To view this discussion, visit https://groups.google.com/d/msgid/cprover-support/PN5P287MB4273633CD1341BDDC98E60FFC514A%40PN5P287MB4273.INDP287.PROD.OUTLOOK.COM.

[Mandayam Srivas]

That doesn't fail either.   I see not a single "unwinding assertion" failure until full recursion unnwinding depth.  Why?  I suspect the unwinding assertion VCC (when I checked) looks a bit suspect to me.

---

From: cprover...@googlegroups.com <cprover...@googlegroups.com> on behalf of Peter Schrammel <schra...@gmail.com>
Sent: Tuesday, September 16, 2025 7:53 PM
To: cprover...@googlegroups.com <cprover...@googlegroups.com>
Subject: Re: Unwinding assertions with recursion

 

To view this discussion, visit https://groups.google.com/d/msgid/cprover-support/CACcecPjYcerfKS2TzoftoorRgycF_SuHrkZRgmbQf7AHny994Q%40mail.gmail.com.