#38 closed defect (fixed)

Report attempts to use symbolic data if symbolic is disable

Reported by: Vladimír Štill Owned by: mornfall
Priority: major Milestone: 5.0
Component: other Keywords:
Cc:

Description

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).

Change History (2)

comment:1 Changed 22 months ago by mornfall

Milestone: future5.0

Milestone renamed

comment:2 Changed 10 months ago by mornfall

Resolution: fixed
Status: newclosed

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
Note: See TracTickets for help on using tickets.