File: test.desc

package info (click to toggle)
cbmc 6.6.0-4
  • links: PTS
  • area: main
  • in suites: forky, sid, trixie
  • size: 153,852 kB
  • sloc: cpp: 386,459; ansic: 114,466; java: 28,405; python: 6,003; yacc: 4,552; makefile: 4,041; lex: 2,487; xml: 2,388; sh: 2,050; perl: 557; pascal: 184; javascript: 163; ada: 36
file content (10 lines) | stat: -rw-r--r-- 532 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
 
CORE
main.c
--vsd
^SIGNAL=0$
^EXIT=0$
--
--
This expression is derived from a real system under test. Due to inadvertent reevaluation of expression operands, all expression evaluations had geometric complexity (even more so in the presence of TOP values). This particular expression took nearly two hours to evaluate. Reworking to prevent repeated reevaluation brings this down to a few tenths.
See https://github.com/diffblue/cbmc/pull/6290
If this test appears to hang, the constant_evaluator is probably your first port of call.