Michael Tautschnig
Michael Tautschnig
Requested feature: `cbmc` and also `goto-instrument` can be invoked with `--validate-goto-model` to perform consistency checks on the GOTO model. `cbmc` furthermore supports `--validate-ssa-equation` to enable consistency checks on the formula...
The following tasks either aren't memory safe or have a wrong verdict for unreach-call (see [CBMC's results](https://sv-comp.sosy-lab.org/2021/results/results-verified/cbmc.results.SV-COMP21.All.table.html#/table?filter=0(0*status*(category(in(wrong)))))): - [ ] c/ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko.cil.out.yml -> #1274 - [ ] c/ldv-linux-3.0/module_get_put-drivers-net-atl1c-atl1c.ko.cil.out.yml - [ ]...
... other than those explicitly listed in the SV-COMP rules. As initially many benchmarks will violate this check, a blacklist needs to be maintained. I will push for this as...
Various device driver benchmarks either completely lack initialisation of pointers passed around or do not suitably initialise members of allocated storage. See #1049 for a (likely incomplete) list of benchmarks,...
Hi, In #4, #5, #6 I have provided patches for those benchmarks that I have submitted or feel somewhat responsible for. check-blacklist nevertheless still lists 3560 broken benchmarks, which ought...
* TeX_read returns a `bool`, which will be `_Bool` when `stdbool.h` is available. * `px_fopen` requires a function (pointer) that takes a `char *` argument.
Revert the change to `scripts/setup/ubuntu/install_doc_deps.sh` done in #3004 once https://github.com/dylanowen/mdbook-graphviz has released a new version with consistent dependencies (their CI is also failing in https://github.com/dylanowen/mdbook-graphviz/pull/106 and https://github.com/dylanowen/mdbook-graphviz/pull/104).
Requires support in CBMC. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Requires support in CBMC. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Requires fixes in CBMC's sqrt* implementations. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.