replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

static initialization must do framework variables first 

This ensures, among others, that the rounding mode is set before any
initializers are evaluated.

Fixes #3708.
This commit is contained in:
Daniel Kroening 2019-01-08 23:44:33 +00:00
parent b93a666813
commit 958a61f6dc
2 changed files with 18 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
regression/cbmc/Float-rounding/compile_time_rounding.desc
View File

@ -1,4 +1,4 @@
KNOWNBUG CORE
compile_time_rounding.c compile_time_rounding.c
^EXIT=0$ ^EXIT=0$

23
src/linking/static_lifetime_init.cpp
View File

@ -127,14 +127,25 @@ void static_lifetime_init(
symbols.insert(id2string(symbol_pair.first)); symbols.insert(id2string(symbol_pair.first));
} }
// first do framework variables
for(const std::string &id : symbols) for(const std::string &id : symbols)
{ if(has_prefix(id, CPROVER_PREFIX))
auto code = static_lifetime_init(id, symbol_table); {
if(code.has_value()) auto code = static_lifetime_init(id, symbol_table);
dest.add(std::move(*code)); if(code.has_value())
} dest.add(std::move(*code));
}
// call designated "initialization" functions // now all other variables
for(const std::string &id : symbols)
if(!has_prefix(id, CPROVER_PREFIX))
{
auto code = static_lifetime_init(id, symbol_table);
if(code.has_value())
dest.add(std::move(*code));
}
// now call designated "initialization" functions
for(const std::string &id : symbols) for(const std::string &id : symbols)
{ {