File tree 4 files changed +7
-3
lines changed
4 files changed +7
-3
lines changed Original file line number Diff line number Diff line change @@ -63,6 +63,8 @@ class goto_modelt
63
63
goto_functions=std::move (other.goto_functions );
64
64
return *this ;
65
65
}
66
+
67
+ void unload (const irep_idt &name) { goto_functions.unload (name); }
66
68
};
67
69
68
70
#endif // CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
Original file line number Diff line number Diff line change @@ -100,7 +100,7 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
100
100
throw 0 ;
101
101
}
102
102
103
- language_filet &lf=language_files. add_file (filename);
103
+ language_filet &lf=add_language_file (filename);
104
104
lf.language =get_language_from_filename (filename);
105
105
106
106
if (lf.language ==nullptr )
Original file line number Diff line number Diff line change @@ -71,6 +71,8 @@ class lazy_goto_modelt
71
71
// / Eagerly loads all functions from the symbol table.
72
72
void load_all_functions () const ;
73
73
74
+ void unload (const irep_idt &name) const { goto_functions.unload (name); }
75
+
74
76
language_filet &add_language_file (const std::string &filename)
75
77
{
76
78
return language_files.add_file (filename);
@@ -96,9 +98,9 @@ class lazy_goto_modelt
96
98
public:
97
99
// / Reference to symbol_table in the internal goto_model
98
100
symbol_tablet &symbol_table;
99
- const lazy_goto_functions_mapt<goto_programt> goto_functions;
100
101
101
102
private:
103
+ const lazy_goto_functions_mapt<goto_programt> goto_functions;
102
104
language_filest language_files;
103
105
104
106
// Function/module processing functions
Original file line number Diff line number Diff line change @@ -62,7 +62,7 @@ bool rebuild_goto_start_function_baset<goto_modelt>::operator()()
62
62
// Remove the function from the goto functions so it is copied back in
63
63
// from the symbol table during goto_convert
64
64
if (!return_code)
65
- goto_model.goto_functions . unload (goto_functionst::entry_point ());
65
+ goto_model.unload (goto_functionst::entry_point ());
66
66
67
67
return return_code;
68
68
}
You can’t perform that action at this time.
0 commit comments