-
Notifications
You must be signed in to change notification settings - Fork 274
Do not assume that build architecture has byte/char==8 bits #5962
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected] | |
|
||
#include "janalyzer_parse_options.h" | ||
|
||
#include <climits> | ||
#include <cstdlib> // exit() | ||
#include <fstream> | ||
#include <iostream> | ||
|
@@ -357,8 +358,9 @@ int janalyzer_parse_optionst::doit() | |
// Print a banner | ||
// | ||
log.status() << "JANALYZER version " << CBMC_VERSION << " " | ||
<< sizeof(void *) * 8 << "-bit " << config.this_architecture() | ||
<< " " << config.this_operating_system() << messaget::eom; | ||
<< sizeof(void *) * CHAR_BIT << "-bit " | ||
<< config.this_architecture() << " " | ||
<< config.this_operating_system() << messaget::eom; | ||
|
||
register_languages(); | ||
|
||
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -11,8 +11,9 @@ Author: Daniel Kroening, [email protected] | |
|
||
#include "jbmc_parse_options.h" | ||
|
||
#include <fstream> | ||
#include <climits> | ||
#include <cstdlib> // exit() | ||
#include <fstream> | ||
#include <iostream> | ||
#include <memory> | ||
|
||
|
@@ -484,8 +485,9 @@ int jbmc_parse_optionst::doit() | |
// | ||
// Print a banner | ||
// | ||
log.status() << "JBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8 | ||
<< "-bit " << config.this_architecture() << " " | ||
log.status() << "JBMC version " << CBMC_VERSION << " " | ||
<< sizeof(void *) * CHAR_BIT << "-bit " | ||
<< config.this_architecture() << " " | ||
<< config.this_operating_system() << messaget::eom; | ||
|
||
// output the options | ||
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected] | |
|
||
#include "convert_character_literal.h" | ||
|
||
#include <climits> | ||
|
||
#include <util/arith_tools.h> | ||
#include <util/c_types.h> | ||
#include <util/std_expr.h> | ||
|
@@ -51,7 +53,7 @@ exprt convert_character_literal( | |
for(unsigned i=0; i<value.size(); i++) | ||
{ | ||
mp_integer z=(unsigned char)(value[i]); | ||
z=z<<((value.size()-i-1)*8); | ||
z = z << ((value.size() - i - 1) * CHAR_BIT); | ||
x+=z; | ||
} | ||
|
||
|
@@ -84,7 +86,7 @@ exprt convert_character_literal( | |
for(unsigned i=0; i<value.size(); i++) | ||
{ | ||
mp_integer z=(unsigned char)(value[i]); | ||
z=z<<((value.size()-i-1)*8); | ||
z = z << ((value.size() - i - 1) * CHAR_BIT); | ||
x+=z; | ||
} | ||
|
||
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -11,8 +11,9 @@ Author: Daniel Kroening, [email protected] | |
|
||
#include "cbmc_parse_options.h" | ||
|
||
#include <fstream> | ||
#include <climits> | ||
#include <cstdlib> // exit() | ||
#include <fstream> | ||
#include <iostream> | ||
#include <memory> | ||
|
||
|
@@ -519,8 +520,9 @@ int cbmc_parse_optionst::doit() | |
// | ||
// Print a banner | ||
// | ||
log.status() << "CBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8 | ||
<< "-bit " << config.this_architecture() << " " | ||
log.status() << "CBMC version " << CBMC_VERSION << " " | ||
<< sizeof(void *) * CHAR_BIT << "-bit " | ||
<< config.this_architecture() << " " | ||
<< config.this_operating_system() << messaget::eom; | ||
|
||
// | ||
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -11,9 +11,10 @@ Author: Daniel Kroening, [email protected] | |
|
||
#include "goto_analyzer_parse_options.h" | ||
|
||
#include <climits> | ||
#include <cstdlib> // exit() | ||
#include <iostream> | ||
#include <fstream> | ||
#include <iostream> | ||
#include <memory> | ||
|
||
#include <ansi-c/ansi_c_language.h> | ||
|
@@ -402,8 +403,9 @@ int goto_analyzer_parse_optionst::doit() | |
// Print a banner | ||
// | ||
log.status() << "GOTO-ANALYSER version " << CBMC_VERSION << " " | ||
<< sizeof(void *) * 8 << "-bit " << config.this_architecture() | ||
<< " " << config.this_operating_system() << messaget::eom; | ||
<< sizeof(void *) * CHAR_BIT << "-bit " | ||
<< config.this_architecture() << " " | ||
<< config.this_operating_system() << messaget::eom; | ||
|
||
register_languages(); | ||
|
||
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -7,8 +7,6 @@ Author: Malte Mues <[email protected]> | |
|
||
\*******************************************************************/ | ||
|
||
#include <cstdlib> | ||
|
||
#include "analyze_symbol.h" | ||
|
||
#include <util/c_types.h> | ||
|
@@ -20,6 +18,9 @@ Author: Malte Mues <[email protected]> | |
#include <util/string_constant.h> | ||
#include <util/string_utils.h> | ||
|
||
#include <climits> | ||
#include <cstdlib> | ||
|
||
gdb_value_extractort::gdb_value_extractort( | ||
const symbol_tablet &symbol_table, | ||
const std::vector<std::string> &args) | ||
|
@@ -102,7 +103,7 @@ mp_integer gdb_value_extractort::get_type_size(const typet &type) const | |
{ | ||
const auto maybe_size = pointer_offset_bits(type, ns); | ||
CHECK_RETURN(maybe_size.has_value()); | ||
return *maybe_size / 8; | ||
return *maybe_size / CHAR_BIT; | ||
} | ||
|
||
void gdb_value_extractort::analyze_symbols(const std::vector<irep_idt> &symbols) | ||
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected] | |
|
||
#include "config.h" | ||
|
||
#include <climits> | ||
#include <cstdlib> | ||
|
||
#include "arith_tools.h" | ||
|
@@ -1010,42 +1011,43 @@ bool configt::set(const cmdlinet &cmdline) | |
if(arch==this_arch && os==this_os) | ||
{ | ||
INVARIANT( | ||
ansi_c.int_width == sizeof(int) * 8, | ||
ansi_c.int_width == sizeof(int) * CHAR_BIT, | ||
"int width shall be equal to the system int width"); | ||
INVARIANT( | ||
ansi_c.long_int_width == sizeof(long) * 8, | ||
ansi_c.long_int_width == sizeof(long) * CHAR_BIT, | ||
"long int width shall be equal to the system long int width"); | ||
INVARIANT( | ||
ansi_c.bool_width == sizeof(bool) * 8, | ||
ansi_c.bool_width == sizeof(bool) * CHAR_BIT, | ||
"bool width shall be equal to the system bool width"); | ||
INVARIANT( | ||
ansi_c.char_width == sizeof(char) * 8, | ||
ansi_c.char_width == sizeof(char) * CHAR_BIT, | ||
"char width shall be equal to the system char width"); | ||
INVARIANT( | ||
ansi_c.short_int_width == sizeof(short) * 8, | ||
ansi_c.short_int_width == sizeof(short) * CHAR_BIT, | ||
"short int width shall be equal to the system short int width"); | ||
INVARIANT( | ||
ansi_c.long_long_int_width == sizeof(long long) * 8, | ||
ansi_c.long_long_int_width == sizeof(long long) * CHAR_BIT, | ||
"long long int width shall be equal to the system long long int width"); | ||
INVARIANT( | ||
ansi_c.pointer_width == sizeof(void *) * 8, | ||
ansi_c.pointer_width == sizeof(void *) * CHAR_BIT, | ||
"pointer width shall be equal to the system pointer width"); | ||
INVARIANT( | ||
ansi_c.single_width == sizeof(float) * 8, | ||
ansi_c.single_width == sizeof(float) * CHAR_BIT, | ||
"float width shall be equal to the system float width"); | ||
INVARIANT( | ||
ansi_c.double_width == sizeof(double) * 8, | ||
ansi_c.double_width == sizeof(double) * CHAR_BIT, | ||
"double width shall be equal to the system double width"); | ||
INVARIANT( | ||
ansi_c.char_is_unsigned == (static_cast<char>(255) == 255), | ||
ansi_c.char_is_unsigned == | ||
(static_cast<char>((1 << CHAR_BIT) - 1) == (1 << CHAR_BIT) - 1), | ||
"char_is_unsigned flag shall indicate system char unsignedness"); | ||
|
||
#ifndef _WIN32 | ||
#ifndef _WIN32 | ||
// On Windows, long double width varies by compiler | ||
INVARIANT( | ||
ansi_c.long_double_width == sizeof(long double) * 8, | ||
ansi_c.long_double_width == sizeof(long double) * CHAR_BIT, | ||
"long double width shall be equal to the system long double width"); | ||
#endif | ||
#endif | ||
} | ||
|
||
// the following allows overriding the defaults | ||
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -35,6 +35,7 @@ Author: Michael Tautschnig, [email protected] | |
// MURMURHASH2A compares most favourably on String6 with 3076 fewer | ||
// calls (2.9%) | ||
|
||
#include <climits> | ||
#include <cstddef> // std::size_t | ||
|
||
#ifdef _MSC_VER | ||
|
@@ -117,10 +118,9 @@ inline std::size_t basic_hash_finalize( | |
|
||
// Boost uses the symbol hash_combine, if you're getting problems here then | ||
// you've probably included a Boost header after this one | ||
#define hash_combine(h1, h2) \ | ||
basic_hash_combine<sizeof(std::size_t)*8>(h1, h2) | ||
#define hash_finalize(h1, len) \ | ||
basic_hash_finalize(h1, len) | ||
# define hash_combine(h1, h2) \ | ||
basic_hash_combine<sizeof(std::size_t) * CHAR_BIT>(h1, h2) | ||
# define hash_finalize(h1, len) basic_hash_finalize(h1, len) | ||
|
||
#endif | ||
|
||
|
@@ -224,10 +224,10 @@ inline std::size_t murmurhash2a_hash_finalize<64>( | |
return h1; | ||
} | ||
|
||
#define hash_combine(h1, h2) \ | ||
murmurhash2a_hash_combine<sizeof(std::size_t)*8>(h1, h2) | ||
#define hash_finalize(h1, len) \ | ||
murmurhash2a_hash_finalize<sizeof(std::size_t)*8>(h1, len) | ||
# define hash_combine(h1, h2) \ | ||
murmurhash2a_hash_combine<sizeof(std::size_t) * CHAR_BIT>(h1, h2) | ||
# define hash_finalize(h1, len) \ | ||
murmurhash2a_hash_finalize<sizeof(std::size_t) * CHAR_BIT>(h1, len) | ||
|
||
#endif | ||
|
||
|
@@ -340,10 +340,10 @@ inline std::size_t murmurhash3_hash_finalize<64>( | |
return fmix64(h1); | ||
} | ||
|
||
#define hash_combine(h1, h2) \ | ||
murmurhash3_hash_combine<sizeof(std::size_t)*8>(h1, h2) | ||
#define hash_finalize(h1, len) \ | ||
murmurhash3_hash_finalize<sizeof(std::size_t)*8>(h1, len) | ||
# define hash_combine(h1, h2) \ | ||
murmurhash3_hash_combine<sizeof(std::size_t) * CHAR_BIT>(h1, h2) | ||
# define hash_finalize(h1, len) \ | ||
murmurhash3_hash_finalize<sizeof(std::size_t) * CHAR_BIT>(h1, len) | ||
|
||
#endif | ||
|
||
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected] | |
|
||
#include <algorithm> | ||
#include <cctype> | ||
#include <climits> | ||
#include <cstdlib> | ||
#include <limits> | ||
#include <ostream> | ||
|
@@ -122,7 +123,7 @@ const mp_integer binary2integer(const std::string &n, bool is_signed) | |
if(n.empty()) | ||
return 0; | ||
|
||
if(n.size()<=(sizeof(unsigned long)*8)) | ||
if(n.size() <= (sizeof(unsigned long) * CHAR_BIT)) | ||
{ | ||
// this is a tuned implementation for short integers | ||
|
||
|
@@ -264,10 +265,8 @@ mp_integer arith_left_shift( | |
ullong_t shift=b.to_ulong(); | ||
|
||
llong_t result=a.to_long()<<shift; | ||
llong_t mask= | ||
true_size<(sizeof(llong_t)*8) ? | ||
(1LL << true_size) - 1 : | ||
-1; | ||
llong_t mask = | ||
true_size < (sizeof(llong_t) * CHAR_BIT) ? (1LL << true_size) - 1 : -1; | ||
return result&mask; | ||
} | ||
|
||
|
@@ -303,7 +302,7 @@ mp_integer logic_left_shift( | |
|
||
ullong_t shift=b.to_ulong(); | ||
llong_t result=a.to_long()<<shift; | ||
if(true_size<(sizeof(llong_t)*8)) | ||
if(true_size < (sizeof(llong_t) * CHAR_BIT)) | ||
{ | ||
const llong_t sign = (1LL << (true_size - 1)) & result; | ||
const llong_t mask = (1LL << true_size) - 1; | ||
|
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Out-of-scope for this PR, but give how this exact log.status pattern is duplicated several times, it does rather feel like a utility function could be useful :-)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank you for highlighting this. Now PR'ed in #6089.