Search code examples
c++z3

Taking the address of a temporary object of type 'z3::expr'


I want to access the address of a z3::expr inside a z3::expr_vector.

z3::context ctx;
z3::expr_vector x(c);

// populate x with some push_backs ...

// access the address of the first element: 
z3::expr* t1 = &x[0]; // -Waddress-of-temporary: Taking the address of a temporary object 
                      // of type 'z3::expr' 

I took a look at this question, but that only talks about the z3::expr's constructor.

If I use a std::vector<z3_expr> instead it works:

std::vector<z3::expr> x2;
...
z3::expr* t2 = &x2[0]; // This works

Is this intended, i.e. is the address not available to the user? Should I maintain an std::vector<z3::expr> instead?

Additionally, if I want to create a z3::expr* conditionally, how does go about it?

z3::expr* e;
if (some condition) {
    e = &(ctx.bv_const("s", 1)); // this gives the same compiler warning.
} else {
    e = &(ctx.bv_const("s", 1)); // as does this.
}

// use e

Some pointers regarding the correct usage would be really helpful.


Solution

  • z3::expr_vector is a typedef for z3::ast_vector_tpl, whose operator[] returns elements by value, ie a temporary copy. So your z3::expr_vector example fails, because it is illegal to take the memory address of a temporary.

    AFAICS, ast_vector_tpl does not have any methods that return access to its elements by reference/pointer, only by value. Neither does its iterator (so, something like z3::expr* t1 = &*(x.begin()); would not work, either).

    std::vector, on the other hand, has an operator[] (and an iterator with an operator*) that returns access to its elements by reference instead, which is why your std::vector example works.