AliveToolkit alive2 issues

AliveToolkit / alive2

Automatic verification of LLVM optimizations

MIT License

769 stars 97 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

ReadMe, `alive-tv --help`: correct timeout, BUILD_SHARED_LIBS optional

#992 FlashSheridan closed 9 months ago
0
unconditionally check for source functions that are UB for all executions, but don't error out

#991 regehr closed 9 months ago
1
startswith() now gives a warning on my machine due to being deprecated

#990 regehr closed 9 months ago
0
Bump github/codeql-action from 2 to 3

#989 dependabot[bot] closed 9 months ago
0
int2ptr support

#988 nunoplopes closed 4 weeks ago
0
ir/memory.cpp:309: smt::expr IR::Byte::nonPoison() const: Assertion `!np.isValid() || ptrNonpoison().eq(np == 1)' failed.

#987 regehr closed 9 months ago
0
False negative in LoopVectorizePass on runtime-checks-difference.ll in Compiler Explorer instance

#986 FlashSheridan closed 9 months ago
9
ReadMe: metadata, SDK, appending other opt options

#985 FlashSheridan closed 9 months ago
0
False positive with hoisted load of `dereferenceable` pointer.

#984 fhahn closed 9 months ago
1
Bad perf with memory refinement query

#983 regehr opened 10 months ago
3
floating point value mismatches from the middle-end

#982 regehr closed 10 months ago
3
refinement failure roundtripping through the AArch64 backend for an fadd with rounding=dynamic, exceptions=strict

#981 regehr closed 10 months ago
2
runtime error: reference binding to null pointer of type 'const struct FloatType'

#980 regehr closed 10 months ago
0
Timout on alive-tv

#979 Ralender closed 10 months ago
4
Add support for disjoint

#978 dtcxzyw closed 10 months ago
1
Assertion failed: (high >= low && high < bits()), function extract, file expr.cpp, line 1809.

#977 regehr closed 10 months ago
0
"ERROR: Invalid expr" with -tgt-is-asm

#976 regehr closed 10 months ago
0
Odd behavior with function calls, alive says functions don't return or trigger UB

#975 jeremy-rifkin closed 10 months ago
6
Severe Z3 error: sort is not a bit-vector [code=3]

#974 regehr closed 10 months ago
0
Is a specific version of llvm needed to build alive2?

#973 jeremy-rifkin closed 10 months ago
7
adding --disable-undef-input and --disable-poison-input creates a value mismatch (with --tgt-is-asm)

#972 regehr closed 10 months ago
8
poison problem with the asm memory model

#971 regehr closed 10 months ago
1
poison problem with the asm memory model

#970 regehr closed 10 months ago
0
Missing support for memory(argmem) with escaped ptrs through ptr2int

#969 regehr opened 10 months ago
5
performance problem with indirection

#968 regehr opened 10 months ago
0
crash

#967 regehr closed 10 months ago
0
Infer nsw/nuw/etc attributes in tgt

#966 nunoplopes opened 10 months ago
2
segfault

#965 regehr closed 10 months ago
1
--verbose and --no-timeout options for opt-alive.sh

#964 FlashSheridan closed 10 months ago
0
Assertion `!bid.isValid() || !offset.isValid() || p.bits() == totalBits()' failed.

#963 regehr closed 10 months ago
0
Infer poison-generating flags

#962 dtcxzyw closed 10 months ago
1
False positive for the same GEP pointer after unrolling the loop

#961 XChy closed 10 months ago
1
crash

#960 regehr closed 10 months ago
4
as Nuno suggested, add @llvm.assert which in Alive is just an alias

#959 regehr closed 10 months ago
0
False positive with function argument refinement: local -> non-local

#958 nunoplopes opened 11 months ago
1
ReadMe: Diagnosing Unsoundness Reports

#957 FlashSheridan closed 10 months ago
0
Add support for writable attribute

#956 nunoplopes closed 3 months ago
0
ARM support

#955 regehr closed 10 months ago
0
Escaped pointers have non-deterministic address

#954 dzaima opened 11 months ago
3
Implement initial memory counterexample printing

#953 nunoplopes closed 10 months ago
0
Alive2 recognized infinite empty loop as flat ret

#952 XChy closed 11 months ago
1
Incorrect transform in loop not detected

#951 nikic closed 11 months ago
0
False negative with loops + memory

#950 dtcxzyw closed 11 months ago
3
Friendlier CMake output and ReadMe tips

#949 FlashSheridan closed 11 months ago
0
ReadMe: Mac deployment workaround, new PM example

#948 FlashSheridan closed 11 months ago
0
More ReadMe tweaks: fix my paths, use real files

#947 FlashSheridan closed 11 months ago
0
should it invalid for divided by 0 ?

#946 vfdff closed 11 months ago
1
Tweak ReadMe: Variablize uses of ~/llvm in the build instructions,

#945 FlashSheridan closed 11 months ago
0
Synthesize RHS constants

#944 nunoplopes opened 11 months ago
1
[alive2]ERROR: Unsupported attribute: noalias

#943 erickq closed 1 year ago
1

Previous Next