Martin Wehking
Martin Wehking
This draft PR introduces an analysis for affine equalities (ref: [Michael Karr , 1976](https://scholar.google.com/scholar_url?url=https://idp.springer.com/authorize/casa%3Fredirect_uri%3Dhttps://link.springer.com/content/pdf/10.1007/BF00268497.pdf%26casa_token%3DjHkKNvRPTY4AAAAA:yxzkcPFZP1RWxLZY-TWAg7cO8EfC0Txc78-CTZiDMFnyvkXp54p3s6RHEnxG0Auh7NRZELlImjxkZTat&hl=en&sa=T&oi=gsb-gga&ct=res&cd=0&d=14162577617566575899&ei=444CYu9y-pXL1g-ynpHACg&scisig=AAGBfm24cgr8mbazZ4npHDMjTnSTHqGDUA)) that can be run independently from the already existing apron analyses. Abstract states in the newly...
The following tests fail: - [ ] [sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.yml](file:///home/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c) - [ ] ([sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.yml](file:///home/sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c) with the following exception (the same for both): `Fatal error: exception IntDomain.IncompatibleIKinds("ikinds unsigned long long and unsigned int...
The following test becomes true but should actually be false: - [ ] sv-benchmarks/c/ldv-validator-v0.8/linux-stable-8817633-1-144_2a-drivers--staging--media--easycap--easycap.ko-entry_point_ldv-val-v0.8.cil.out.c I've used the following settings: ``` { "ana": { "sv-comp": { "enabled": true, "functions": true },...
CI testing for [UR PR #1538](https://github.com/oneapi-src/unified-runtime/pull/1538)
Add CMake to emit .bc files when compiling devicelib libraries to bitcode for NVPTX. Make the driver consume these files. This is a WIP with many sledgehammer-like additions and many...
Create one single bitcode library for NVPTX by compiling each libdev file into bitcode first, linking these together and running opt on them. Strip away metadata by reusing prepare_builtins from...
_Note: This patch is based on [15048](https://github.com/intel/llvm/pull/15048) (Not merged yet) and links against the final resulting bitcode library that is created through that patch_ Use the `-mlink-builtin-bitcode` flag to link...