Skip to content

Commit

Permalink
Fix null ref on access of Entry[] contents (#5947)
Browse files Browse the repository at this point in the history
Co-authored-by: jfleisher <jofleish@microsoft.com>
  • Loading branch information
fleisherdev and jfleisher authored Apr 6, 2022
1 parent bd70c79 commit ac2523a
Showing 1 changed file with 6 additions and 5 deletions.
11 changes: 6 additions & 5 deletions src/api/dotnet/NativeFuncInterp.cs
Original file line number Diff line number Diff line change
Expand Up @@ -85,13 +85,14 @@ internal NativeFuncInterp(NativeContext ctx, NativeModel mdl, Z3_func_decl decl,

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);
Expand Down

0 comments on commit ac2523a

Please sign in to comment.