Skip to content

Commit 0f0ab68

Browse files
committed
progress output
1 parent 775bbef commit 0f0ab68

File tree

3 files changed

+44
-0
lines changed

3 files changed

+44
-0
lines changed
Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
2+
int x;
3+
4+
void h()
5+
{
6+
x = 1;
7+
}
8+
9+
void g()
10+
{
11+
h();
12+
}
13+
14+
void f()
15+
{
16+
g();
17+
}
18+
19+
int main()
20+
{
21+
f();
22+
}
23+
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--function-inline main --log - --no-caching --verbosity 9
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

src/goto-programs/goto_inline_class.cpp

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -683,8 +683,16 @@ void goto_inlinet::expand_function_call(
683683
arguments,
684684
constrain);
685685

686+
progress() << "Inserting " << identifier << " into caller" << eom;
687+
progress() << "Number of instructions: "
688+
<< cached.body.instructions.size() << eom;
689+
686690
if(!caching)
687691
{
692+
progress() << "Removing " << identifier << " from cache" << eom;
693+
progress() << "Number of instructions: "
694+
<< cached.body.instructions.size() << eom;
695+
688696
inline_log.cleanup(cached.body);
689697
cache.erase(identifier);
690698
}
@@ -950,6 +958,11 @@ const goto_inlinet::goto_functiont &goto_inlinet::goto_inline_transitive(
950958

951959
goto_functiont &cached=cache[identifier];
952960
assert(cached.body.empty());
961+
962+
progress() << "Creating copy of " << identifier << eom;
963+
progress() << "Number of instructions: "
964+
<< goto_function.body.instructions.size() << eom;
965+
953966
cached.copy_from(goto_function); // location numbers not changed
954967
inline_log.copy_from(goto_function.body, cached.body);
955968

0 commit comments

Comments
 (0)