Problems in SV-COMP

[otis01329]

I have some doubts about the use of DIVINE4 software.

In C++ file:

#############################
#include <iostream>
#include <assert.h>

using namespace std;

extern int VERIFIER_nondet_int();

int main() {

int x = VERIFIER_nondet_int();
cout<<"x = "<<x<<endl;
assert(x==0);

}
#############################
command :
divine check testcpp.cpp

error message:
compiling testcpp.cpp
loading bitcode … LART … RR … constants … ERROR: Program::insert: Unresolved symbol (function): _Z21VERIFIER_nondet_intv

What can I do to solve the problems in C++ files?

2.

In C file:

#############################
#include <stdio.h>
#include <assert.h>

extern int VERIFIER_nondet_int();

int main() {

int x = VERIFIER_nondet_int();
printf("x = %d",x);
assert(x==0);

}
#############################
command :
divine check testc.c

Divine4 did not verify any errors in the C file.
Because the value of the variable X is always zero.
(int x = VERIFIER_nondet_int())
Can't feel the effect of VERIFIER_nondet_int().

[Henrich Lauko]

Hi,

to use sv-comp nondet functions you need to run divine with the option --symbolic, which enables symbolic verification.

Moreover, you have a typo in the function name the proper name is VERIFIER_nondet_int(). Furthermore, you need to declare it as extern "C" not just extern.

Also probably you do not want to print nondet values since it would mean that you will print all the possible values of x.

[otis01329]

I made some changes after listening to your suggestions.

This is my c++ code.
############################
#include <iostream>
#include <assert.h>

using namespace std;

extern"C" int VERIFIER_nondet_int();

int main() {

int x = VERIFIER_nondet_int();
cout<<"x = "<<x<<endl;
assert(x==0);

}
############################
command:
divine check --symbolic --svcomp testcpp.cpp

or

divine check --symbolic testcpp.cpp

error message:
compiling testcpp.cpp
loading bitcode … LART … E: Propagating through unsupported operation in sym domain:

%add.ptr = getelementptr inbounds i8, i8* %3, i64 %vbase.offset, !dbg !60838

core dumped

Can you provide a C++ example that you can successfully execute divine4?
C++ code needs to include "VERIFIER_nondet_int()" and execute command.
Thanks.

[Henrich Lauko]

You still have the same problem. In DIVINE it is not possible to print nondeterministic value.

#include <cassert>

extern"C" int __VERIFIER_nondet_int();

int main() {
     int x = __VERIFIER_nondet_int();
     assert(x==0);
}

If you run divine check --symbolic test.cpp with above program divine succesuffuly terminates with following result:

  ...
  ASSUME (not (= var_0 #x00000000))
  (0) Assertion failed: x==0, file test.cpp, line 7.
  FAULT: 
  [0] FATAL: assertion failure in userspace

active stack:
  - symbol: void __dios::FaultBase::handler<__dios::Upcall<__dios::fs::VFS<__dios::ProcessManager<__dios::Fault<__dios::Scheduler<__dios::config::Base> > > > > >(_VM_Fault, _VM_Frame*, void (*)())
    location: /dios/include/dios/sys/fault.hpp:86
  - symbol: __dios_fault
    location: /dios/src/libc/sys/fault.c:14
  - symbol: __assert_fail
    location: /dios/src/libc/_PDCLIB/assert.c:21
  - symbol: main
    location: test.cpp:7
  - symbol: _start
    location: /dios/src/libc/sys/start.cpp:102
a report was written to test.report

DIVINE finds that there is a possibility to trigger assert at line 7.