Re: Specifiy unwind bound for recursion loop

[Peter Schrammel]

There's already a ticket for this: https://github.com/diffblue/cbmc/issues/1680

Yes, it would be very useful if --show-loops could display this.

Using --unwind-set already works regardless. The loop id of the recursion is simply the function name of the recursive function.

Peter

On 12.03.20 12:23, Andreas Tiemeyer wrote:

The process for assigning a specific unwind bounds for a loop in the program is:

1. list all loops using --show-loop
2. set the bound of the target loop using --unwindset

Does this work for recursion loops? They don't show when using --show-loops, so it's not clear how to set their unwind limit.

Is this a know limitation, or am I missing something?

Andreas  

--

---
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/3ece6407-24e6-49e5-b78b-555aa15be0f0%40googlegroups.com.