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-- 351 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
 
CORE dfcc-only
main.c
--dfcc main --enforce-contract foo --apply-loop-contracts
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
--
checks that when assignment lhs expressions have ternary expressions,
loop assigns clause checking correctly infers what gets assigned and
automatically tracks targets in the both the top level and the loop write sets.