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 (20 lines) | stat: -rw-r--r-- 791 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
 
CORE
main.c
--dfcc main --replace-call-with-contract cmp
^EXIT=10$
^SIGNAL=0$
^\[main\.assertion\.1\] line \d+ expecting SUCCESS: SUCCESS$
^\[main\.assertion\.2\] line \d+ expecting FAILURE: FAILURE$
^\[main\.assertion\.3\] line \d+ expecting SUCCESS: SUCCESS$
^\[main\.assertion\.4\] line \d+ expecting FAILURE: FAILURE$
^\*\* 2 of \d+ failed
^VERIFICATION FAILED$
--
--
This test checks that the return value of a replaced function call is made 
nondet at each replacement site.
The replaced function is called twice. Each call is expected to have a different
return value. If the return value of the call is not made nondet at each
replacement, it would be subject to contradictory constraints
(from the post conditions) and the assertions expected to fail would 
be vacuously satisfied.