Opened 3 months ago

Last modified 3 months ago

#38 new defect

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 (1)

comment:1 Changed 3 months ago by mornfall

Milestone: future5.0

Milestone renamed

Note: See TracTickets for help on using tickets.