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 (16 lines) | stat: -rw-r--r-- 678 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
 
CORE dfcc-only smt-backend broken-cprover-smt-backend
main.c
--dfcc main --apply-loop-contracts --enforce-contract foo --malloc-may-fail --malloc-fail-null _ --z3 --slice-formula --no-standard-checks
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
--

Tests support for quantifiers in loop contracts with the SMT backend.
When quantified loop invariants are used, they are inserted three times
in the transformed program (base case assertion, step case assumption,
step case assertion), and each occurrence needs to be rewritten with fresh
symbols for the quantified variables. The SMT solver would with an error
whenever this renaming is not properly done.