File tree Expand file tree Collapse file tree 7 files changed +88
-0
lines changed Expand file tree Collapse file tree 7 files changed +88
-0
lines changed Original file line number Diff line number Diff line change @@ -61,6 +61,7 @@ add_subdirectory(linking-goto-binaries)
61
61
add_subdirectory (symtab2gb )
62
62
add_subdirectory (validate-trace-xml-schema )
63
63
add_subdirectory (cbmc-primitives )
64
+ add_subdirectory (goto-interpreter )
64
65
add_subdirectory (cbmc-sequentialization )
65
66
66
67
if (WITH_MEMORY_ANALYZER )
Original file line number Diff line number Diff line change @@ -35,6 +35,7 @@ DIRS = cbmc \
35
35
goto-ld \
36
36
validate-trace-xml-schema \
37
37
cbmc-primitives \
38
+ goto-interpreter \
38
39
# Empty last line
39
40
40
41
ifeq ($(OS ) ,Windows_NT)
Original file line number Diff line number Diff line change
1
+ if (WIN32 )
2
+ set (is_windows true )
3
+ else ()
4
+ set (is_windows false )
5
+ endif ()
6
+
7
+ add_test_pl_tests (
8
+ "${CMAKE_CURRENT_SOURCE_DIR} /chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> ${is_windows} "
9
+ )
Original file line number Diff line number Diff line change
1
+ default : tests.log
2
+
3
+ include ../../src/config.inc
4
+ include ../../src/common
5
+
6
+ ifeq ($(BUILD_ENV_ ) ,MSVC)
7
+ exe=../../../src/goto-cc/goto-cl
8
+ is_windows=true
9
+ else
10
+ exe=../../../src/goto-cc/goto-cc
11
+ is_windows=false
12
+ endif
13
+
14
+ test :
15
+ @../test.pl -e -p -c ' ../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)'
16
+
17
+ tests.log :
18
+ @../test.pl -e -p -c ' ../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)'
19
+
20
+ show :
21
+ @for dir in * ; do \
22
+ if [ -d " $$ dir" ]; then \
23
+ vim -o " $$ dir/*.c" " $$ dir/*.out" ; \
24
+ fi ; \
25
+ done ;
26
+
27
+ clean :
28
+ @for dir in * ; do \
29
+ $(RM ) tests.log; \
30
+ if [ -d " $$ dir" ]; then \
31
+ cd " $$ dir" ; \
32
+ $(RM ) * .out * .gb; \
33
+ cd ..; \
34
+ fi \
35
+ done
Original file line number Diff line number Diff line change
1
+ #! /usr/bin/env bash
2
+
3
+ set -e
4
+
5
+ goto_cc=$1
6
+ goto_instrument=$2
7
+ is_windows=$3
8
+
9
+ options=${*: 4: $# -4}
10
+ name=${*: $# }
11
+ base_name=${name% .c}
12
+
13
+ if [[ " ${is_windows} " == " true" ]]; then
14
+ " ${goto_cc} " " ${name} "
15
+ mv " ${base_name} .exe" " ${base_name} .gb"
16
+ else
17
+ " ${goto_cc} " " ${name} " -o " ${base_name} .gb"
18
+ fi
19
+
20
+ echo ${options} | tr , ' \n' | " ${goto_instrument} " --interpreter " ${base_name} .gb"
Original file line number Diff line number Diff line change
1
+ int main (int argc , char * * argv )
2
+ {
3
+ return 0 ;
4
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ main.c
3
+ h,q
4
+ ^Starting interpreter$
5
+ ^Interpreter help$
6
+ ^h: display this menu$
7
+ ^j: output json trace$
8
+ ^m: output memory dump$
9
+ ^o: output goto trace$
10
+ ^q: quit$
11
+ ^r: run until completion$
12
+ ^s#: step a number of instructions$
13
+ ^sa: step across a function$
14
+ ^so: step out of a function$
15
+ ^\d+- Program End\.$
16
+ ^EXIT=0$
17
+ ^SIGNAL=0$
18
+ --
You can’t perform that action at this time.
0 commit comments