1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
#!/usr/bin/env bash
_cbmc_autocomplete()
{
#list of all switches cbmc has. IMPORTANT: in the template file, this variable must be defined on line 5.
local switches=""
#word on which the cursor is
local cur=${COMP_WORDS[COMP_CWORD]}
#previous word (in case it is a switch with a parameter)
local prev=${COMP_WORDS[COMP_CWORD-1]}
#check if the command before cursor is a switch that takes parameters, if yes,
#offer a choice of parameters
case "$prev" in
--cover) #for coverage we list the options explicitly
COMPREPLY=( $( compgen -W "assertion path branch location decision condition mcdc cover" -- $cur ) )
return 0
;;
--mm) #for memory models we list the options explicitly
COMPREPLY=( $( compgen -W "sc tso pso" -- $cur ) )
return 0
;;
--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
;;
--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
_filedir -f
return 0
;;
esac
#complete a switch from a standard list, if the parameter under cursor starts with a hyphen
if [[ "$cur" == -* ]]; then
COMPREPLY=( $( compgen -W "$switches" -- $cur ) )
return 0
fi
#if none of the above applies, offer directories and files that we can analyze
_filedir -d
COMPREPLY+=( $(compgen -G "$cur*.c") )
COMPREPLY+=( $(compgen -G "$cur*.c\+\+") )
COMPREPLY+=( $(compgen -G "$cur*.cc") )
COMPREPLY+=( $(compgen -G "$cur*.class") )
COMPREPLY+=( $(compgen -G "$cur*.cpp") )
COMPREPLY+=( $(compgen -G "$cur*.cxx") )
COMPREPLY+=( $(compgen -G "$cur*.gb") )
COMPREPLY+=( $(compgen -G "$cur*.i") )
COMPREPLY+=( $(compgen -G "$cur*.ii") )
COMPREPLY+=( $(compgen -G "$cur*.jar") )
}
complete -F _cbmc_autocomplete cbmc
|
