Fix and cross-reference C11 undefined behavior documentation

doc/C/c11-undefined-behavior.html

@@ -643,7 +643,7 @@
 – A file with the same name as one of the standard headers, not provided as part of the
 implementation, is placed in any of the standard places that are searched for included
 source files (7.1.2).</td>
-<td></td>
+<td>no</td>
 </tr>
 
 <tr><td>
@@ -960,7 +960,7 @@
 &ndash; The string pointed to by the mode argument in a call to the
 <code>fopen</code> function does not
 exactly match one of the specified character sequences (7.21.5.3).</td>
-<td>mo</td>
+<td>no</td>
 </tr>
 
 <tr><td>

doc/architectural/c11-ub-coverage-plan.md

@@ -0,0 +1,105 @@
+# Covering C11 Undefined Behaviors in CBMC
+
+This document tracks which C11 undefined behaviors (Appendix J.2) CBMC
+does not yet check and categorizes them by feasibility. The reference
+list is in `doc/C/c11-undefined-behavior.html`. Row numbers below refer
+to that table.
+
+## Tier 1 — Front-end / type-checker checks
+
+Small effort each. These are compile-time constraints the C front-end or
+linker could reject or warn about.
+
+| Row | J.2 ref | Description | Status |
+|-----|---------|-------------|--------|
+| 4 | 5.1.2.2.1 | `main()` not in specified form | |
+| 8 | 6.2.2 | Same identifier with internal and external linkage | |
+| 32 | 6.4.2.2 | Explicit declaration of `__func__` | |
+| 38–40 | 6.5.2.2 | Calls without prototype / wrong argument count or types | partially checked |
+| 41 | 6.5.2.2 | Function defined with incompatible type | |
+| 59 | 6.7 | Object with no linkage and incomplete type | |
+| 60 | 6.7.1 | Block-scope function with non-`extern` storage class | |
+| 61 | 6.7.2.1 | Struct/union without named members | |
+| 63 | 6.7.2.3 | Incomplete struct/union not completed in same scope | |
+| 66 | 6.7.3 | Function type with type qualifiers | |
+| 70 | 6.7.4 | Inline + external linkage but not defined in TU | |
+| 71 | 6.7.4 | `_Noreturn` function returns | |
+| 84 | 6.9 | Missing/duplicate external definitions | |
+| 85–86 | 6.9.1 | K&R function definition issues | |
+| 88 | 6.9.1 | `}` reached in non-void function, value used | |
+| 89 | 6.9.2 | Internal linkage + incomplete type + tentative def | |
+
+## Tier 2 — Runtime checks (goto-check instrumentation)
+
+Medium effort each. These require adding assertions during the
+goto-check pass, similar to existing bounds/pointer/overflow checks.
+
+| Row | J.2 ref | Description | Status |
+|-----|---------|-------------|--------|
+| 5 | 5.1.2.4 | Data races | CBMC has concurrency support |
+| 10 | 6.2.4 | Use of pointer to ended-lifetime object | extend pointer-check |
+| 11 | 6.2.4 | Use of indeterminate (uninitialized) value | |
+| 12–13 | 6.2.6.1 | Trap representations | |
+| 18 | 6.3.1.5 | Float demotion out of range | extend float-overflow-check |
+| 24 | 6.3.2.3 | Pointer-to-integer conversion out of range | extend conversion-check |
+| 25 | 6.3.2.3 | Misaligned pointer conversion | |
+| 26 | 6.3.2.3 | Function pointer type mismatch on call | extend function-pointer removal |
+| 35 | 6.5 | Unsequenced side effects | needs sequence-point analysis |
+| 37 | 6.5 | Strict aliasing violation | needs type-based alias analysis |
+| 46 | 6.5.6 | Pointer arithmetic producing out-of-bounds result | partially covered |
+| 50 | 6.5.6 | Pointer subtraction result not representable in `ptrdiff_t` | |
+| 54 | 6.5.16.1 | Assignment to overlapping object | |
+| 62 | 6.7.2.1 | Access flexible array member with no elements | extend bounds-check |
+| 65 | 6.7.3 | Volatile access through non-volatile lvalue | |
+| 68–69 | 6.7.3.1 | `restrict` pointer violations | needs restrict analysis |
+| 77 | 6.7.6.3 | `static` array parameter size not met at call site | |
+| 136–143 | 7.16 | `va_list` / `va_arg` misuse | |
+| 176 | 7.22.3 | Use of zero-size allocation | extend pointer-check |
+| 178 | 7.22.3.1 | `aligned_alloc` invalid alignment | add check in model |
+| 179 | 7.22.3 | Double free / free of non-malloc'd pointer | partially covered |
+
+## Tier 3 — C library model improvements
+
+Small effort each, mostly mechanical: add precondition assertions to
+existing library models in `src/ansi-c/library/`.
+
+| Row | J.2 ref | Description | Status |
+|-----|---------|-------------|--------|
+| 108 | 7.1.4 | Invalid argument to library function | |
+| 113 | 7.4 | Character function argument not `EOF`/`unsigned char` | |
+| 126–127 | 7.13.2.1 | `longjmp` to nonexistent/modified environment | |
+| 146–175 | 7.21 | stdio / file I/O UBs (~30 items) | |
+| 153–168 | 7.21.6 | printf/scanf format string UBs (~16 items) | partial printf model exists |
+| 176,178–181 | 7.22.3 | malloc/realloc/calloc UBs | |
+| 184 | 7.22.4.6 | Modifying `getenv`/`strerror` result | |
+| 187–189 | 7.22.5 | `bsearch`/`qsort` invalid arguments | |
+| 190,200 | 7.22.7 | Multibyte conversion state | |
+| 193–194 | 7.24.4.5 | `strxfrm`/`strtok` misuse | |
+| 197 | 7.27.3.1 | `asctime` out-of-range argument | |
+
+## Tier 4 — Out of scope
+
+These are preprocessor-phase, translation-phase, or environmental issues
+that CBMC cannot meaningfully check because it operates on
+already-preprocessed code.
+
+Rows: 1–3, 6–7, 14, 16, 28–31, 34, 42, 72–74, 76, 79–80, 90–99,
+101–107, 110–112, 114–118, 120–125, 128–135, 144–145, 182–183,
+185–186, 195–196, 198–203.
+
+~70 items. Not planned.
+
+## Recommended priorities
+
+1. **Quick wins**: [71] `_Noreturn` returns and [88] non-void function
+   fall-through — common bugs, easy to add as goto-check assertions.
+
+2. **High value**: [11] indeterminate values, [25] misaligned pointers,
+   [50] `ptrdiff_t` overflow, [77] `static` array parameter size —
+   catch real bugs users care about.
+
+3. **Library models**: printf/scanf format checking [153–168] covers 16
+   UBs at once. stdio state tracking [146–175] is another large cluster.
+
+4. **Long-term**: [5] data races, [35] sequence points, [37] strict
+   aliasing, [68–69] `restrict` — architecturally hard but high value.

doc/cprover-manual/properties.md

@@ -54,7 +54,8 @@ We won't explain the properties in detail. Most of them
 relate to behaviors that are left undefined by the respective language
 semantics. For a discussion on why these behaviors are usually very
 undesirable, read [this](http://blog.regehr.org/archives/213) blog post
-by John Regehr.
+by John Regehr. For a complete list of C11 undefined behaviors and which
+ones CBMC checks, see [doc/C/c11-undefined-behavior.html](../C/c11-undefined-behavior.html).
 
 All the properties described above are *reachability* properties. They
 are always of the form