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 (13 lines) | stat: -rw-r--r-- 431 bytes parent folder | download | duplicates (2) 
1
2
3
4
5
6
7
8
9
10
11
12
13
 
CORE
main.c
--dfcc main --enforce-contract foo
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
--
This test checks that verification succeeds if only expressions inside the assigns clause are assigned within the function.

Note: For all 'enforce' tests, nothing can be assumed about the return value of the function (as the function call is not replaced at this point).

To make such assumptions would cause verification to fail.