Skip to content

add git shortened sha1sum to CBMC version for unique id #668

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 6 commits into from
Closed

add git shortened sha1sum to CBMC version for unique id #668

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
556f322
Print git revision with all --version outputs
tautschnig May 31, 2016
ff9024b
use git-describe for version UID creation
Mar 23, 2017
70d919d
windowsify compiler options
Mar 23, 2017
159bd83
Build .release_info files containing the version string
tautschnig Mar 24, 2017
f7be1c4
RELEASE_INFO -> GIT_INFO
Mar 24, 2017
4df4a36
add centered git version to CBMC banner
May 10, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ src/goto-analyzer/taint_driver_scripts/.idea/*
*.obj
*.a
*.lib
.release_info
src/ansi-c/arm_builtin_headers.inc
src/ansi-c/clang_builtin_headers.inc
src/ansi-c/cprover_library.inc
Expand Down
8 changes: 8 additions & 0 deletions src/cbmc/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,14 @@ CLEANFILES = cbmc$(EXEEXT)

all: cbmc$(EXEEXT)

ifeq ($(BUILD_ENV_),MSVC)
CP_CXXFLAGS += /DCBMC_TAG_VERSION='"""$(CBMC_VERSION)"""' \
/DCBMC_VERSION='"""($(GIT_INFO))"""'
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this different from https://github.com/diffblue/cbmc/pull/668/files#diff-d9c95ec27fc25a0481354de531adad56R34?

else
CP_CXXFLAGS += -DCBMC_TAG_VERSION="\"$(CBMC_VERSION)\"" \
-DCBMC_VERSION="\"($(GIT_INFO))\""
endif

ifneq ($(wildcard ../bv_refinement/Makefile),)
OBJ += ../bv_refinement/bv_refinement$(LIBEXT)
CP_CXXFLAGS += -DHAVE_BV_REFINEMENT
Expand Down
4 changes: 2 additions & 2 deletions src/cbmc/cbmc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,6 @@ Author: Daniel Kroening, [email protected]
#include "cbmc_solvers.h"
#include "cbmc_parse_options.h"
#include "bmc.h"
#include "version.h"
#include "xml_interface.h"

/*******************************************************************\
Expand Down Expand Up @@ -1045,13 +1044,14 @@ void cbmc_parse_optionst::help()
{
std::cout <<
"\n"
"* * CBMC " CBMC_VERSION " - Copyright (C) 2001-2016 ";
"* * CBMC " CBMC_TAG_VERSION " - Copyright (C) 2001-2016 ";

std::cout << "(" << (sizeof(void *)*8) << "-bit version)";

std::cout << " * *\n";

std::cout <<
"* * " CBMC_VERSION " * * \n"
"* * Daniel Kroening, Edmund Clarke * *\n"
"* * Carnegie Mellon University, Computer Science Department * *\n"
"* * [email protected] * *\n"
Expand Down
1 change: 0 additions & 1 deletion src/cbmc/cbmc_solvers.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,6 @@ Author: Daniel Kroening, [email protected]
#include "bv_cbmc.h"
#include "cbmc_dimacs.h"
#include "counterexample_beautification.h"
#include "version.h"

/*******************************************************************\

Expand Down
6 changes: 0 additions & 6 deletions src/cbmc/version.h
View file
Open in desktop

This file was deleted.

6 changes: 6 additions & 0 deletions src/clobber/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,12 @@ CLEANFILES = clobber$(EXEEXT)

all: clobber$(EXEEXT)

ifeq ($(BUILD_ENV_),MSVC)
CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
else
CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
endif

ifneq ($(wildcard ../bv_refinement/Makefile),)
OBJ += ../bv_refinement/bv_refinement$(LIBEXT)
CP_CXXFLAGS += -DHAVE_BV_REFINEMENT
Expand Down
2 changes: 0 additions & 2 deletions src/clobber/clobber_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,6 @@ Author: Daniel Kroening, [email protected]

#include <langapi/mode.h>

#include <cbmc/version.h>

#include "clobber_parse_options.h"
// #include "clobber_instrumenter.h"

Expand Down
18 changes: 16 additions & 2 deletions src/common
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
# get version from git
GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a")

# Build platform
# (use one of AUTO, Unix, OSX, OSX_Universal, MSVC, Cygwin, MinGW)

Expand Down Expand Up @@ -182,12 +185,24 @@ OBJ += $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC)))
%.obj:%.c
$(CC) $(CP_CFLAGS) /nologo /c /EHsc $< /Fo$@

# make >= 4.0 has a `file` function that may be faster than `shell cat`
# for now, portability wins
KNOWN_RELEASE_INFO = $(shell cat .release_info 2>/dev/null)
ifneq ($(GIT_INFO), $(KNOWN_RELEASE_INFO))
$(filter %_parse_options$(OBJEXT), $(OBJ)): .release_info

.release_info:
echo $(GIT_INFO) > $@

.PHONY: .release_info
endif

clean:
$(RM) $(patsubst %.cpp, %$(OBJEXT), $(filter %.cpp, $(SRC))) \
$(patsubst %.cpp, %.d, $(filter %.cpp, $(SRC))) \
$(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC))) \
$(patsubst %.cc, %.d, $(filter %.cc, $(SRC))) \
$(CLEANFILES)
$(CLEANFILES) .release_info

.PHONY: first_target clean all
.PHONY: sources generated_files
Expand All @@ -207,4 +222,3 @@ D_FILES1 = $(SRC:.c=.d)
D_FILES = $(D_FILES1:.cpp=.d)

-include $(D_FILES)

3 changes: 3 additions & 0 deletions src/config.inc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,3 +28,6 @@ MINISAT2 = ../../minisat-2.2.1
# Signing identity for MacOS Gatekeeper

OSX_IDENTITY="Developer ID Application: Daniel Kroening"

# Detailed version information
CBMC_VERSION = 5.7
6 changes: 6 additions & 0 deletions src/goto-analyzer/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,12 @@ CLEANFILES = goto-analyzer$(EXEEXT)

all: goto-analyzer$(EXEEXT)

ifeq ($(BUILD_ENV_),MSVC)
CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
else
CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
endif

ifneq ($(wildcard ../java_bytecode/Makefile),)
OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
Expand Down
2 changes: 0 additions & 2 deletions src/goto-analyzer/goto_analyzer_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,8 +42,6 @@ Author: Daniel Kroening, [email protected]
#include <util/string2int.h>
#include <util/unicode.h>

#include <cbmc/version.h>

#include "goto_analyzer_parse_options.h"
#include "taint_analysis.h"
#include "unreachable_instructions.h"
Expand Down
6 changes: 6 additions & 0 deletions src/goto-cc/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,12 @@ all: goto-cl$(EXEEXT)
endif
all: goto-cc$(EXEEXT)

ifeq ($(BUILD_ENV_),MSVC)
CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
else
CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
endif

ifneq ($(wildcard ../java_bytecode/Makefile),)
OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
endif
Expand Down
2 changes: 0 additions & 2 deletions src/goto-cc/as_mode.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,6 @@ Author: Michael Tautschnig
#include <util/get_base_name.h>
#include <util/cout_message.h>

#include <cbmc/version.h>

#include "compile.h"

#include "as_mode.h"
Expand Down
2 changes: 0 additions & 2 deletions src/goto-cc/compile.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,6 @@ Date: June 2006

#include <langapi/mode.h>

#include <cbmc/version.h>

#include "compile.h"

#define DOTGRAPHSETTINGS "color=black;" \
Expand Down
2 changes: 0 additions & 2 deletions src/goto-cc/gcc_mode.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,8 +26,6 @@ Author: CM Wintersteiger, 2006
#include <util/get_base_name.h>
#include <util/run.h>

#include <cbmc/version.h>

#include "compile.h"
#include "gcc_mode.h"

Expand Down
1 change: 0 additions & 1 deletion src/goto-cc/goto_cc_mode.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,6 @@ Author: CM Wintersteiger, 2006
#include <sysexits.h>
#endif

#include <cbmc/version.h>

#include "goto_cc_mode.h"

Expand Down
2 changes: 0 additions & 2 deletions src/goto-cc/ms_cl_mode.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,6 @@ Author: CM Wintersteiger, 2006
#include <util/config.h>
#include <util/get_base_name.h>

#include <cbmc/version.h>

#include "ms_cl_mode.h"
#include "compile.h"

Expand Down
6 changes: 6 additions & 0 deletions src/goto-diff/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,12 @@ CLEANFILES = goto-diff$(EXEEXT)

all: goto-diff$(EXEEXT)

ifeq ($(BUILD_ENV_),MSVC)
CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
else
CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
endif

ifneq ($(wildcard ../java_bytecode/Makefile),)
OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
Expand Down
2 changes: 0 additions & 2 deletions src/goto-diff/goto_diff_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,6 @@ Author: Peter Schrammel

#include <langapi/mode.h>

#include <cbmc/version.h>

#include "goto_diff_parse_options.h"
#include "goto_diff.h"
#include "syntactic_diff.h"
Expand Down
6 changes: 6 additions & 0 deletions src/goto-instrument/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,12 @@ include ../common

all: goto-instrument$(EXEEXT)

ifeq ($(BUILD_ENV_),MSVC)
CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
else
CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
endif

ifneq ($(wildcard ../java_bytecode/Makefile),)
OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
Expand Down
2 changes: 0 additions & 2 deletions src/goto-instrument/goto_instrument_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,6 @@ Author: Daniel Kroening, [email protected]
#include <analyses/constant_propagator.h>
#include <analyses/is_threaded.h>

#include <cbmc/version.h>

#include "goto_instrument_parse_options.h"
#include "document_properties.h"
#include "uninitialized.h"
Expand Down
6 changes: 6 additions & 0 deletions src/memory-models/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,12 @@ CLEANFILES = memory_models$(LIBEXT) \

all: mmcc$(EXEEXT)

ifeq ($(BUILD_ENV_),MSVC)
CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
else
CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
endif

###############################################################################

mm_y.tab.cpp: parser.y
Expand Down
2 changes: 0 additions & 2 deletions src/memory-models/mmcc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]

#include <util/cout_message.h>

#include <cbmc/version.h>

#include "mm_parser.h"
#include "mm2cpp.h"
#include "mmcc_parse_options.h"
Expand Down
6 changes: 6 additions & 0 deletions src/musketeer/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,12 @@ include ../common

all: musketeer$(EXEEXT)

ifeq ($(BUILD_ENV_),MSVC)
CP_CXXFLAGS += /DMUSKETEER_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
else
CP_CXXFLAGS += -DMUSKETEER_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
endif

ifneq ($(LIB_GLPK),)
LIBS += $(LIB_GLPK)
CP_CXXFLAGS += -DHAVE_GLPK
Expand Down
1 change: 0 additions & 1 deletion src/musketeer/musketeer_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,6 @@ Module: Main Module
#include <goto-instrument/wmm/weak_memory.h>

#include "propagate_const_function_pointers.h"
#include "version.h"
#include "musketeer_parse_options.h"
#include "fencer.h"
#include "fence_shared.h"
Expand Down
6 changes: 0 additions & 6 deletions src/musketeer/version.h
View file
Open in desktop

This file was deleted.

6 changes: 6 additions & 0 deletions src/symex/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,12 @@ CLEANFILES = symex$(EXEEXT)

all: symex$(EXEEXT)

ifeq ($(BUILD_ENV_),MSVC)
CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
else
CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
endif

ifneq ($(wildcard ../bv_refinement/Makefile),)
OBJ += ../bv_refinement/bv_refinement$(LIBEXT)
CP_CXXFLAGS += -DHAVE_BV_REFINEMENT
Expand Down
2 changes: 0 additions & 2 deletions src/symex/symex_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,6 @@ Author: Daniel Kroening, [email protected]

#include <langapi/mode.h>

#include <cbmc/version.h>

#include <path-symex/locs.h>

#include "path_search.h"
Expand Down