diff options
| author | Clifford Wolf <clifford@clifford.at> | 2017-05-17 21:07:54 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2017-05-17 21:07:54 +0200 |
| commit | 2122ae69b3c12057d3d4a4f5060bbdba70462d6a (patch) | |
| tree | 5a9594af83a7bbdfbf6e5fa8ce0f95865b196a68 /backends/simplec | |
| parent | 662a04781504c95f77e76e0026247806ac410cfc (diff) | |
| download | yosys-2122ae69b3c12057d3d4a4f5060bbdba70462d6a.tar.gz yosys-2122ae69b3c12057d3d4a4f5060bbdba70462d6a.tar.bz2 yosys-2122ae69b3c12057d3d4a4f5060bbdba70462d6a.zip | |
Add workaround for CBMC bug to SimpleC back-end
Diffstat (limited to 'backends/simplec')
| -rw-r--r-- | backends/simplec/simplec.cc | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/backends/simplec/simplec.cc b/backends/simplec/simplec.cc index 5768e3499..c9656caff 100644 --- a/backends/simplec/simplec.cc +++ b/backends/simplec/simplec.cc @@ -482,7 +482,9 @@ struct SimplecWorker string a_expr = a.wire ? util_get_bit(work->prefix + cid(a.wire->name), a.wire->width, a.offset) : a.data ? "1" : "0"; string b_expr = b.wire ? util_get_bit(work->prefix + cid(b.wire->name), b.wire->width, b.offset) : b.data ? "1" : "0"; string s_expr = s.wire ? util_get_bit(work->prefix + cid(s.wire->name), s.wire->width, s.offset) : s.data ? "1" : "0"; - string expr = stringf("%s ? %s : %s", s_expr.c_str(), b_expr.c_str(), a_expr.c_str()); + + // casts to bool are a workaround for CBMC bug (https://github.com/diffblue/cbmc/issues/933) + string expr = stringf("%s ? (bool)%s : (bool)%s", s_expr.c_str(), b_expr.c_str(), a_expr.c_str()); log_assert(y.wire); funct_declarations.push_back(util_set_bit(work->prefix + cid(y.wire->name), y.wire->width, y.offset, expr) + |