Skip to content

Make CBMC more fun #1989

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 1 commit into from
Closed

Make CBMC more fun #1989

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
6 changes: 3 additions & 3 deletions src/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ add_subdirectory(goto-symex)
add_subdirectory(jsil)
add_subdirectory(json)
add_subdirectory(langapi)
add_subdirectory(linking)
add_subdirectory(inking)
add_subdirectory(memory-models)
add_subdirectory(pointer-analysis)
add_subdirectory(solvers)
Expand All @@ -102,7 +102,7 @@ add_subdirectory(clobber)

add_subdirectory(cbmc)
add_subdirectory(jbmc)
add_subdirectory(goto-cc)
add_subdirectory(goto-instrument)
add_subdirectory(goto-sea-sea)
add_subdirectory(goto-inkstrument)
add_subdirectory(goto-analyzer)
add_subdirectory(goto-diff)
24 changes: 12 additions & 12 deletions src/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
DIRS = ansi-c big-int cbmc jbmc cpp goto-cc goto-instrument goto-programs \
goto-symex langapi pointer-analysis solvers util linking xmllang \
DIRS = ansi-c big-int cbmc jbmc cpp goto-sea-sea goto-inkstrument goto-programs \
goto-symex langapi pointer-analysis solvers util inking xmllang \
assembler analyses java_bytecode \
json goto-analyzer jsil goto-diff clobber \
memory-models miniz

all: cbmc.dir jbmc.dir goto-cc.dir goto-instrument.dir \
all: cbmc.dir jbmc.dir goto-sea-sea.dir goto-inkstrument.dir \
goto-analyzer.dir goto-diff.dir

###############################################################################
Expand All @@ -17,32 +17,32 @@ $(patsubst %, %.dir, $(filter-out big-int util, $(DIRS))): util.dir
.PHONY: languages
.PHONY: clean

cpp.dir: ansi-c.dir linking.dir
cpp.dir: ansi-c.dir inking.dir

java_bytecode.dir: miniz.dir

languages: util.dir langapi.dir \
cpp.dir ansi-c.dir xmllang.dir assembler.dir java_bytecode.dir \
jsil.dir

goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
goto-symex.dir linking.dir analyses.dir solvers.dir \
goto-inkstrument.dir: languages goto-programs.dir pointer-analysis.dir \
goto-symex.dir inking.dir analyses.dir solvers.dir \
json.dir

cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \
pointer-analysis.dir goto-programs.dir linking.dir \
goto-instrument.dir
pointer-analysis.dir goto-programs.dir inking.dir \
goto-inkstrument.dir

jbmc.dir: java_bytecode.dir cbmc.dir

goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \
json.dir goto-instrument.dir
goto-analyzer.dir: languages analyses.dir goto-programs.dir inking.dir \
json.dir goto-inkstrument.dir

goto-diff.dir: languages goto-programs.dir pointer-analysis.dir \
linking.dir analyses.dir goto-instrument.dir \
inking.dir analyses.dir goto-inkstrument.dir \
solvers.dir json.dir goto-symex.dir

goto-cc.dir: languages pointer-analysis.dir goto-programs.dir linking.dir
goto-sea-sea.dir: languages pointer-analysis.dir goto-programs.dir inking.dir

# building for a particular directory

Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -123,4 +123,4 @@ set_source_files_properties(

generic_includes(ansi-c)

target_link_libraries(ansi-c util linking goto-programs assembler)
target_link_libraries(ansi-c util inking goto-programs assembler)
2 changes: 1 addition & 1 deletion src/ansi-c/ansi_c_entry_point.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ Author: Daniel Kroening, [email protected]
#include <util/symbol.h>

#include <goto-programs/goto_functions.h>
#include <linking/static_lifetime_init.h>
#include <inking/static_lifetime_init.h>

#include "c_nondet_symbol_factory.h"

Expand Down
6 changes: 3 additions & 3 deletions src/ansi-c/ansi_c_language.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,8 @@ Author: Daniel Kroening, [email protected]
#include <util/config.h>
#include <util/get_base_name.h>

#include <linking/linking.h>
#include <linking/remove_internal_symbols.h>
#include <inking/inking.h>
#include <inking/remove_internal_symbols.h>

#include "ansi_c_entry_point.h"
#include "ansi_c_typecheck.h"
Expand Down Expand Up @@ -118,7 +118,7 @@ bool ansi_c_languaget::typecheck(

remove_internal_symbols(new_symbol_table);

if(linking(symbol_table, new_symbol_table, get_message_handler()))
if(inking(symbol_table, new_symbol_table, get_message_handler()))
return true;

return false;
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/c_nondet_symbol_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ Author: Diffblue Ltd.
#include <util/std_types.h>
#include <util/string_constant.h>

#include <linking/zero_initializer.h>
#include <inking/zero_initializer.h>

#include <goto-programs/goto_functions.h>

Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/c_typecheck_base.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
if(symbol.is_file_local)
{
// file-local stuff -- stays as is
// collisions are resolved during linking
// collisions are resolved during inking
}
else if(symbol.is_extern && !is_function)
{
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/c_typecheck_code.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
#include "c_typecheck_base.h"

#include <util/config.h>
#include <linking/zero_initializer.h>
#include <inking/zero_initializer.h>

#include "ansi_c_declaration.h"

Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/c_typecheck_initializer.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Author: Daniel Kroening, [email protected]
#include <util/string_constant.h>
#include <util/type_eq.h>

#include <linking/zero_initializer.h>
#include <inking/zero_initializer.h>

#include "anonymous_member.h"

Expand Down
12 changes: 6 additions & 6 deletions src/ansi-c/library/jsa.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -391,7 +391,7 @@ __CPROVER_jsa_inline _Bool __CPROVER_jsa__internal_is_in_valid_list(
;
#endif

__CPROVER_jsa_inline void __CPROVER_jsa__internal_assume_linking_correct(
__CPROVER_jsa_inline void __CPROVER_jsa__internal_assume_inking_correct(
const __CPROVER_jsa_abstract_heapt * const heap,
const __CPROVER_jsa_node_id_t node_id,
const __CPROVER_jsa_node_id_t prev,
Expand Down Expand Up @@ -419,7 +419,7 @@ __CPROVER_jsa_inline void __CPROVER_jsa__internal_assume_linking_correct(
;
#endif

__CPROVER_jsa_inline void __CPROVER_jsa__internal_assume_valid_iterator_linking(
__CPROVER_jsa_inline void __CPROVER_jsa__internal_assume_valid_iterator_inking(
const __CPROVER_jsa_abstract_heapt * const h,
const __CPROVER_jsa_list_id_t list,
const __CPROVER_jsa_node_id_t node_id,
Expand Down Expand Up @@ -596,7 +596,7 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap(
__CPROVER_jsa_assume(h->list_head_nodes[node_list] == cnode);
__CPROVER_jsa_assume(__CPROVER_jsa__internal_is_valid_node_id(nxt));
__CPROVER_jsa_assume(__CPROVER_jsa__internal_is_valid_node_id(prev));
__CPROVER_jsa__internal_assume_linking_correct(h, cnode, prev, nxt);
__CPROVER_jsa__internal_assume_inking_correct(h, cnode, prev, nxt);
}
}
#if 0 < __CPROVER_JSA_MAX_ABSTRACT_NODES
Expand All @@ -610,7 +610,7 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap(
__CPROVER_jsa_assume(__CPROVER_jsa__internal_is_valid_node_id(prev));
const __CPROVER_jsa_id_t nid=
__CPROVER_jsa__internal_get_abstract_node_id(anode);
__CPROVER_jsa__internal_assume_linking_correct(h, nid, prev, nxt);
__CPROVER_jsa__internal_assume_inking_correct(h, nid, prev, nxt);
}
#endif
#if 0 < __CPROVER_JSA_MAX_ABSTRACT_RANGES
Expand Down Expand Up @@ -644,9 +644,9 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap(
else
{
__CPROVER_jsa_assume(list < h->list_count);
__CPROVER_jsa__internal_assume_valid_iterator_linking(
__CPROVER_jsa__internal_assume_valid_iterator_inking(
h, list, next_node, next_index);
__CPROVER_jsa__internal_assume_valid_iterator_linking(
__CPROVER_jsa__internal_assume_valid_iterator_inking(
h, list, prev_node, prev_index);
if(__CPROVER_jsa_null!=next_node && __CPROVER_jsa_null != prev_node)
__CPROVER_jsa__internal_assume_is_neighbour(
Expand Down
4 changes: 2 additions & 2 deletions src/cbmc/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,13 @@ target_link_libraries(cbmc-lib
assembler
big-int
cpp
goto-instrument-lib
goto-inkstrument-lib
goto-programs
goto-symex
java_bytecode
json
langapi
linking
inking
pointer-analysis
solvers
util
Expand Down
28 changes: 14 additions & 14 deletions src/cbmc/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ SRC = all_properties.cpp \
OBJ += ../ansi-c/ansi-c$(LIBEXT) \
../cpp/cpp$(LIBEXT) \
../java_bytecode/java_bytecode$(LIBEXT) \
../linking/linking$(LIBEXT) \
../inking/inking$(LIBEXT) \
../big-int/big-int$(LIBEXT) \
../goto-programs/goto-programs$(LIBEXT) \
../goto-symex/goto-symex$(LIBEXT) \
Expand All @@ -31,19 +31,19 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
../pointer-analysis/add_failed_symbols$(OBJEXT) \
../pointer-analysis/rewrite_index$(OBJEXT) \
../pointer-analysis/goto_program_dereference$(OBJEXT) \
../goto-instrument/reachability_slicer$(OBJEXT) \
../goto-instrument/full_slicer$(OBJEXT) \
../goto-instrument/nondet_static$(OBJEXT) \
../goto-instrument/cover$(OBJEXT) \
../goto-instrument/cover_basic_blocks$(OBJEXT) \
../goto-instrument/cover_filter$(OBJEXT) \
../goto-instrument/cover_instrument_branch$(OBJEXT) \
../goto-instrument/cover_instrument_condition$(OBJEXT) \
../goto-instrument/cover_instrument_decision$(OBJEXT) \
../goto-instrument/cover_instrument_location$(OBJEXT) \
../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
../goto-instrument/cover_instrument_other$(OBJEXT) \
../goto-instrument/cover_util$(OBJEXT) \
../goto-inkstrument/reachability_slicer$(OBJEXT) \
../goto-inkstrument/full_slicer$(OBJEXT) \
../goto-inkstrument/nondet_static$(OBJEXT) \
../goto-inkstrument/cover$(OBJEXT) \
../goto-inkstrument/cover_basic_blocks$(OBJEXT) \
../goto-inkstrument/cover_filter$(OBJEXT) \
../goto-inkstrument/cover_instrument_branch$(OBJEXT) \
../goto-inkstrument/cover_instrument_condition$(OBJEXT) \
../goto-inkstrument/cover_instrument_decision$(OBJEXT) \
../goto-inkstrument/cover_instrument_location$(OBJEXT) \
../goto-inkstrument/cover_instrument_mcdc$(OBJEXT) \
../goto-inkstrument/cover_instrument_other$(OBJEXT) \
../goto-inkstrument/cover_util$(OBJEXT) \
../analyses/analyses$(LIBEXT) \
../langapi/langapi$(LIBEXT) \
../xmllang/xmllang$(LIBEXT) \
Expand Down
36 changes: 32 additions & 4 deletions src/cbmc/cbmc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,10 +54,10 @@ Author: Daniel Kroening, [email protected]
#include <goto-symex/rewrite_union.h>
#include <goto-symex/adjust_float_expressions.h>

#include <goto-instrument/reachability_slicer.h>
#include <goto-instrument/full_slicer.h>
#include <goto-instrument/nondet_static.h>
#include <goto-instrument/cover.h>
#include <goto-inkstrument/reachability_slicer.h>
#include <goto-inkstrument/full_slicer.h>
#include <goto-inkstrument/nondet_static.h>
#include <goto-inkstrument/cover.h>

#include <pointer-analysis/add_failed_symbols.h>

Expand Down Expand Up @@ -876,6 +876,34 @@ void cbmc_parse_optionst::help()
// clang-format off
std::cout <<
"\n"
" _________ \n"
" _______. _ _ .___/ \ \n"
" / -_ / \ / \ / _ _ | \n"
" | _ _ \ | \/ | / / \/ \ | \n"
" | / \ / \| \ / | |.||.| / \n"
" | |.| |.|| \ / | \_/\_/ / \n"
" \_ \_/ \_// \ / \ ___ _/ \n"
" \ _/ \/ \_\_/ / \n"
" | \_/ ___\| / \n"
" ..____/_.. /.-_/o\____/.. \n"
" .. || o\o \~.o. //~ //..|| \\ .. \n"
" .. |/ .|| \\.. // || ..|| || .. \n"
" .. //o .o\\ || .. // // .. // || . \n"
" .. || .. \o \\ //. // .. || || .. \n"
" .. o// .. \\ ^\// .. // . |/ .\| .. \n"
" .. // .. || /\ .// .. // . \\ .. \n"
" .. |/ .. \| //\| || ../| .. || .. \n"
" o .. o l o //.. .|\ .. \\ .. \n"
" .. |/ .. |/ .. \| .. \n"
" o . o o \n"
" \n"
" ______________ ________ \n"
" / __ | ___ | \/ / __ \ \n"
" | / \| |_/ | . . | / \/ \n"
" | | | ___ | |\/| | | \n"
" | \__/| |_/ | | | | \__/\ \n"
" \____\____/\_| |_/\____/ \n"
" \n"
"* * CBMC " CBMC_VERSION " - Copyright (C) 2001-2018 ";

std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
Expand Down
12 changes: 6 additions & 6 deletions src/cbmc/dist-linux
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,17 +12,17 @@ DEB_ARCH=`dpkg --print-architecture`

echo $VERSION_FILE

(cd ../goto-cc; make; strip goto-cc)
(cd ../goto-instrument; make; strip goto-instrument)
(cd ../goto-sea-sea; make; strip goto-sea-sea)
(cd ../goto-inkstrument; make; strip goto-inkstrument)

mkdir /tmp/cbmc-dist
cp ../cbmc/cbmc ../goto-cc/goto-cc \
../goto-instrument/goto-instrument /tmp/cbmc-dist/
cp ../cbmc/cbmc ../goto-sea-sea/goto-sea-sea \
../goto-inkstrument/goto-inkstrument /tmp/cbmc-dist/
cp ../../LICENSE /tmp/cbmc-dist/
cp ../../doc/man/cbmc.1 /tmp/cbmc-dist/
cd /tmp/cbmc-dist
tar cfz cbmc-${VERSION_FILE}-linux-${BITS}.tgz cbmc \
goto-cc goto-instrument LICENSE
goto-sea-sea goto-inkstrument LICENSE

mkdir debian
mkdir debian/DEBIAN
Expand All @@ -31,7 +31,7 @@ mkdir debian/usr/bin
mkdir debian/usr/share
mkdir debian/usr/share/man
mkdir debian/usr/share/man/man1
cp cbmc goto-cc goto-instrument \
cp cbmc goto-sea-sea goto-inkstrument \
debian/usr/bin/
cp cbmc.1 debian/usr/share/man/man1

Expand Down
8 changes: 4 additions & 4 deletions src/cbmc/dist-macos
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ umask u=rwx,g=rx,o=rx

make cbmc-mac-signed

(cd ../goto-cc; make goto-cc-mac-signed)
(cd ../goto-instrument; make goto-instrument-mac-signed)
(cd ../goto-sea-sea; make goto-sea-sea-mac-signed)
(cd ../goto-inkstrument; make goto-inkstrument-mac-signed)

VERSION=`./cbmc --version`
VERSION_FILE=`echo $VERSION | sed "y/./-/"`
Expand All @@ -22,8 +22,8 @@ mkdir /tmp/cbmc-dist/package-root/usr/local/bin
mkdir /tmp/cbmc-dist/resources
mkdir /tmp/cbmc-dist/resources/en.lproj

cp ../cbmc/cbmc ../goto-cc/goto-cc \
../goto-instrument/goto-instrument /tmp/cbmc-dist/package-root/usr/local/bin/
cp ../cbmc/cbmc ../goto-sea-sea/goto-sea-sea \
../goto-inkstrument/goto-inkstrument /tmp/cbmc-dist/package-root/usr/local/bin/
cp ../../LICENSE /tmp/cbmc-dist/resources/license.html
cp distribution.xml /tmp/cbmc-dist/

Expand Down
8 changes: 4 additions & 4 deletions src/cbmc/dist-win
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,19 +8,19 @@ VERSION_FILE=`echo $VERSION | sed "y/./-/"`

echo $VERSION_FILE

(cd ../goto-cc; make; strip goto-cc.exe ; cp goto-cc.exe goto-cl.exe)
(cd ../goto-instrument; make; strip goto-instrument.exe)
(cd ../goto-sea-sea; make; strip goto-sea-sea.exe ; cp goto-sea-sea.exe goto-cl.exe)
(cd ../goto-inkstrument; make; strip goto-inkstrument.exe)

mkdir /tmp/cbmc-dist
cp ../cbmc/cbmc.exe \
../goto-cc/goto-cl.exe ../goto-instrument/goto-instrument.exe \
../goto-sea-sea/goto-cl.exe ../goto-inkstrument/goto-inkstrument.exe \
/tmp/cbmc-dist/
cp ~/progr/cbmc.vs64/src/cbmc/cbmc.exe /tmp/cbmc-dist/cbmc64.exe
cp ../../LICENSE /tmp/cbmc-dist/LICENSE.txt
unix2dos /tmp/cbmc-dist/LICENSE.txt
cd /tmp/cbmc-dist
zip -9 cbmc-${VERSION_FILE}-win.zip cbmc.exe \
cbmc64.exe goto-instrument.exe goto-cl.exe LICENSE.txt
cbmc64.exe goto-inkstrument.exe goto-cl.exe LICENSE.txt

echo Copying.
scp cbmc-${VERSION_FILE}-win.zip [email protected]:/srv/www/cprover.org/cbmc/download/
Expand Down
4 changes: 2 additions & 2 deletions src/clobber/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ generic_includes(clobber-lib)
target_link_libraries(clobber-lib
ansi-c
cpp
linking
inking
big-int
goto-programs
analyses
Expand All @@ -21,7 +21,7 @@ target_link_libraries(clobber-lib
util
goto-symex
pointer-analysis
goto-instrument-lib
goto-inkstrument-lib
)

add_if_library(clobber-lib bv_refinement)
Expand Down
Loading