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 (12 lines) | stat: -rw-r--r-- 390 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
 
CORE
main.c
--no-malloc-may-fail --dfcc main --enforce-contract foo _ --no-standard-checks
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
--
Checks that assigns clause checking explicitly checks assignments to locally
declared symbols with composite types, when they are dirty.
Out of bounds accesses to locally declared arrays, structs, etc.
will be detected by assigns clause checking.