Gidon Ernst
Gidon Ernst
For example benchexec -Dfoo=bar benchmark.xml would replace `${foo}` by `bar` in benchmark.xml just like `${rundefinition_name}`.
For example: https://github.com/sosy-lab/sv-benchmarks/blob/b61ec96df19679bf5a65ec48ec1651ad2c8a0374/c/aws-c-common/aws_byte_buf_cat_harness.i#L9113 leading to undefined behavior in the test harness.
It would be nice to include a new function into the benchmark rules void *__VERIFIER_base_pointer(void *ptr); that denotes the base pointer of an object, similarly to [__CPROVER_POINTER_OBJECT](http://www.cprover.org/cprover-manual/api/) as supported by...
The following program trips up handling of single-bit values vs booleans in the backend, such a single-bit value can be passed either as test to `_sym_build_bool_to_bits` or as constraint `_sym_push_path_constraint`,...