Add missing Makefile, Readme and documentation

Author: NlightNFotis

CMakeLists.txt

@@ -158,6 +158,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
               "$<TARGET_FILE:goto-cc>"
               "$<TARGET_FILE:goto-diff>"
               "$<TARGET_FILE:goto-instrument>"
+              "$<TARGET_FILE:goto-inspect>"
               "$<TARGET_FILE:goto-synthesizer>"
               "$<TARGET_FILE:janalyzer>"
               "$<TARGET_FILE:jbmc>"

CODEOWNERS

@@ -53,6 +53,7 @@
 /src/goto-harness/ @martin-cs @chris-ryder @peterschrammel
 /src/goto-instrument/ @martin-cs @chris-ryder @peterschrammel @tautschnig @kroening
 /src/goto-instrument/contracts/ @tautschnig @feliperodri @remi-delmas-3000
+/src/goto-inspect/ @diffblue/diffblue-opensource
 /src/goto-synthesizer/ @qinheping @tautschnig @feliperodri @remi-delmas-3000
 /src/goto-diff/ @tautschnig @peterschrammel
 /src/jsil/ @kroening @tautschnig

doc/man/goto-inspect.1

@@ -0,0 +1,33 @@
+.TH GOTO-INSPECT "2" "May 2023" "goto-inspect-5.81.0" "User Commands"
+.SH NAME
+goto\-inspect \- Inspect goto-binaries.
+.SH SYNOPSIS
+.TP
+.B goto\-inspect [\-?] [\-h] [\-\-help]
+show help
+.TP
+.B goto\-inspect \-\-version
+show version and exit
+.TP
+.B goto\-inspect [options] \fIin\fR
+Inspect (show properties, goto-functions, etc of) given goto-binary.  
+.SH DESCRIPTION
+\fBgoto-inspect\fR reads a GOTO binary, and shows goto-functions, properties,
+and other attributes associated with the goto-program.
+.SH OPTIONS
+.SS "User-interface options:"
+.TP
+\fB\-\-show\-goto\-functions\fR
+print the goto-program instructions for the functions contained by the binary.
+.SH ENVIRONMENT
+All tools honor the TMPDIR environment variable when generating temporary
+files and directories.
+.SH BUGS
+If you encounter a problem please create an issue at
+.B https://github.com/diffblue/cbmc/issues
+.SH SEE ALSO
+.BR cbmc (1),
+.BR goto-cc (1)
+.BR goto-instrument (1)
+.SH COPYRIGHT
+2023, Fotis Koutoulakis

src/Makefile

@@ -10,6 +10,7 @@ DIRS = analyses \
        goto-cc \
        goto-checker \
        goto-diff \
+       goto-inspect \
        goto-instrument \
        goto-harness \
        goto-programs \
@@ -36,6 +37,7 @@ all: cbmc.dir \
      goto-cc.dir \
      goto-diff.dir \
      goto-instrument.dir \
+     goto-inspect.dir \
      goto-harness.dir \
      goto-synthesizer.dir \
      symtab2gb.dir \
@@ -82,6 +84,8 @@ goto-harness.dir: util.dir goto-programs.dir langapi.dir linking.dir \
 goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
                      goto-symex.dir linking.dir analyses.dir solvers.dir
 
+goto-inspect.dir: util.dir goto-programs.dir languages linking.dir
+
 goto-checker.dir: solvers.dir goto-symex.dir goto-programs.dir
 
 cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \
@@ -190,8 +194,8 @@ doc :
 install: all
 	for b in \
 		cbmc crangler \
-		goto-analyzer goto-cc goto-diff goto-instrument goto-harness goto-synthesizer \
-		symtab2gb ; do \
+		goto-analyzer goto-cc goto-diff goto-instrument goto-inspect goto-harness \
+    goto-synthesizer symtab2gb ; do \
 		  cp $$b/$$b $(PREFIX)/bin/ ; \
 			cp ../doc/man/$$b.1 $(PREFIX)/doc/man/man1/ ; \
 	done

src/goto-inspect/CMakeLists.txt

@@ -1,17 +1,22 @@
+# For goto-inspect, we are not building a library - only a binary.
+
 file(GLOB_RECURSE sources "*.cpp" "*.h")
+
 add_executable(goto-inspect ${sources})
+
 generic_includes(goto-inspect)
 
 target_link_libraries(goto-inspect
   util
   goto-programs
 )
+
 install(TARGETS goto-inspect DESTINATION ${CMAKE_INSTALL_BINDIR})
 
-# # Man page
-# if(NOT WIN32)
-#   install(
-#     DIRECTORY ${CMAKE_SOURCE_DIR}/doc/man/
-#     DESTINATION ${CMAKE_INSTALL_MANDIR}/man1
-#     FILES_MATCHING PATTERN "goto-harness*")
-# endif()
+# Man page
+if(NOT WIN32)
+  install(
+    DIRECTORY ${CMAKE_SOURCE_DIR}/doc/man/
+    DESTINATION ${CMAKE_INSTALL_MANDIR}/man1
+    FILES_MATCHING PATTERN "goto-harness*")
+endif()

src/goto-inspect/Makefile

@@ -0,0 +1,31 @@
+SRC = goto_inspect_main.cpp \
+      goto_inspect_parse_options.cpp \
+      # Empty last line
+
+OBJ += ../big-int/big-int$(LIBEXT) \
+       ../linking/linking$(LIBEXT) \
+       ../langapi/langapi$(LIBEXT) \
+       ../goto-programs/goto-programs$(LIBEXT) \
+       ../util/util$(LIBEXT) \
+       # Empty last line
+
+INCLUDES= -I ..
+
+LIBS =
+
+CLEANFILES = goto-inspect$(EXEEXT) goto-inspect$(LIBEXT)
+
+include ../config.inc
+include ../common
+
+all: goto-inspect$(EXEEXT)
+
+###############################################################################
+
+goto-inspect$(EXEEXT): $(OBJ)
+	$(LINKBIN)
+
+.PHONY: goto-inspect-mac-signed
+
+goto-inspect-mac-signed: goto-inspect$(EXEEXT)
+	codesign -v -s $(OSX_IDENTITY) goto-inspect$(EXEEXT)

src/goto-inspect/goto_inspect_main.cpp

@@ -1,8 +1,20 @@
 // Author: Fotis Koutoulakis for Diffblue Ltd.
 
+#ifdef _MSC_VER
+#  include <util/unicode.h>
+#endif
+
 #include "goto_inspect_parse_options.h"
 
-int main(int argc, const char *argv[])
+#ifdef _MSC_VER
+int wmain(int argc, const wchar_t **argv_wide)
+{
+  auto vec = narrow_argv(argc, argv_wide);
+  auto narrow = to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv = narrow.data();
+#else
+int main(int argc, const char **argv)
 {
+#endif
   return goto_inspect_parse_optionst{argc, argv}.main();
 }

src/goto-inspect/goto_inspect_parse_options.cpp

@@ -5,8 +5,6 @@
 #include <util/config.h>
 #include <util/exception_utils.h>
 #include <util/exit_codes.h>
-#include <util/invariant.h>
-#include <util/make_unique.h>
 #include <util/version.h>
 
 #include <goto-programs/goto_model.h>
@@ -36,7 +34,7 @@ int goto_inspect_parse_optionst::doit()
   // This just sets up the defaults (and would interpret options such as --32).
   config.set(cmdline);
 
-  // Normally we would register language front-ends here but as goto-harness
+  // Normally we would register language front-ends here but as goto-inspect
   // only works on goto binaries, we don't need to
 
   auto binary_filename = cmdline.args[0];

src/goto-inspect/goto_inspect_parse_options.h

@@ -1,12 +1,10 @@
 // Author: Fotis Koutoulakis for Diffblue Ltd.
 
-#ifndef CPROVER_GOTO_INSPECT_PARSE_OPTIONS_H
-#define CPROVER_GOTO_INSPECT_PARSE_OPTIONS_H
+#ifndef CPROVER_GOTO_INSPECT_GOTO_INSPECT_PARSE_OPTIONS_H
+#define CPROVER_GOTO_INSPECT_GOTO_INSPECT_PARSE_OPTIONS_H
 
 #include <util/parse_options.h>
 
-#include <string>
-
 // clang-format off
 #define GOTO_INSPECT_OPTIONS                                                   \
   "(version)"                                                                  \
@@ -23,4 +21,4 @@ struct goto_inspect_parse_optionst : public parse_options_baset
   goto_inspect_parse_optionst(int argc, const char *argv[]);
 };
 
-#endif // CPROVER_GOTO_INSPECT_PARSE_OPTIONS_H
+#endif // CPROVER_GOTO_INSPECT_GOTO_INSPECT_PARSE_OPTIONS_H

src/goto-inspect/module_dependencies.txt

@@ -0,0 +1,2 @@
+goto-programs
+util

src/goto-inspect/readme.md

@@ -0,0 +1,10 @@
+\ingroup module_hidden
+\defgroup goto-synthesizer goto-synthesizer
+
+# Folder goto-inspect
+
+\author Fotis Koutoulakis
+
+The `goto-inspect/` contains the code for the binary `goto-inspect`, intended
+to provide an all-purpose tool for inspection of goto-binaries (properties,
+goto-functions, etc).