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

Fix null ref on access of Entry[] contents (#5947)

Browse source 
Co-authored-by: jfleisher <jofleish@microsoft.com>
This commit is contained in:
fleisherdev 2022-04-05 23:37:51 -04:00 • committed by GitHub
parent bd70c79b25
commit ac2523af82
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 6 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/api/dotnet/NativeFuncInterp.cs
View file

@ -85,13 +85,14 @@ namespace Microsoft.Z3
for (uint j = 0; j < numEntries; ++j)
{
var entry = Native.Z3_func_interp_get_entry(nCtx, fi, j);
Native.Z3_func_entry_inc_ref(nCtx, entry);
var ntvEntry = Native.Z3_func_interp_get_entry(nCtx, fi, j);
Entries[j] = new Entry();
Native.Z3_func_entry_inc_ref(nCtx, ntvEntry);
Entries[j].Arguments = new Z3_ast[numArgs];
for (uint i = 0; i < numArgs; ++i)
Entries[j].Arguments[i] = Native.Z3_func_entry_get_arg(nCtx, entry, i);
Entries[j].Result = Native.Z3_func_entry_get_value(nCtx, entry);
Native.Z3_func_entry_dec_ref(nCtx, entry);
Entries[j].Arguments[i] = Native.Z3_func_entry_get_arg(nCtx, ntvEntry, i);
Entries[j].Result = Native.Z3_func_entry_get_value(nCtx, ntvEntry);
Native.Z3_func_entry_dec_ref(nCtx, ntvEntry);
}
Native.Z3_func_interp_dec_ref(nCtx, fi);