Skip to content

Commit 8645b9d

Browse files
committed
goto-program interpreter: test and fix 'r' command
Fix basic execution as sparse vectors do not (yet) support resizing to smaller sizes (performing a clear+resize instead).
1 parent 18700e0 commit 8645b9d

File tree

4 files changed

+21
-0
lines changed

4 files changed

+21
-0
lines changed
Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
int main()
2+
{
3+
int x;
4+
__CPROVER_assert(x == 42, "should fail");
5+
return 0;
6+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
r,q
4+
^Starting interpreter$
5+
^\d+- Program End\.$
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--

src/goto-programs/interpreter.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -858,6 +858,7 @@ void interpretert::execute_function_call()
858858
void interpretert::build_memory_map()
859859
{
860860
// put in a dummy for NULL
861+
memory.clear();
861862
memory.resize(1);
862863
inverse_memory_map[0] = {};
863864

src/util/sparse_vector.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,12 @@ template<class T> class sparse_vectort
5151
_size=new_size;
5252
}
5353

54+
void clear()
55+
{
56+
underlying.clear();
57+
_size = 0;
58+
}
59+
5460
typedef typename underlyingt::iterator iteratort;
5561
typedef typename underlyingt::const_iterator const_iteratort;
5662

0 commit comments

Comments
 (0)