cbmc generated 0 vcc(s), always successful

[reico ming]

I have installed CBMC version 5.41.0 (cbmc-5.41.0) 64-bit x86_64 windows for my Visual Studio 2019 and I tried to exam a bug project. but it shows verification successfully.

And I tried to install CBMC version 5.10 (cbmc-5.10) 64-bit x86_64 linux for my subsystem linux. When it is done, I think this problem would be solved. I am sorry to tell this still fails.

Why this happen! I really need your help.

[Thomas Spriggs]

Hi

Assuming you were expecting cbmc to detect the out of bounds array access, you need to pass the --pointer-check argument to cbmc in order to enable bounds checking. Hope that helps.

Thomas

--

---
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 on the web, visit https://groups.google.com/d/msgid/cprover-support/80d55c2f-b17e-4c03-873b-ee784cf30ddbn%40googlegroups.com.

Diffblue Ltd, a company registered in England and Wales number 09958102. Registered office 10 St Ebbes Street, Oxford, OX1 1PT, UK