"AssertionError: Non-external global variable with no initializer" in LLVM frontend
Executing
scripts/cpa.sh -generateCFA test.ll
with test.ll as follows
; Declare a global variable causing the error.
@var = extern_weak global i8*
; Print "hello world" as execution would otherwise fail for another reason.
; Declare the string constant as a global constant.
@.str = private unnamed_addr constant [13 x i8] c"hello world\0A\00"
; External declaration of the puts function
declare i32 @puts(i8* nocapture) nounwind
; Definition of main function
define i32 @main() { ; i32()*
; Convert [13 x i8]* to i8*...
%cast210 = getelementptr [13 x i8], [13 x i8]* @.str, i64 0, i64 0
; Call puts function to write out the string to stdout.
call i32 @puts(i8* %cast210)
ret i32 0
}
; Named metadata
!0 = !{i32 42, null, !"string"}
!foo = !{!0}
causes an AssertionError
with the following stack trace:
Exception in thread "main" java.lang.AssertionError: Non-external global variable with no initializer: @var = extern_weak global i8*
at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.visitGlobalItem(CFABuilder.java:1904)
at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.iterateOverGlobals(CFABuilder.java:207)
at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.visit(CFABuilder.java:176)
at org.sosy_lab.cpachecker.cfa.parser.llvm.CFABuilder.build(CFABuilder.java:162)
at org.sosy_lab.cpachecker.cfa.parser.llvm.LlvmParser.buildCfa(LlvmParser.java:93)
at org.sosy_lab.cpachecker.cfa.parser.llvm.LlvmParser.parseFile(LlvmParser.java:55)
at org.sosy_lab.cpachecker.cfa.CFACreator.parseToCFAs(CFACreator.java:630)
at org.sosy_lab.cpachecker.cfa.CFACreator.parseFileAndCreateCFA(CFACreator.java:440)
at org.sosy_lab.cpachecker.core.CPAchecker.parse(CPAchecker.java:485)
at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:344)
at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:169)