diff --git a/cmake/packaging.cmake b/cmake/packaging.cmake index 53728653bd7..25f49fd6264 100644 --- a/cmake/packaging.cmake +++ b/cmake/packaging.cmake @@ -24,8 +24,9 @@ set(CPACK_PACKAGE_RESOURCE_FILE_README "${CMAKE_CURRENT_SOURCE_DIR}/README.md") # Automatically find dependencies for shared libraries set(CPACK_DEBIAN_PACKAGE_SHLIBDEPS YES) -# In addition, we depend on gcc for preprocessing -set(CPACK_DEBIAN_PACKAGE_DEPENDS gcc) +# In addition, we depend on gcc for preprocessing and bash-completion to make +# CBMC's bash completion work +set(CPACK_DEBIAN_PACKAGE_DEPENDS "gcc, bash-completion") # Enable debug output so that we can see the dependencies being generated in the # logs diff --git a/scripts/bash-autocomplete/Readme.md b/scripts/bash-autocomplete/Readme.md index a56074561da..2da762f390a 100644 --- a/scripts/bash-autocomplete/Readme.md +++ b/scripts/bash-autocomplete/Readme.md @@ -23,6 +23,8 @@ Follow 1. 2. and 3. as above. 4. Put the following at the end of your `~/.zshrc`, with the directories adapted to your directory structure: ```bash + autoload -Uz compinit + compinit autoload bashcompinit bashcompinit cbmcautocomplete=~/diffblue/cbmc/scripts/bash-autocomplete/cbmc.sh diff --git a/scripts/bash-autocomplete/cbmc.sh.template b/scripts/bash-autocomplete/cbmc.sh.template index 0e241d0b3bf..355019e84f2 100644 --- a/scripts/bash-autocomplete/cbmc.sh.template +++ b/scripts/bash-autocomplete/cbmc.sh.template @@ -19,14 +19,30 @@ _cbmc_autocomplete() COMPREPLY=( $( compgen -W "sc tso pso" -- $cur ) ) return 0 ;; - --arch) #for architecture we list the options explicitly - COMPREPLY=( $( compgen -W "i386 x86_64" -- $cur ) ) + --arch) #for architecture we list the options explicitly; this list is populated using + # `grep -w 'arch[[:space:]]*==' src/util/config.cpp | cut # -f2 -d'"' | sort` + COMPREPLY=( $( compgen -W "alpha arm arm64 armel armhf hppa i386 ia64 mips mips64 mips64el mipsel mipsn32 mipsn32el none powerpc ppc64 ppc64le riscv64 s390 s390x sh4 sparc sparc64 v850 x32 x86_64" -- $cur ) ) return 0 ;; - -I|--classpath|-cp|--outfile|--existing-coverage|--graphml-cex) + --os) #for architecture we list the options explicitly + COMPREPLY=( $( compgen -W "freebsd linux macos solaris windows" -- $cur ) ) + return 0 + ;; + --timestamp) #for timestamp we list the options explicitly + COMPREPLY=( $( compgen -W "monotonic wall" -- $cur ) ) + return 0 + ;; + --paths) #for paths we list the options explicitly + COMPREPLY=( $( compgen -W "fifo lifo" -- $cur ) ) + return 0 + ;; + -I|--classpath|-cp) # a directory + _filedir -d + return 0 + ;; + --external-sat-solver|--incremental-smt2-solver) #a switch that takes a file parameter of which we don't know an extension - #TODO probably we can do more for -I, --classpath, -cp - COMPREPLY=( $(compgen -f -- $cur) ) + _filedir -f return 0 ;; esac diff --git a/scripts/bash-autocomplete/extract_switches.sh b/scripts/bash-autocomplete/extract_switches.sh index e000b469bea..c876e420af7 100755 --- a/scripts/bash-autocomplete/extract_switches.sh +++ b/scripts/bash-autocomplete/extract_switches.sh @@ -1,23 +1,17 @@ #!/bin/bash -echo "Compiling the helper file to extract the raw list of parameters from cbmc" -g++ -c -MMD -MP -std=c++11 -Wall -I ../../src/ -ftrack-macro-expansion=0 -fno-diagnostics-show-caret switch_extractor_helper.c -o tmp.o 2> pragma.txt -retval=$? +set -e -#clean up compiled files, we don't need them. -rm tmp.o 2> /dev/null -rm tmp.d 2> /dev/null +# make sure we execute the remainder in the directory containing this script +cd `dirname $0` -#check if compilation went fine -if [ $retval -ne 0 ]; then - echo "Problem compiling the helper file, parameter list not extracted." - exit 1; -fi +echo "Compiling the helper file to extract the raw list of parameters from cbmc" +g++ -E -dM -std=c++11 -I../../src ../../src/cbmc/cbmc_parse_options.cpp -o macros.c +echo CBMC_OPTIONS >> macros.c echo "Converting the raw parameter list to the format required by autocomplete scripts" -rawstring=`sed "s/^.*pragma message: \(.*\)/\1/" pragma.txt` -#delete pragma file, we won't need it -rm pragma.txt 2> /dev/null +rawstring="`gcc -E -P -w macros.c` \"?h(help)\"" +rm macros.c #now the main bit, convert from raw format to a proper list of switches cleanstring=`( @@ -26,7 +20,7 @@ cleanstring=`( (echo $rawstring | grep -o "([^)]*)" | sed "s/^.\(.*\).$/--\1/") ; #extract 1-hyphen switches, such as -F #use sed to remove all (foo) expressions, then you're left with switches and ':', so grep the colons out and then use sed to include the '-' - (echo $rawstring | sed "s/([^)]*)//g" | grep -o "[a-zA-Z0-9]" | sed "s/\(.*\)/-\1/") + (echo $rawstring | sed "s/([^)]*)//g" | grep -o "[a-zA-Z0-9?]" | sed "s/\(.*\)/-\1/") ) | tr '\n' ' '` #sanity check that there is only one line of output @@ -36,13 +30,10 @@ if [ `echo $cleanstring | wc -l | awk '{print $1}'` -ne 1 ]; then fi #sanity check that there are no dangerous characters -echo $cleanstring | grep -q "[^a-zA-Z0-9 -]" -if [ $? -eq 0 ]; then +if echo $cleanstring | grep -q "[^a-zA-Z0-9? -]"; then echo "Problem converting the parameter list to the correct format, illegal characters detected. This is likely to be an error in this conversion script." exit 1; fi echo "Injecting the parameter list to the autocomplete file." sed "5 s/.*/ local switches=\"$cleanstring\"/" cbmc.sh.template > cbmc.sh - -rm pragma.txt 2> /dev/null diff --git a/src/cbmc/CMakeLists.txt b/src/cbmc/CMakeLists.txt index 85968407c55..0e26151180e 100644 --- a/src/cbmc/CMakeLists.txt +++ b/src/cbmc/CMakeLists.txt @@ -57,3 +57,19 @@ if(NOT WIN32) PATTERN "c*" PATTERN "g*") endif() + +# bash completion +if(NOT WIN32) + add_custom_command(OUTPUT "${CMAKE_SOURCE_DIR}/scripts/bash-autocomplete/cbmc.sh" + COMMAND "${CMAKE_SOURCE_DIR}/scripts/bash-autocomplete/extract_switches.sh" + DEPENDS $ + ) + add_custom_target(cbmc.sh ALL + DEPENDS "${CMAKE_SOURCE_DIR}/scripts/bash-autocomplete/cbmc.sh" + ) + install( + FILES ${CMAKE_SOURCE_DIR}/scripts/bash-autocomplete/cbmc.sh + DESTINATION etc/bash_completion.d + RENAME cbmc + ) +endif()