Use incompleteness behaviour

[benozol]

This PR

• introduces a type to capture a state with a result if the semantics/interpreter covered the execution, or without result for incompletnesses of the interpreters

type result 'a = Result 'a | Incomplete
type state_result 'a = (state, result 'a)

• uses the incompletness behaviour as a result for known utiltiies and arguments that are not implemented. Incompleteness was previously only used for stack overflow or loop limits. This approach allows identifying errorneous behaviour in presence of incomplete behaviour. For example

$ cat test.sh
if mkdir /abc; then
  admin # Not implemented
else
  foo # Error
fi
$ ./bin/colis --run-symbolic test.sh; echo -- $?
* Initial state
- id: init-0
  root: r₁
  cwd: /
  clause: dir(r₁)
  
* Error states
- id: error-1
  root: r₁₄
  cwd: /
  clause: ∃ ?₁₀⋅ r₁ = r₁₄ ∧ r₁[abc]?₁₀ ∧ dir(r₁)
  stdout: |
    [ERR] mkdir /abc: target already exists
    [ERR] Utility foo not found
    
* Incomplete symbolic execution
- id: notcovered-1
  root: r₁₆
  cwd: /
  clause: ∃ abc₆⋅ r₁₆[abc]abc₆ ∧ r₁[abc]↑ ∧ dir(r₁) ∧ dir(abc₆) ∧ dir(r₁₆) ∧ abc₆[∅] ∧ r₁ ~{abc} r₁₆
  stdout: |
    [DBG] mkdir /abc: create directory
    [INCOMPLETE] Utility admin not implemented
    
* Summary

- Success cases: 0
- Error cases: 1
- Incomplete symbolic execution: 1

-- 1

• The difference between an error (foo) and an incompletness (admin) is made by a list of utilities in Utilities (copied from https://pubs.opengroup.org/onlinepubs/9699919799/).
• rename behaviour BFailure into BIncomplete

This required comprehensive changes to SymbolicSpecifications and SymbolicUtilities, and will influence future changes for #65 #69. But I think it’s the right @claudemarche @Niols, what do you think? We can discuss on Wednesday.

Fixes #70