Skip to content

Commit 2ac5414

Browse files
committed
Move link_goto_model to read_goto_binary.cpp
This is the only code that uses the functions from link_goto_model.{h,cpp}, and those functions weren't an easily usable API anyway as a certain protocol needs to be followed.
1 parent a75f6d0 commit 2ac5414

File tree

6 files changed

+195
-246
lines changed

6 files changed

+195
-246
lines changed

scripts/expected_doxygen_warnings.txt

+1-1
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@
8282
warning: Include graph for 'cbmc_parse_options.cpp' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8383
warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8484
warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
85-
warning: Included by graph for 'goto_model.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
85+
warning: Included by graph for 'goto_model.h' not generated, too many nodes (108), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8686
warning: Included by graph for 'arith_tools.h' not generated, too many nodes (183), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8787
warning: Included by graph for 'c_types.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8888
warning: Included by graph for 'config.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/goto-programs/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,6 @@ SRC = add_malloc_may_fail_variable_initializations.cpp \
3030
json_expr.cpp \
3131
json_goto_trace.cpp \
3232
label_function_pointer_call_sites.cpp \
33-
link_goto_model.cpp \
3433
link_to_library.cpp \
3534
loop_ids.cpp \
3635
mm_io.cpp \

src/goto-programs/README.md

-9
Original file line numberDiff line numberDiff line change
@@ -567,15 +567,6 @@ deserialises the passed file into a temporary `::goto_modelt` instance, and
567567
then it performs 'linking' of the temporary into a passed destination
568568
`::goto_modelt` instance.
569569

570-
Details about linking of `::goto_modelt` instances can be found
571-
[here](\ref section-linking-goto-models).
572-
573-
\section section-linking-goto-models Linking Goto Models
574-
575-
C++ modules:
576-
- `link_goto_model.h`
577-
- `link_goto_model.cpp`
578-
579570
Dependencies:
580571
- [linking folder](\ref linking).
581572
- [typecheck](\ref section-goto-typecheck).

src/goto-programs/link_goto_model.cpp

-205
This file was deleted.

src/goto-programs/link_goto_model.h

-29
This file was deleted.

0 commit comments

Comments
 (0)