Project

General

Profile

Actions
Copy link

Bug #4689

closed

Caught exception: symex_assign_rec: unexpected assignment to union member

Added by Sepideh Asadi over 7 years ago. Updated over 7 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Karine Even Mendoza
Start date:
07/03/2017
Due date:
% Done:

100%

Estimated time:

Description

./hifrog --claim 7 ~/dev/hi-bench/main-bench/Funfrog15_bench/disk.c --logic prop/qflra/qfuf

Actions
Copy link
 #1

Updated by Sepideh Asadi over 7 years ago

expected result for claim 7: successful verification

This problem is happening in almost all of disk.c
Caught exception: symex_assign_rec: unexpected assignment to union member

Actions
Copy link
 #2

Updated by Karine Even Mendoza over 7 years ago

  • Assignee set to Karine Even Mendoza
  • % Done changed from 0 to 60

Cprover bug - follow up when upgrading the versions

Actions
Copy link
 #3

Updated by Karine Even Mendoza over 7 years ago

  • % Done changed from 60 to 70

After cprover upgrade, all works but prop logic, need to check the assert there.

Actions
Copy link
 #4

Updated by Karine Even Mendoza over 7 years ago

  • Status changed from New to In Progress
Actions
Copy link
 #5

Updated by Karine Even Mendoza over 7 years ago

  • Status changed from In Progress to Closed
  • % Done changed from 70 to 100

fixed. added optimisations from cbmc

Actions
Copy link

Also available in: Atom PDF