File tree 2 files changed +18
-7
lines changed
regression/cbmc/Float-rounding 2 files changed +18
-7
lines changed Original file line number Diff line number Diff line change 1
- KNOWNBUG
1
+ CORE
2
2
compile_time_rounding.c
3
3
4
4
^EXIT=0$
Original file line number Diff line number Diff line change @@ -127,14 +127,25 @@ void static_lifetime_init(
127
127
symbols.insert (id2string (symbol_pair.first ));
128
128
}
129
129
130
+ // first do framework variables
130
131
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
+ }
136
147
137
- // call designated "initialization" functions
148
+ // now call designated "initialization" functions
138
149
139
150
for (const std::string &id : symbols)
140
151
{
You can’t perform that action at this time.
0 commit comments