Report attempts to use symbolic data if symbolic is disable

[Vladimír Štill]

Currently, if a benchmark which contains symbolic data is analyzed without --symbolic, DIVINE silently proceeds with 0 as the value of would-be-symbolic variables. E.g., divine check test/sym/call-a.pkg.cpp reports no errors. This situation should be reported as an error, or, alternatively, DIVINE should auto-configure based on the analyzed program and run --symbolic automatically (but this would be harder probably).

[mornfall]

Milestone renamed

[mornfall]

As of today's next, it should be impossible to accidentally run symbolic models in explicit mode.

$ divine check boom.c
compiling boom.c
loading bitcode … DiOS … LART … RR … constants … ERROR: unresolved symbol (function): __lamp_any_i8

$ divine check --lamp-config symbolic boom.c
compiling boom.c
loading bitcode … DiOS … LART … RR … constants … done
booting … done
states per second: 26.3158                                                        
state count: 1
mips: 0
ERROR: Cannot evaluate an assumption without a solver.
Did you mean to use --symbolic?

$ divine check --symbolic boom.c
compiling boom.c
loading bitcode … DiOS … LART … RR … constants … done
booting … done
states per second: 38.961                                                         
state count: 3
mips: 0.28
symbolic: 1

error found: yes
error trace: |
  ASSUME (not (= var_1 #x00000000))
  (0) Non-zero exit code: 1
  FAULT: exit called with non-zero value
  [0] FATAL: unknown in userspace

active stack:
  - symbol: void __dios::FaultBase::handler<__dios::Context>(_VM_Fault, _VM_Frame*, void (*)())
    location: /dios/sys/fault.hpp:119
  - symbol: __dios_fault
    location: /dios/arch/divm/fault.c:12
  - symbol: _exit
    location: /dios/libc/sys/start.cpp:62
  - symbol: _Exit
    location: /dios/libc/stdlib/_Exit.c:19
  - symbol: exit
    location: /dios/libc/stdlib/exit.c:6
  - symbol: __dios_start
    location: /dios/libc/sys/start.cpp:110
a report was written to boom.report