CODEWITHSUNDEEP
c++z3
harishankarv
harishankarv

Reputation: 338

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.

Upvotes: 0

Views: 162

Answers (1)

Remy Lebeau
Remy Lebeau

Reputation: 595402

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.

Upvotes: 2

Related Questions