#!/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="--program-only --show-byte-ops --show-vcc --show-goto-symex-steps --show-points-to-sets --slice-formula --unwinding-assertions --no-unwinding-assertions --no-self-loops-to-assumptions --partial-loops --paths --show-symex-strategies --depth --max-field-sensitivity-array-size --no-array-field-sensitivity --graphml-witness --symex-complexity-limit --symex-complexity-failed-child-loops-limit --incremental-loop --unwind-min --unwind-max --ignore-properties-before-unwind-min --symex-cache-dereferences --show-loops --unwind --unwindset --no-standard-checks --preprocess --slice-by-trace --function --no-simplify --full-slice --reachability-slice --reachability-slice-fb --no-propagation --no-simplify-if --document-subgoals --test-preprocessor --show-array-constraints --include --function --c89 --c99 --c11 --c17 --c23 --cpp98 --cpp03 --cpp11 --unsigned-char --round-to-even --round-to-nearest --round-to-plus-inf --round-to-minus-inf --round-to-zero --no-library --arch --os --16 --32 --64 --LP64 --ILP64 --LLP64 --ILP32 --LP32 --little-endian --big-endian --i386-linux --i386-win32 --win32 --winx64 --i386-macos --ppc-macos --gcc --object-bits --malloc-fail-assert --malloc-fail-null --malloc-may-fail --no-malloc-may-fail --string-abstraction --dfcc-debug-lib --dfcc-simple-invalid-pointer-model --bounds-check --pointer-check --memory-leak-check --memory-cleanup-check --div-by-zero-check --float-div-by-zero-check --enum-range-check --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --conversion-check --undefined-shift-check --float-overflow-check --nan-check --no-built-in-assertions --pointer-primitive-check --retain-trivial-checks --error-label --no-assertions --no-assumptions --assert-to-assume --no-bounds-check --no-pointer-check --no-signed-overflow-check --no-pointer-primitive-check --no-undefined-shift-check --no-div-by-zero-check --xml-ui --xml-interface --json-ui --json-interface --smt1 --smt2 --fpa --cvc3 --cvc4 --cvc5 --bitwuzla --boolector --yices --z3 --mathsat --cprover-smt2 --incremental-smt2-solver --external-smt2-solver --sat-solver --external-sat-solver --no-sat-preprocessor --beautify --dimacs --refine --max-node-refinement --refine-arrays --refine-arithmetic --outfile --dump-smt-formula --write-solver-stats-to --refine-strings --string-printable --show-goto-functions --list-goto-functions --show-properties --show-symbol-table --show-parse-tree --drop-unused-functions --property --stop-on-fail --trace --verbosity --no-library --nondet-static --version --export-symex-ready-goto --cover --cover-failed-assertions --show-test-suite --symex-coverage-report --mm --timestamp --arrays-uf-always --arrays-uf-never --flush --localize-faults --trace-json-extended --trace-show-function-calls --trace-show-code --trace-hex --compact-trace --stack-trace --validate-goto-model --validate-ssa-equation --max-nondet-tree-depth --min-null-tree-depth --claim --show-claims --floatbv --all-claims --all-properties --help -D -I -? -h "
  #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|--external-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
