search

ftsrg / gazer

An LLVM-based formal verification frontend for C programs.
24 stars 5 forks source link

Using constant zero-aggregate initializers results in a crash #65

Closed sallaigy closed 3 years ago

sallaigy commented 3 years ago

LLVM represents zero-initialized aggregate values with the ConstantAggregateZero class, for which do not have support yet in the memory models, causing a crash.

LLVM IR to reproduce:

; RUN: %bmc -skip-pipeline -bound 1 "%s" | FileCheck "%s"
; CHECK: Verification SUCCESSFUL

@a = internal unnamed_addr global [2 x double] zeroinitializer, align 16

define dso_local i32 @main() {
bb:
  %tmp = load i64, i64* bitcast ([2 x double]* @a to i64*), align 16
  store i64 %tmp, i64* bitcast (double* getelementptr inbounds ([2 x double], [2 x double]* @a, i64 0, i64 1) to i64*), align 8
  ret i32 0
}

Exhibited behavior:

Unhandled value type
UNREACHABLE executed at /home/gyula/projects/gazer/src/LLVM/Automaton/InstToExpr.cpp:898!