[clang-cpp-frontend] support rvalue references C++11

[XLiZHI]

This PR adds new node support in the clang C++ frontend RValuereference

A new OM was established: std::move

The example code is as follows:

#include <assert.h>
#include <utility>

int main() 
{
    int a = 10;

    assert(std::move(a) == 10);

    int &&rref = std::move(a);

    assert(rref == 10);

    rref = 3;

    assert(rref == 3);

    return 0;
}

esbmc main.cpp --cppstd 11

Goto functions:

move (c:@N@std@F@move<#&I>#S0_#):
        // 20 file utility line 61 column 3 function move
        RETURN: (signed int *)((signed int)t)
        // 21 file utility line 62 column 1 function move
        END_FUNCTION // move
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

main (c:@F@main#):
        // 22 file main2.cpp line 6 column 5 function main
        signed int a;
        // 23 file main2.cpp line 6 column 5 function main
        a=10;
        // 24 file main2.cpp line 8 column 12 function main
        signed int * return_value$_move$1;
        // 25 file main2.cpp line 8 column 12 function main
        FUNCTION_CALL:  return_value$_move$1=move(&a)
        // 26 file main2.cpp line 8 column 5 function main
        ASSERT *return_value$_move$1 == 10 // assertion std::move(a) == 10   //turn std::move(a) into *std::move(a)
        // 27 file main2.cpp line 8 column 5 function main
        IF !(*return_value$_move$1 == 10) THEN GOTO 1
        // 28 file main2.cpp line 8 column 5 function main
        0;

        // 29 file main2.cpp line 10 column 5 function main
     1: signed int * rref;
        // 30 file main2.cpp line 10 column 18 function main
        signed int * return_value$_move$2;
        // 31 file main2.cpp line 10 column 18 function main
        FUNCTION_CALL:  return_value$_move$2=move(&a)
        // 32 file main2.cpp line 10 column 5 function main
        rref=(signed int *)return_value$_move$2;
        // 33 file main2.cpp line 12 column 5 function main
        ASSERT (signed int)(*rref) == 10 // assertion rref == 10  //turn rref into *rref
        // 34 file main2.cpp line 12 column 5 function main
        IF !((signed int)(*rref) == 10) THEN GOTO 2
        // 35 file main2.cpp line 12 column 5 function main
        0;

        // 36 file main2.cpp line 14 column 5 function main
     2: *rref=3;                                                //turn rref into *rref
        // 37 file main2.cpp line 16 column 5 function main
        ASSERT (signed int)(*rref) == 3 // assertion rref == 3  //turn rref into *rref
        // 38 file main2.cpp line 16 column 5 function main
        IF !((signed int)(*rref) == 3) THEN GOTO 3
        // 39 file main2.cpp line 16 column 5 function main
        0;

        // 40 file main2.cpp line 18 column 5 function main
     3: RETURN: 0
        // 41 file main2.cpp line 19 column 1 function main
        END_FUNCTION // main
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[fbrausse]

I just have questions about the C++ OMs: As they don't appear to contain ESBMC-specific parts, could they be removed?

[fbrausse]

1. Do we need this new header? What happens if we use the one from the C++ library installed on the system?
2. Please consider using #pragma once (our Clang frontend supports this) or to rename the include guard to have an __ESBMC_ prefix.

[XLiZHI]

What happens if we use the one from the C++ library installed on the system?

I tried it and our frontend complained about it. It's not just this method in the standard library, there are a lot of other methods that our frontend doesn't support yet. I thought maybe we could handle it this way for now to avoid more changes.

Please consider using #pragma once (our Clang frontend supports this) or to rename the include guard to have an _ESBMC prefix.

Yes, I'll change it.

[lucasccordeiro]

Thanks for submitting this PR, @XLiZHI.