README.md: fix wrong URL for GitLab CI status badge image
pure/bmc-harness: prove lossless integer float range
Add a test harness that proves [-2²⁴, 2²⁴] is the range of integers that can
fit in a 32-bit float without losing any precision.
This is relevant because we convert between integers and floats.
posix: add app that uses pulseaudio
Not long ago, I deleted posix/app/ because it was unmaintained. However,
that version didn't create an audio stream, so it was of little use.
This version of posix/app gives us more traction: it creates an audio
stream with pulseaudio, which is still a pretty common audio middleware
thingy. It's a bit funny for the test suite to make sound, but this
ensures that posix/app is run on a regular basis. Maybe I'll get tired
of it soon?
sequencer: add BMC harness for tick_index_update
app: move format conversion into platform
contrib/debug-mcu: update MCU binary path
envsetup.sh: remove commented out code
bmc-harness: refactor
- Use __CPROVER_assume when testing injectivity
- Break up harness functions into roughly one property per function
- Name the slow properties as being slow rather than commenting them out
sampler: add const qualifier to a variable
sampler: rename interpolate_linear to interpolate
The function implements both zero-order hold and linear interpolation,
so the new name is more accurate.
sampler: add documentation comments
trigger: add documentation comment
util: add documentation comment
len: add documentation comment
bitset: add documentation comments
README.md: use diffblue's CBMC documentation link
Diffblue seems to be the current maintainer of CBMC. The previously linked
page for documentation is out of date and incomplete. The new link is for
current documentation.
README.md: add section for external documentation
These documents are important, but not well known. I expect
the links to break, but at least the documents are named.
mcu: initialize the bitset first
The bitset needs to be initialized before the interrupts happen.
Running it before _any_ peripherals are initialized removes any doubt.