Project

General

Profile

Bug #7277

timeout in ssh categories; several examples stop in early stages

Added by Sepideh Asadi almost 6 years ago. Updated almost 6 years ago.

Status:
New
Priority:
Urgent
Assignee:
-
Start date:
07/05/2018
Due date:
% Done:

0%

Estimated time:

Description

File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/c/ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c
File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c
File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c

Verification not successful, here is the last few lines: ...

Converting
Type-checking s3_srvr.blast.08_false-unreach-call.i.cil
Generating GOTO Program
Ignoring CPROVER library
Removal of function pointers and virtual functions
Generic Property Instrumentation
LOAD Time: 2.419 sec.
Total number of claims in program...(1)
A specific claim is not set, nor any other claim specification is set.
Warrning: --claim is set to 1.
; Warning: disabling SATElite preprocessing to track proof
Use QF_UF logic.

---------checking claim # 1 ---------

; Warning: disabling SATElite preprocessing to track proof
Command terminated by signal 24
timeout 200 (s)

History

#1 Updated by Sepideh Asadi almost 6 years ago

and also ssh-simplified categories suffer from the same problem:

File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/c/ssh-simplified/s3_srvr_8_true-unreach-call.cil.c

File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/c/ssh-simplified/s3_clnt_3_true-unreach-call.cil.c

File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/ct/ssh-simplified/s3_srvr_4_true-unreach-call.cil.c

.
.
.

#2 Updated by Sepideh Asadi almost 6 years ago

for instance CBMC for this example take 29 second to verify this: ssh-simplified/s3_srvr_7_true-unreach-call.cil.c

Also available in: Atom PDF