Skip to content

CBMC error caused by conditional statements if 2nd operand is missing #2662

Closed
@polgreen

Description

@polgreen

CBMC can't currently handle correctly conditional statements without the 2nd operand, e.g., C = A?: B, equivalent to C = A ? A : B

The following example causes CBMC to return the error
file conditional.c line 6 function main: symex_assign: unexpected side effect: gcc_conditional_expression

int A = 10;
int B = 20;

int main()
{
  int C = A ?: B;   
 __CPROVER_assert(0,"");
}

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions