Skip to content

Commit bcb3821

Browse files
tautschnigtautschnig
authored
Merge pull request #5962 from tautschnig/char_bit
Do not assume that build architecture has byte/char==8 bits
2 parents 0f16836 + 74978c0 commit bcb3821

File tree

13 files changed

+74
-56
lines changed

13 files changed

+74
-56
lines changed

‎jbmc/src/janalyzer/janalyzer_parse_options.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "janalyzer_parse_options.h"
1313

14+
#include <climits>
1415
#include <cstdlib> // exit()
1516
#include <fstream>
1617
#include <iostream>
@@ -357,8 +358,9 @@ int janalyzer_parse_optionst::doit()
357358
// Print a banner
358359
//
359360
log.status() << "JANALYZER version " << CBMC_VERSION << " "
360-
<< sizeof(void *) * 8 << "-bit " << config.this_architecture()
361-
<< " " << config.this_operating_system() << messaget::eom;
361+
<< sizeof(void *) * CHAR_BIT << "-bit "
362+
<< config.this_architecture() << " "
363+
<< config.this_operating_system() << messaget::eom;
362364

363365
register_languages();
364366

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,9 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "jbmc_parse_options.h"
1313

14-
#include <fstream>
14+
#include <climits>
1515
#include <cstdlib> // exit()
16+
#include <fstream>
1617
#include <iostream>
1718
#include <memory>
1819

@@ -484,8 +485,9 @@ int jbmc_parse_optionst::doit()
484485
//
485486
// Print a banner
486487
//
487-
log.status() << "JBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8
488-
<< "-bit " << config.this_architecture() << " "
488+
log.status() << "JBMC version " << CBMC_VERSION << " "
489+
<< sizeof(void *) * CHAR_BIT << "-bit "
490+
<< config.this_architecture() << " "
489491
<< config.this_operating_system() << messaget::eom;
490492

491493
// output the options

‎jbmc/src/jdiff/jdiff_parse_options.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Peter Schrammel
1111

1212
#include "jdiff_parse_options.h"
1313

14+
#include <climits>
1415
#include <cstdlib> // exit()
1516
#include <fstream>
1617
#include <iostream>
@@ -194,8 +195,9 @@ int jdiff_parse_optionst::doit()
194195
//
195196
// Print a banner
196197
//
197-
log.status() << "JDIFF version " << CBMC_VERSION << " " << sizeof(void *) * 8
198-
<< "-bit " << config.this_architecture() << " "
198+
log.status() << "JDIFF version " << CBMC_VERSION << " "
199+
<< sizeof(void *) * CHAR_BIT << "-bit "
200+
<< config.this_architecture() << " "
199201
<< config.this_operating_system() << messaget::eom;
200202

201203
if(cmdline.args.size() != 2)

‎src/ansi-c/literals/convert_character_literal.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "convert_character_literal.h"
1313

14+
#include <climits>
15+
1416
#include <util/arith_tools.h>
1517
#include <util/c_types.h>
1618
#include <util/std_expr.h>
@@ -51,7 +53,7 @@ exprt convert_character_literal(
5153
for(unsigned i=0; i<value.size(); i++)
5254
{
5355
mp_integer z=(unsigned char)(value[i]);
54-
z=z<<((value.size()-i-1)*8);
56+
z = z << ((value.size() - i - 1) * CHAR_BIT);
5557
x+=z;
5658
}
5759

@@ -84,7 +86,7 @@ exprt convert_character_literal(
8486
for(unsigned i=0; i<value.size(); i++)
8587
{
8688
mp_integer z=(unsigned char)(value[i]);
87-
z=z<<((value.size()-i-1)*8);
89+
z = z << ((value.size() - i - 1) * CHAR_BIT);
8890
x+=z;
8991
}
9092

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,9 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "cbmc_parse_options.h"
1313

14-
#include <fstream>
14+
#include <climits>
1515
#include <cstdlib> // exit()
16+
#include <fstream>
1617
#include <iostream>
1718
#include <memory>
1819

@@ -519,8 +520,9 @@ int cbmc_parse_optionst::doit()
519520
//
520521
// Print a banner
521522
//
522-
log.status() << "CBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8
523-
<< "-bit " << config.this_architecture() << " "
523+
log.status() << "CBMC version " << CBMC_VERSION << " "
524+
<< sizeof(void *) * CHAR_BIT << "-bit "
525+
<< config.this_architecture() << " "
524526
<< config.this_operating_system() << messaget::eom;
525527

526528
//

‎src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,10 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "goto_analyzer_parse_options.h"
1313

14+
#include <climits>
1415
#include <cstdlib> // exit()
15-
#include <iostream>
1616
#include <fstream>
17+
#include <iostream>
1718
#include <memory>
1819

1920
#include <ansi-c/ansi_c_language.h>
@@ -402,8 +403,9 @@ int goto_analyzer_parse_optionst::doit()
402403
// Print a banner
403404
//
404405
log.status() << "GOTO-ANALYSER version " << CBMC_VERSION << " "
405-
<< sizeof(void *) * 8 << "-bit " << config.this_architecture()
406-
<< " " << config.this_operating_system() << messaget::eom;
406+
<< sizeof(void *) * CHAR_BIT << "-bit "
407+
<< config.this_architecture() << " "
408+
<< config.this_operating_system() << messaget::eom;
407409

408410
register_languages();
409411

‎src/goto-cc/ms_cl_cmdline.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,10 +11,11 @@ Author: Daniel Kroening
1111

1212
#include "ms_cl_cmdline.h"
1313

14-
#include <cstring>
14+
#include <climits>
1515
#include <cstdlib>
16-
#include <iostream>
16+
#include <cstring>
1717
#include <fstream>
18+
#include <iostream>
1819

1920
#include <util/unicode.h>
2021

@@ -165,7 +166,7 @@ static std::istream &my_wgetline(std::istream &in, std::wstring &dest)
165166
break; // line end
166167
}
167168
else
168-
dest+=wchar_t(ch1+(ch2<<8));
169+
dest += wchar_t(ch1 + (ch2 << CHAR_BIT));
169170
}
170171

171172
return in;

‎src/goto-diff/goto_diff_parse_options.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Peter Schrammel
1111

1212
#include "goto_diff_parse_options.h"
1313

14+
#include <climits>
1415
#include <cstdlib> // exit()
1516
#include <fstream>
1617
#include <iostream>
@@ -162,8 +163,9 @@ int goto_diff_parse_optionst::doit()
162163
// Print a banner
163164
//
164165
log.status() << "GOTO-DIFF version " << CBMC_VERSION << " "
165-
<< sizeof(void *) * 8 << "-bit " << config.this_architecture()
166-
<< " " << config.this_operating_system() << messaget::eom;
166+
<< sizeof(void *) * CHAR_BIT << "-bit "
167+
<< config.this_architecture() << " "
168+
<< config.this_operating_system() << messaget::eom;
167169

168170
if(cmdline.args.size()!=2)
169171
{

‎src/memory-analyzer/analyze_symbol.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,6 @@ Author: Malte Mues <[email protected]>
77
88
\*******************************************************************/
99

10-
#include <cstdlib>
11-
1210
#include "analyze_symbol.h"
1311

1412
#include <util/c_types.h>
@@ -20,6 +18,9 @@ Author: Malte Mues <[email protected]>
2018
#include <util/string_constant.h>
2119
#include <util/string_utils.h>
2220

21+
#include <climits>
22+
#include <cstdlib>
23+
2324
gdb_value_extractort::gdb_value_extractort(
2425
const symbol_tablet &symbol_table,
2526
const std::vector<std::string> &args)
@@ -102,7 +103,7 @@ mp_integer gdb_value_extractort::get_type_size(const typet &type) const
102103
{
103104
const auto maybe_size = pointer_offset_bits(type, ns);
104105
CHECK_RETURN(maybe_size.has_value());
105-
return *maybe_size / 8;
106+
return *maybe_size / CHAR_BIT;
106107
}
107108

108109
void gdb_value_extractort::analyze_symbols(const std::vector<irep_idt> &symbols)

‎src/util/config.cpp

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
88

99
#include "config.h"
1010

11+
#include <climits>
1112
#include <cstdlib>
1213

1314
#include "arith_tools.h"
@@ -1010,42 +1011,43 @@ bool configt::set(const cmdlinet &cmdline)
10101011
if(arch==this_arch && os==this_os)
10111012
{
10121013
INVARIANT(
1013-
ansi_c.int_width == sizeof(int) * 8,
1014+
ansi_c.int_width == sizeof(int) * CHAR_BIT,
10141015
"int width shall be equal to the system int width");
10151016
INVARIANT(
1016-
ansi_c.long_int_width == sizeof(long) * 8,
1017+
ansi_c.long_int_width == sizeof(long) * CHAR_BIT,
10171018
"long int width shall be equal to the system long int width");
10181019
INVARIANT(
1019-
ansi_c.bool_width == sizeof(bool) * 8,
1020+
ansi_c.bool_width == sizeof(bool) * CHAR_BIT,
10201021
"bool width shall be equal to the system bool width");
10211022
INVARIANT(
1022-
ansi_c.char_width == sizeof(char) * 8,
1023+
ansi_c.char_width == sizeof(char) * CHAR_BIT,
10231024
"char width shall be equal to the system char width");
10241025
INVARIANT(
1025-
ansi_c.short_int_width == sizeof(short) * 8,
1026+
ansi_c.short_int_width == sizeof(short) * CHAR_BIT,
10261027
"short int width shall be equal to the system short int width");
10271028
INVARIANT(
1028-
ansi_c.long_long_int_width == sizeof(long long) * 8,
1029+
ansi_c.long_long_int_width == sizeof(long long) * CHAR_BIT,
10291030
"long long int width shall be equal to the system long long int width");
10301031
INVARIANT(
1031-
ansi_c.pointer_width == sizeof(void *) * 8,
1032+
ansi_c.pointer_width == sizeof(void *) * CHAR_BIT,
10321033
"pointer width shall be equal to the system pointer width");
10331034
INVARIANT(
1034-
ansi_c.single_width == sizeof(float) * 8,
1035+
ansi_c.single_width == sizeof(float) * CHAR_BIT,
10351036
"float width shall be equal to the system float width");
10361037
INVARIANT(
1037-
ansi_c.double_width == sizeof(double) * 8,
1038+
ansi_c.double_width == sizeof(double) * CHAR_BIT,
10381039
"double width shall be equal to the system double width");
10391040
INVARIANT(
1040-
ansi_c.char_is_unsigned == (static_cast<char>(255) == 255),
1041+
ansi_c.char_is_unsigned ==
1042+
(static_cast<char>((1 << CHAR_BIT) - 1) == (1 << CHAR_BIT) - 1),
10411043
"char_is_unsigned flag shall indicate system char unsignedness");
10421044

1043-
#ifndef _WIN32
1045+
#ifndef _WIN32
10441046
// On Windows, long double width varies by compiler
10451047
INVARIANT(
1046-
ansi_c.long_double_width == sizeof(long double) * 8,
1048+
ansi_c.long_double_width == sizeof(long double) * CHAR_BIT,
10471049
"long double width shall be equal to the system long double width");
1048-
#endif
1050+
#endif
10491051
}
10501052

10511053
// the following allows overriding the defaults

0 commit comments

Comments
 (0)