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 (11 lines) | stat: -rw-r--r-- 330 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
 
CORE
main.c
--enforce-contract f1 --enforce-contract nextIdx
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
--
This test also ensures that assigns clauses correctly check for global
variables modified by subcalls. In this case, since the assigns clause
doesn't include the modified global variable, the verification should failed.