Open
Description
ID_case
and ID_cond
expressions are used in cbmc/develop but there are no corresponding expression types in std_expr.h
. Moreover, ID_case
and ID_cond
are not assigned in cbmc/develop (they are assigned in EBMC).
New expression types should be added to std_expr.h
and then the code in cbmc/develop should be refactored to use those instead of plain exprt
.
Metadata
Metadata
Assignees
Labels
No labels