From c04b2ffe61ef0361d4a121593ca90f07b11f65a6 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Fri, 14 Aug 2020 12:57:31 -0600 Subject: [PATCH] Updated usage documentation to account for new encoding flags We do not have `--bit-precise` flag any more for example. --- docs/usage-notes.md | 26 +++++++++++++------------- lib/smack/SmackOptions.cpp | 4 ++-- 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/docs/usage-notes.md b/docs/usage-notes.md index de6825971..246c697c5 100644 --- a/docs/usage-notes.md +++ b/docs/usage-notes.md @@ -32,11 +32,11 @@ of `x`, in the 3rd iteration) for the assertion to be reachable. ## Bitwise Operations and Integer Casts If the program to verify contains bitwise operations or integer casts, then the -flag `--bit-precise` may be required. The reason is that SMACK uses the SMT -theory of integers to encode machine integers by default, where bitwise -operations are encoded using uninterpreted functions returning arbitrary values. -Furthermore, precise encoding is required to handle integer signedness casts, -which is not also enabled automatically. +flag `--integer-encoding=bit-vector` may be required. The reason is that SMACK +uses the SMT theory of integers to encode machine integers by default, where +bitwise operations are encoded using uninterpreted functions returning +arbitrary values. Furthermore, precise encoding is required to handle integer +signedness casts, which is not also enabled automatically. The following program demonstrate the problems in the presence of bitwise operations. @@ -72,11 +72,11 @@ Some steps in the error trace are omitted. As you can see, the concrete values of `y` in the error trace before and after the bitwise right shift operation do not follow its semantics because it is modeled as an uninterpreted function. -In this case, we need the `--bit-precise` flag that, as its name indicates, -enables bit-precise modeling of machine integers. +In this case, we need the `--integer-encoding=bit-vector` flag that, as its +name indicates, enables bit-precise modeling of machine integers. ``` -$ smack a.c --bit-precise +$ smack a.c --integer-encoding=bit-vector SMACK program verifier version 1.9.0 SMACK found no errors with unroll bound 1. ``` @@ -91,11 +91,11 @@ Similar to machine integers, floating-point numbers and arithmetic are modeled using the theory of integers and uninterpreted functions, respectively. Therefore, if the assertions to verify depend on precise modeling of floating-point representations, the flag `--float` is needed. Note that -occasionally `--bit-precise` has to be used in addition to `--float`, in -particular when casts between floating-point numbers and integers are present. -Moreover, reasoning about floating-point numbers is often very slow. Please let -us know if you encounter any performance issues. We can share some experiences -that may ease the situation. +occasionally `--integer-encoding=bit-vector` has to be used in addition to +`--float`, in particular when casts between floating-point numbers and integers +are present. Moreover, reasoning about floating-point numbers is often very +slow. Please let us know if you encounter any performance issues. We can share +some experiences that may ease the situation. ## Concurrency Reasoning about pthreads is supported by SMACK with the flag `--pthread`. Please diff --git a/lib/smack/SmackOptions.cpp b/lib/smack/SmackOptions.cpp index 935b53dc6..295e397af 100644 --- a/lib/smack/SmackOptions.cpp +++ b/lib/smack/SmackOptions.cpp @@ -38,11 +38,11 @@ const llvm::cl::opt SmackOptions::SourceLocSymbols( llvm::cl::desc("Include source locations in generated code.")); llvm::cl::opt SmackOptions::BitPrecise( - "bit-precise", llvm::cl::desc("Model non-pointer values as bit vectors.")); + "bit-precise", llvm::cl::desc("Model integer values as bit-vectors.")); const llvm::cl::opt SmackOptions::BitPrecisePointers( "bit-precise-pointers", - llvm::cl::desc("Model pointers and non-pointer values as bit vectors.")); + llvm::cl::desc("Model pointer values as bit-vectors.")); const llvm::cl::opt SmackOptions::AddTiming("timing-annotations",