User Tools

Site Tools


sv-comp_2015_heap-manipulation

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
sv-comp_2015_heap-manipulation [2015/01/14 15:35]
ruben
sv-comp_2015_heap-manipulation [2015/01/14 15:38] (current)
dneville
Line 1: Line 1:
 Michael says: According to my analysis, there are no current issues here in current trunk. Michael says: According to my analysis, there are no current issues here in current trunk.
  
-Daniel ​says: Judging by the cases I've investigated so far, this appears to be the case.  ​I am now working with Daniel P.+Daniel says:  Turns out there was a few errors here in the generation of the graph. ​ In particular code in the form "​!n@m"​ where n and m are integers in the witness XML generation. ​ There are also some issues with $pad0 (i.e. padding) being appended to variable namescausing issues. ​ Michael was present during ​this discussion and has said he will fix these issues. 
 + 
 +Interestingly, ​the presence of # (hash) in the variable names does not cause any issues.  ​Possibly because CPAChecker does not attempt to verify variables names as valid.
  
 ====== Analysis of witness invalid output: ====== ====== Analysis of witness invalid output: ======
Line 37: Line 39:
 Timeouts due to a while loop that cannot be unwound. On line 49: while (_****_VERIFIER_nondet_int()) Timeouts due to a while loop that cannot be unwound. On line 49: while (_****_VERIFIER_nondet_int())
  
-====== Error analysis ====== 
- 
-These return TRUE when it should be FALSE or witness invalid in the competition. 
- 
-In current trunk these all work correctly. 
- 
-**ddv-machzwd/​ddv_machzwd_all_false-unreach-call.i 
-** 
- 
-Returns false correctly. ​ Appears to be functioning correctly. ​ Witness unchecked. 
- 
-**ddv-machzwd/​ddv_machzwd_inw_false-unreach-call.i** 
- 
-Returns false correctly. ​ Appears to be functioning correctly. ​ Witness unchecked. 
- 
-**ddv-machzwd/​ddv_machzwd_outb_false-unreach-call.i 
-** 
- 
-Returns false correctly. ​ Appears to be functioning correctly. ​ Witness unchecked. 
  
sv-comp_2015_heap-manipulation.txt · Last modified: 2015/01/14 15:38 by dneville