Generating GOTO Program failed with Numeric exception

[Sepideh Asadi]

Dear CProver developers,

when I was trying to verify a C program using CBMC-5.12 I got an error in the initial phase of generating goto-program.

I ran ./cbmc --unwind 2  attachedFile.c

The error message is shown below and the C file is attached.

Generating GOTO Program

file /work/ldvuser/novikov/work/current--X--drivers/block/drbd/drbd.ko--X--defaultlinux--X--08_1a--X--cpachecker/linux/csd_deg_dscv/20/dscv_tempdir/dscv/ri/08_1a/drivers/block/drbd/drbd_actlog.c.prepared line 82 function trace_drbd_resync: '__builtin_va_start' expected to have two arguments

Numeric exception : 0

Best regards,

Sepideh