Skip to content

Commit d13f1da

Browse files
author
Daniel Kroening
committed
static initialization must do framework variables first
This ensures, among others, that the rounding mode is set before any initializers are evaluated. Fixes #3708.
1 parent b93a666 commit d13f1da

File tree

2 files changed

+18
-7
lines changed

2 files changed

+18
-7
lines changed

regression/cbmc/Float-rounding/compile_time_rounding.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
compile_time_rounding.c
33

44
^EXIT=0$

src/linking/static_lifetime_init.cpp

Lines changed: 17 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -127,14 +127,25 @@ void static_lifetime_init(
127127
symbols.insert(id2string(symbol_pair.first));
128128
}
129129

130+
// first do framework variables
130131
for(const std::string &id : symbols)
131-
{
132-
auto code = static_lifetime_init(id, symbol_table);
133-
if(code.has_value())
134-
dest.add(std::move(*code));
135-
}
132+
if(has_prefix(id2string(id), CPROVER_PREFIX))
133+
{
134+
auto code = static_lifetime_init(id, symbol_table);
135+
if(code.has_value())
136+
dest.add(std::move(*code));
137+
}
138+
139+
// now all other variables
140+
for(const std::string &id : symbols)
141+
if(!has_prefix(id2string(id), CPROVER_PREFIX))
142+
{
143+
auto code = static_lifetime_init(id, symbol_table);
144+
if(code.has_value())
145+
dest.add(std::move(*code));
146+
}
136147

137-
// call designated "initialization" functions
148+
// now call designated "initialization" functions
138149

139150
for(const std::string &id : symbols)
140151
{

0 commit comments

Comments
 (0)