Skip to content

Commit 9edf8f8

Browse files
committed
goto-program interpreter: output memory map at lower verbosity
The memory map is (only) printed upon a user's request (using the "m" command). It should not be necessary to raise verbosity to debug level to see this output.
1 parent 8645b9d commit 9edf8f8

File tree

3 files changed

+17
-5
lines changed

3 files changed

+17
-5
lines changed
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
int main()
2+
{
3+
return 0;
4+
}
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
s1,so,m
4+
^Starting interpreter$
5+
^__CPROVER_rounding_mode\[0\]=0$
6+
^\d+- Program End\.$
7+
^EXIT=0$
8+
^SIGNAL=0$
9+
--

src/goto-programs/interpreter.cpp

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1070,12 +1070,11 @@ void interpretert::print_memory(bool input_flags)
10701070
const memory_cellt &cell=cell_address.second;
10711071
const auto identifier = address_to_symbol(i).get_identifier();
10721072
const auto offset=address_to_offset(i);
1073-
debug() << identifier << "[" << offset << "]"
1074-
<< "=" << cell.value << eom;
1073+
status() << identifier << "[" << offset << "]"
1074+
<< "=" << cell.value << eom;
10751075
if(input_flags)
1076-
debug() << "(" << static_cast<int>(cell.initialized) << ")"
1077-
<< eom;
1078-
debug() << eom;
1076+
status() << "(" << static_cast<int>(cell.initialized) << ")" << eom;
1077+
status() << eom;
10791078
}
10801079
}
10811080

0 commit comments

Comments
 (0)