Skip to content

Commit a59768d

Browse files
committed
Add loop-contract symbols into symbol table during typecheck
1 parent 582aa69 commit a59768d

File tree

3 files changed

+178
-71
lines changed

3 files changed

+178
-71
lines changed

src/linking/remove_internal_symbols.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,10 @@ Author: Daniel Kroening
2323

2424
#include "static_lifetime_init.h"
2525

26+
static std::unordered_set<irep_idt> loop_contracts_subs{
27+
ID_C_spec_loop_invariant,
28+
ID_C_spec_decreases};
29+
2630
static void get_symbols(
2731
const namespacet &ns,
2832
const symbolt &in_symbol,
@@ -43,8 +47,8 @@ static void get_symbols(
4347

4448
find_symbols_sett new_symbols;
4549

46-
find_type_and_expr_symbols(symbol.type, new_symbols);
47-
find_type_and_expr_symbols(symbol.value, new_symbols);
50+
find_type_and_expr_symbols(symbol.type, new_symbols, loop_contracts_subs);
51+
find_type_and_expr_symbols(symbol.value, new_symbols, loop_contracts_subs);
4852

4953
for(const auto &s : new_symbols)
5054
working_set.push_back(&ns.lookup(s));

0 commit comments

Comments
 (0)