tautschnig
Follow
Popular repositories
1,323 contributions in the last year
Less
More
Activity overview
Contributed to
diffblue/cbmc,
sosy-lab/sv-benchmarks,
tautschnig/fshell-w2t
and 5 other
repositories
Contribution activity
June 2021
tautschnig has no activity
yet for this period.
May 2021
Created 54 commits in 1 repository
Created a pull request in diffblue/cbmc that received 9 comments
[RFC] Two new failing tests demonstrating updates outside member bounds
These examples write to a member different from the access path being used, yet within the object bounds. Each commit message has a non-empty bod…
+245
−16
•
9
comments
Opened 36 other pull requests in 1 repository
diffblue/cbmc
24
merged
12
open
- XML trace test: do not hard-code pointer bit pattern
- bv_pointerst: use convert instead of convert_bv for Boolean expression
- Binary comparison <, <=, >, >= over pointers requires same-object
- simplify_inequality_address_of only supports (not)equal
- bv_pointerst: sum over pointer offsets is restricted to offset bits
- Equip bv_pointerst::postponedt with a constructor
- Remove conversion_failed(exprt, bvt)
- bv_pointerst: else case is just for byte updates
- bv_pointerst::offset_arithmetic: de-duplicate code
- Upgrade CaDiCaL to 1.4.0
- Concurrency: treat updates to an unknown field as atomic
- Dirty locals copied across threads require program-order constraints [depends-on: #6121]
- Concurrency: do not remove shared or dirty pointers from the value set
- Concurrency: ensure function name is correct when starting threads
- Concurrency: do not lose L2 entries of procedure-local variables
- Use simplify_exprtt::resultt in pre-order simplification steps
- Update SV-COMP performance testing tool to 2020/2021
- Value sets: fix byte extracts from structs
- Test contracts/quantifiers-exists-ensures-02 was fixed via c29b69ab49
- Remove broken-smt-backend tags where tests currently pass
- goto-instrument/wmm: do not lookup non-existent symbols in the namespace
- boolbv_index: preserve endianness when generating byte extract
- Detect use of alloca-allocated object after leaving its scope
- Move cbmc/alloca1 to cbmc-library
- CBMC library: fix dead code in pipe()
- Some pull requests not shown.
Reviewed 27 pull requests in 1 repository
diffblue/cbmc 27 pull requests
- Fix CMake doc target
- Adds get_predecessors() to grapht
- Binary comparison <, <=, >, >= over pointers requires same-object
- Add UNIMPLEMENTED_FEATURE macro
- Allow quantifiers within loop invariants
- Use FloatingPoint theory when using --cprover-smt2
- Add start of foundational work for incremental SMT2 solving support
- [RFC] Two new failing tests demonstrating updates outside member bounds
- Upgrade CaDiCaL to 1.4.0
- Concurrency: treat updates to an unknown field as atomic
- Fix side-effect check on loop invariants
- Fix replace_return
- Restore missing header <ctime> causing Visual Studio build to fail.
- Visual Studio compilation documentation
- Restructure compilation documentation
- variants of r/w_ok
- Statement List: Jump instructions
- add missing <algorithm> includes
- Add various formatters
- Add CMake support for building and linking against CaDiCaL using the IPASIR interface
- Fix WIN32 -Werror build error
- (un)reachable functions: valid JSON even without source locations
- Do not assume that build architecture has byte/char==8 bits
- Manage lifetime of MiniSat and Glucose solver pointers using unique_ptr
- Remove unnecessary includes
- Some pull request reviews not shown.
Created an issue in sosy-lab/benchexec that received 1 comment
Feature request: merging tables of different benchmark sets
Apologies if this is already available and I just failed to find the right option: table-generator nicely combines multiple runs over the same set …
1
comment