File: warn_cannot_wildcard.expect

package info (click to toggle)
sail-ocaml 0.19.1%2Bdfsg5-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 18,008 kB
  • sloc: ml: 75,941; ansic: 8,848; python: 1,342; exp: 560; sh: 474; makefile: 218; cpp: 36
file content (8 lines) | stat: -rw-r--r-- 519 bytes parent folder | download
1
2
3
4
5
6
7
8
Warning: Required literal warn_cannot_wildcard.sail:10.14-17:
10 |        (Some(0b1), _)         => (),
   |              ^-^
   | 
Sail cannot simplify the above pattern match:
This bitvector pattern literal must be kept, as it is required for Sail to show that the surrounding pattern match is complete.
When translated into prover targets (e.g. Lem, Coq) without native bitvector patterns, they may be unable to verify that the match covers all possible cases.