Discussions

• 1 You must be logged in to vote

  🙏

  Can smack generate boogie code which saves the metadata in llvm ir?

  Luweicai asked Mar 24, 2022 in Q&A · Answered

  

  

  1
• 1 You must be logged in to vote

  🙏

  What is the form of free loop invariant in the smack generated boogie code(from c)?

  Luweicai asked Jan 10, 2022 in Q&A · Unanswered

  

  

  1
• 2 You must be logged in to vote

  💡

  Idea: Use smack as a Clang drop-in replacement

  teaalltr started May 4, 2021 in Ideas

  

  

  1
• 1 You must be logged in to vote

  💡

  Use UBSan to warn integer sign casts

  shaobo-he started Jan 17, 2021 in Ideas

  

  

  0
• 1 You must be logged in to vote

  💡

  Produce executable error trace in bitcode

  shaobo-he started Jan 5, 2021 in Ideas

  

  

  0
• 1 You must be logged in to vote

  💡

  Simplify memory safety checking

  shaobo-he started Dec 23, 2020 in Ideas

  

  

  0
• 1 You must be logged in to vote

  💬

  Welcome to SMACK Discussions!

  zvonimir started Dec 14, 2020 in General

  

  

  0
• 1 You must be logged in to vote

  💡

  Proposal: capture C expression to boogie_si_record_* calls

  shaobo-he started Dec 9, 2020 in Ideas

  

  

  0
• 1 You must be logged in to vote

  💡

  Motivation for context-sensitive DSA/memory model

  shaobo-he started Nov 21, 2020 in Ideas

  

  

  3
• 1 You must be logged in to vote

  💡

  Proposal: convert C string zero initializers to memset

  shaobo-he started Dec 5, 2020 in Ideas

  

  

  0
• 1 You must be logged in to vote

  💡

  Proposal: revive compilation database frontend

  shaobo-he started Nov 19, 2020 in Ideas

  

  

  1
• 1 You must be logged in to vote

  💡

  Proposal: enable trap instruction checking

  shaobo-he started Nov 19, 2020 in Ideas

  

  

  0
• 1 You must be logged in to vote

  💡

  Proposal: generalize integer overflow checking to undefined behavior checking

  shaobo-he started Nov 19, 2020 in Ideas

  

  

  0
• 1 You must be logged in to vote

  💡

  Integrate SMACK into cargo

  shaobo-he started May 4, 2020 in Ideas

  

  

  0
• 1 You must be logged in to vote

  💡

  Verifying the function call sequence

  StanPlatinum started Mar 12, 2020 in Ideas

  

  

  

  

  4