<html>
<head>
<base href="https://bugs.llvm.org/">
</head>
<body><table border="1" cellspacing="0" cellpadding="8">
<tr>
<th>Bug ID</th>
<td><a class="bz_bug_link
bz_status_NEW "
title="NEW - clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:102: clang::ento::ConstraintManager::ProgramStatePair clang::ento::ConstraintManager::assumeDual(clang::ento::ProgramStateRef, clang::ento::DefinedSVal): Assertion `assume(State, Co"
href="https://bugs.llvm.org/show_bug.cgi?id=40231">40231</a>
</td>
</tr>
<tr>
<th>Summary</th>
<td>clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:102: clang::ento::ConstraintManager::ProgramStatePair clang::ento::ConstraintManager::assumeDual(clang::ento::ProgramStateRef, clang::ento::DefinedSVal): Assertion `assume(State, Co
</td>
</tr>
<tr>
<th>Product</th>
<td>clang
</td>
</tr>
<tr>
<th>Version</th>
<td>trunk
</td>
</tr>
<tr>
<th>Hardware</th>
<td>PC
</td>
</tr>
<tr>
<th>OS</th>
<td>All
</td>
</tr>
<tr>
<th>Status</th>
<td>NEW
</td>
</tr>
<tr>
<th>Severity</th>
<td>enhancement
</td>
</tr>
<tr>
<th>Priority</th>
<td>P
</td>
</tr>
<tr>
<th>Component</th>
<td>Static Analyzer
</td>
</tr>
<tr>
<th>Assignee</th>
<td>dcoughlin@apple.com
</td>
</tr>
<tr>
<th>Reporter</th>
<td>vlad@tsyrklevich.net
</td>
</tr>
<tr>
<th>CC</th>
<td>dcoughlin@apple.com, llvm-bugs@lists.llvm.org
</td>
</tr></table>
<p>
<div>
<pre>Created <span class=""><a href="attachment.cgi?id=21294" name="attach_21294" title="Unreduced input">attachment 21294</a> <a href="attachment.cgi?id=21294&action=edit" title="Unreduced input">[details]</a></span>
Unreduced input
On a Linux build of recent clang with Z3 4.8.4 (built using
<a href="https://github.com/vlad902/kernel-uninitialized-memory-checker/blob/master/build.sh">https://github.com/vlad902/kernel-uninitialized-memory-checker/blob/master/build.sh</a>)
I was able to hit the titled exception with the following reduced input:
long a() {
int b = a();
b++;
while (b) {
b > 0;
unsigned c = b;
c > 5;
b += 5;
}
}
and the following command:
~/kernel-uninitialized-memory-checker/build/bin/clang-8 -cc1 -triple
x86_64-unknown-linux-gnu -analyze -analyzer-store=region
-analyzer-opt-analyze-nested-blocks -analyzer-checker=core -nobuiltininc
-std=gnu89 -analyzer-output=html -o /tmp/out -x c reduced.c
Note that with an (identically?) built clang on OSX I was not able to hit this
exception. I'm not sure why. The full output is:
clang-8:
/root/kernel-uninitialized-memory-checker/llvm/tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:102:
clang::ento::ConstraintManager::ProgramStatePair
clang::ento::ConstraintManager::assumeDual(clang::ento::ProgramStateRef,
clang::ento::DefinedSVal): Assertion `assume(State, Cond, false) && "System is
over constrained."' failed.
Stack dump:
0. Program arguments:
/root/kernel-uninitialized-memory-checker/build/bin/clang-8 -cc1 -triple
x86_64-unknown-linux-gnu -analyze -analyzer-store=region
-analyzer-opt-analyze-nested-blocks -analyzer-checker=core -nobuiltininc
-std=gnu89 -analyzer-output=html -o /tmp/out -x c reduced.c
1. <eof> parser at end of file
2. While analyzing stack:
#0 Calling a at line 2
#1 Calling a at line 2
#2 Calling a at line 2
#3 Calling a at line 2
#4 Calling a
3. reduced.c:7:5: Error evaluating statement
4. reduced.c:7:5: Error evaluating statement
#0 0x000055c3d07d4ea0 llvm::sys::PrintStackTrace(llvm::raw_ostream&)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x32f4ea0)
#1 0x000055c3d07d4f33 PrintStackTraceSignalHandler(void*)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x32f4f33)
#2 0x000055c3d07d2a13 llvm::sys::RunSignalHandlers()
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x32f2a13)
#3 0x000055c3d07d48b6 SignalHandler(int)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x32f48b6)
#4 0x00007f2ab2966dd0 __restore_rt
(/lib/x86_64-linux-gnu/libpthread.so.0+0x12dd0)
#5 0x00007f2ab0f6d077 gsignal (/lib/x86_64-linux-gnu/libc.so.6+0x41077)
#6 0x00007f2ab0f4e535 abort (/lib/x86_64-linux-gnu/libc.so.6+0x22535)
#7 0x00007f2ab0f4e40f __tls_get_addr (/lib/x86_64-linux-gnu/libc.so.6+0x2240f)
#8 0x00007f2ab0f5e142 (/lib/x86_64-linux-gnu/libc.so.6+0x32142)
#9 0x000055c3d294bdbf
clang::ento::ConstraintManager::assumeDual(llvm::IntrusiveRefCntPtr<clang::ento::ProgramState
const>, clang::ento::DefinedSVal)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x546bdbf)
#10 0x000055c3d294c0a9
clang::ento::ProgramState::assume(clang::ento::DefinedOrUnknownSVal) const
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x546c0a9)
#11 0x000055c3d2ec57f8
clang::ento::ExprEngine::evalEagerlyAssumeBinOpBifurcation(clang::ento::ExplodedNodeSet&,
clang::ento::ExplodedNodeSet&, clang::Expr const*)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x59e57f8)
#12 0x000055c3d2ebd8d2 clang::ento::ExprEngine::Visit(clang::Stmt const*,
clang::ento::ExplodedNode*, clang::ento::ExplodedNodeSet&)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x59dd8d2)
#13 0x000055c3d2eb9852 clang::ento::ExprEngine::ProcessStmt(clang::Stmt const*,
clang::ento::ExplodedNode*)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x59d9852)
#14 0x000055c3d2eb8a18
clang::ento::ExprEngine::processCFGElement(clang::CFGElement,
clang::ento::ExplodedNode*, unsigned int, clang::ento::NodeBuilderContext*)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x59d8a18)
#15 0x000055c3d2ea3da5 clang::ento::CoreEngine::HandlePostStmt(clang::CFGBlock
const*, unsigned int, clang::ento::ExplodedNode*)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x59c3da5)
#16 0x000055c3d2ea2ab4
clang::ento::CoreEngine::dispatchWorkItem(clang::ento::ExplodedNode*,
clang::ProgramPoint, clang::ento::WorkListUnit const&) (.localalias.0)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x59c2ab4)
#17 0x000055c3d2ea2600
clang::ento::CoreEngine::ExecuteWorkList(clang::LocationContext const*,
unsigned int, llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x59c2600)
#18 0x000055c3d28baa96
clang::ento::ExprEngine::ExecuteWorkList(clang::LocationContext const*,
unsigned int)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x53daa96)
#19 0x000055c3d28bdc35 (anonymous
namespace)::AnalysisConsumer::RunPathSensitiveChecks(clang::Decl*,
clang::ento::ExprEngine::InliningModes, llvm::DenseSet<clang::Decl const*,
llvm::DenseMapInfo<clang::Decl const*> >*)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x53ddc35)
#20 0x000055c3d28bda70 (anonymous
namespace)::AnalysisConsumer::HandleCode(clang::Decl*, unsigned int,
clang::ento::ExprEngine::InliningModes, llvm::DenseSet<clang::Decl const*,
llvm::DenseMapInfo<clang::Decl const*> >*)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x53dda70)
#21 0x000055c3d28bc732 (anonymous
namespace)::AnalysisConsumer::HandleDeclsCallGraph(unsigned int)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x53dc732)
#22 0x000055c3d28bcba3 (anonymous
namespace)::AnalysisConsumer::runAnalysisOnTranslationUnit(clang::ASTContext&)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x53dcba3)
#23 0x000055c3d28bcdf6 (anonymous
namespace)::AnalysisConsumer::HandleTranslationUnit(clang::ASTContext&)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x53dcdf6)
#24 0x000055c3d301ca94 clang::ParseAST(clang::Sema&, bool, bool)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x5b3ca94)
#25 0x000055c3d127c9d1 clang::ASTFrontendAction::ExecuteAction()
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x3d9c9d1)
#26 0x000055c3d127c3c2 clang::FrontendAction::Execute()
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x3d9c3c2)
#27 0x000055c3d1209676
clang::CompilerInstance::ExecuteAction(clang::FrontendAction&)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x3d29676)
#28 0x000055c3d13d546b
clang::ExecuteCompilerInvocation(clang::CompilerInstance*)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x3ef546b)
#29 0x000055c3cf279314 cc1_main(llvm::ArrayRef<char const*>, char const*,
void*) (/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x1d99314)
#30 0x000055c3cf26f033 ExecuteCC1Tool(llvm::ArrayRef<char const*>,
llvm::StringRef)
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x1d8f033)
#31 0x000055c3cf27009f main
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x1d9009f)
#32 0x00007f2ab0f5009b __libc_start_main
(/lib/x86_64-linux-gnu/libc.so.6+0x2409b)
#33 0x000055c3cf26b39a _start
(/root/kernel-uninitialized-memory-checker/build/bin/clang-8+0x1d8b39a)
I've attached the unreduced input for verification.</pre>
</div>
</p>
<hr>
<span>You are receiving this mail because:</span>
<ul>
<li>You are on the CC list for the bug.</li>
</ul>
</body>
</html>