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-- 436 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
 
CORE
dummy.c
--function main --harness-type call-function
\[default_serve\.assertion\.1\] line \d+ assertion 0 && \"default serve should fail so we can see it is being called\": FAILURE
^EXIT=10$
^SIGNAL=0$
--
static void default_serve
--
When running the harness we should run into the assertion failure from the
static default_serve function, but the harness C code should not contain this
or any other static functions or variables.