File tree Expand file tree Collapse file tree 8 files changed +107
-0
lines changed
goto-harness-multi-file-project Expand file tree Collapse file tree 8 files changed +107
-0
lines changed Original file line number Diff line number Diff line change @@ -52,6 +52,7 @@ add_subdirectory(statement-list)
52
52
add_subdirectory (systemc )
53
53
add_subdirectory (contracts )
54
54
add_subdirectory (goto-harness )
55
+ add_subdirectory (goto-harness-multi-file-project )
55
56
add_subdirectory (goto-cc-file-local )
56
57
add_subdirectory (linking-goto-binaries )
57
58
add_subdirectory (symtab2gb )
Original file line number Diff line number Diff line change
1
+ add_test_pl_tests (
2
+ "${CMAKE_CURRENT_LIST_DIR} /chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-harness> $<TARGET_FILE:cbmc>" )
Original file line number Diff line number Diff line change
1
+ default : test
2
+
3
+ test :
4
+ @../test.pl -e -p -c " ../chain.sh \
5
+ ../../../src/goto-cc/goto-cc \
6
+ ../../../src/goto-harness/goto-harness \
7
+ ../../../src/cbmc/cbmc"
8
+ clean :
9
+ find -name ' *.out' -execdir $(RM ) ' {}' \;
10
+ $(RM ) tests.log
Original file line number Diff line number Diff line change
1
+ #! /bin/bash
2
+
3
+ set -x
4
+ set -e
5
+ goto_cc=" $1 "
6
+ goto_harness=" $2 "
7
+ cbmc=" $3 "
8
+ goto_harness_args=" ${@: 4: $# -4} "
9
+
10
+ source_dir=" $( pwd) "
11
+ target_dir=" $( mktemp -d) "
12
+
13
+ # Compiling
14
+ for file in " $source_dir " /* .c; do
15
+ file_name=" $( basename " $file " ) "
16
+ " $goto_cc " -c " $file " -o " $target_dir " /" ${file_name% .c} .o"
17
+ done
18
+
19
+ # Linking
20
+
21
+ main_exe=" $target_dir /main.gb"
22
+ " $goto_cc " " $target_dir " /* .o -o " $main_exe "
23
+
24
+ harness_out_file=" $target_dir /harness.c"
25
+ " $goto_harness " " $main_exe " " $harness_out_file " --harness-function-name harness $goto_harness_args
26
+ cat " $harness_out_file "
27
+ " $cbmc " " $main_exe " " $harness_out_file " --function harness
28
+
Original file line number Diff line number Diff line change
1
+ #include "service.h"
2
+
3
+ // this isn't testing any interesting harness
4
+ // properties so we just have a main function
5
+ // with no parameters
6
+ int main (void )
7
+ {
8
+ service_t * service = get_default_service ();
9
+ service_serve (service );
10
+ }
Original file line number Diff line number Diff line change
1
+ #include "service.h"
2
+ #include <assert.h>
3
+
4
+ // contents of the struct
5
+ // (mostly just a vtable)
6
+
7
+ struct service
8
+ {
9
+ void (* serve )(void );
10
+ };
11
+
12
+ void service_serve (service_t * service )
13
+ {
14
+ service -> serve ();
15
+ }
16
+
17
+ static void default_serve (void )
18
+ {
19
+ assert (0 && "default serve should fail so we can see it is being called" );
20
+ }
21
+
22
+ // this static initialisation should not show up in output
23
+ // in fact, there is a bit of a bug with dump-c where this
24
+ // initialisation would appear but the default_serve function
25
+ // would be omitted in certain cases.
26
+ static service_t default_service = {.serve = default_serve };
27
+
28
+ service_t * get_default_service (void )
29
+ {
30
+ return & default_service ;
31
+ }
Original file line number Diff line number Diff line change
1
+ #include <stddef.h>
2
+
3
+ // common pattern:
4
+ // Some sort of interface defined over "abstract" type with hidden
5
+ // implementation details, effectively C style OOP
6
+ //
7
+ // This is a straw example of course, but very reminiscent of patterns that
8
+ // occur in real programs
9
+
10
+ typedef struct service service_t ;
11
+
12
+ service_t * get_default_service (void );
13
+ void service_serve (service_t * service );
Original file line number Diff line number Diff line change
1
+ CORE
2
+ dummy.c
3
+ --function main --harness-type call-function
4
+ \[default_serve\.assertion\.1\] line \d+ assertion 0 && \"default serve should fail so we can see it is being called\": FAILURE
5
+ ^EXIT=10$
6
+ ^SIGNAL=0$
7
+ --
8
+ static void default_serve
9
+ --
10
+ When running the harness we should run into the assertion failure from the
11
+ static default_serve function, but the harness C code should not contain this
12
+ or any other static functions or variables.
You can’t perform that action at this time.
0 commit comments