mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

add stub for #2522

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-08 09:54:07 -07:00
parent 7e174f50c1
commit 27765ee0f4
1 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/api/java/Expr.java
View file

@ -1290,6 +1290,22 @@ public class Expr extends AST
return Native.getString(getContext().nCtx(), getNativeObject()); return Native.getString(getContext().nCtx(), getNativeObject());
} }
/**
* TBD: sketch for #2522, 'Pointer' seems deprecated and instead
* approach seems to be around Set/Get CharArrayRegion and updating Native.cpp
* code generation to produce the char[].
*
public char[] getNativeString()
{
Native.IntPtr len = new Native.IntPtr();
long s = Native.getLstring(getContext().nCtx(), getNativeObject(), len);
char[] result = new char[len.value];
Pointer ptr = Pointer.createConstant(s);
for (int i = 0; i < len.value; ++i) result[i] = ptr.getChar(i);
return result;
}
*/
/** /**
* Check whether expression is a concatenation * Check whether expression is a concatenation
* @return a boolean * @return a boolean