C++ Support For Operator Overloading

[zhanghongce]

It seems that CBMC supports operator overloading according to Supported Language Features. However when I tried the following example:

//FILE: /home/hongce/sysClearn/sysCVerif/testop.cpp
#include <cassert>

class t1{
    public:
        t1 (int n) :value(n) {}
    public:
        int value;
        int operator[](int n) { return n*value; }
        
};

int operator+(t1 left, int right) {return left.value+right;}

int main()
{
    t1 t(10);
    int t_1 = t + 5;
    int t_2 = t[5];
    assert(t_1 == 15);
    assert(t_2 == 50);
    return 0;
}

This is the error.

$ ~/cbmc-src/cbmc/src/cbmc/cbmc testop.cpp
CBMC version 5.7 64-bit x86_64 linux
Parsing testop.cpp
Converting
Type-checking testop
file testop.cpp line 18 function main: operator '+' not defined for types 'class' and 'int'
CONVERSION ERROR

Even after changing addition overloading as the member of class t1, it does not work.
Mysteriously the index operator works, if I remove the addition overloading staffs.

Does anyone know what is the problem?

[peterschrammel]

Hi,
can you please try the version in https://github.com/peterschrammel/cbmc, branch systemc?
Most of the operator overloading issues have been solved there, but have not yet made their way into the master branch.
Let me know whether this solves the problem for you (ignore the extended debug output that is currently produced in that version).
Thanks,
Peter

[zhanghongce]

Hi,
Thank you for your help! It works!

Best,
Hongce

[tautschnig]

May I suggest to leave this issue open for the time being and close it via a pull request once @peterschrammel finds time to submit his work for inclusion into master?

[zhanghongce]

@peterschrammel Sorry to bother again! I found that branch rather useful. Besides operator overloading, it has a better support of template than the master branch as well. But I found a strange bug. Here is the C++ code.

template <class T>
class sc_signal
{
public:
    T data;
    sc_signal(){}
    sc_signal(const char *p) {}
    T read() {return data;}
    void write(const T &d) {data = d;}
};


struct rbm
{

   sc_signal<unsigned int>  data_out;   //<L1>

   sc_signal<bool>   done;  // <L2>

   sc_signal<bool> conf_done;

   void config();

   rbm()
   {

   }

};


void rbm::config()
{
   do {
         conf_done.write(true);
         __CPROVER_assert( conf_done.data == true , "abc");
    } while ( !conf_done.read() );
}

int main()
{
    rbm IMPL;
    IMPL.config();

    return 0;
}

From my understanding, the assertion should pass, because conf.data has been set to true by the previous conf_done.write(true). However, the assertion will fail.

Mysteriously, if I remove either Line L1 or L2, it will pass.

The master branch won't even accept the code. It will complain "identifier this not found".

[peterschrammel]

Not sure why this happens, @zhanghongce. I'll investigate this asap.