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 (14 lines) | stat: -rw-r--r-- 520 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
 
CORE
main.c
--dfcc main --apply-loop-contracts
^Decreases clause is not side-effect free.$
^EXIT=6$
^SIGNAL=0$
--
--
This test fails because the decreases clause contains a function call. Decreases
clauses must not contain loops, since we want to ensure that the
calculation of decreases clauses will terminate. To enforce this requirement,
for now, we simply ban decreases clauses from containing function calls.
In the future, we may allow function calls (but definitely not loops) to appear
inside decreases clauses.