Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refactor writing to pointers #1531

Draft
wants to merge 9 commits into
base: master
Choose a base branch
from
Draft

Refactor writing to pointers #1531

Changes from 1 commit
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
9485208
Remove deadcode that catches `SetDomain.Unsupported`
karoliineh Jun 28, 2024
65e1ccc
Replace complicated set logic with simplified AD.fold
karoliineh Jun 28, 2024
87a979a
Make update_one case handling explicit
karoliineh Jun 28, 2024
c4d96e8
Assert that the set of lvals is not empty when written to
karoliineh Jul 1, 2024
c7199a0
Do not remove NullPtr-s from address sets
karoliineh Jul 1, 2024
7816bed
Add stdlib.h for correctly importing strtol
karoliineh Jul 1, 2024
7d87b35
Fix `17-per_elem_simp`: nowarn -> norace
karoliineh Jul 1, 2024
a30fbfc
Do not remove `UnknownPtr` from address set before running `reachable…
karoliineh Jul 1, 2024
6843784
Use `sem.null-pointer.dereference` option for writing as well
karoliineh Aug 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Do not remove UnknownPtr from address set before running `reachable… 
…_vars`
  • Loading branch information
@karoliineh
karoliineh committed Jul 1, 2024
commit a30fbfc3add97d40d400bce360f9cb821439f35e
10 changes: 3 additions & 7 deletions src/analyses/base.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1486,13 +1486,9 @@ struct
| Top -> Queries.Result.top q
| Bot -> Queries.Result.bot q (* TODO: remove *)
| Address a ->
let a' = AD.remove Addr.UnknownPtr a in (* run reachable_vars without unknown just to be safe: TODO why? *)
let addrs = reachable_vars ~ctx ctx.local [a'] in
let addrs' = List.fold_left (AD.join) (AD.empty ()) addrs in
if AD.may_be_unknown a then
AD.add UnknownPtr addrs' (* add unknown back *)
else
addrs'
[a]
|> reachable_vars ~ctx ctx.local
|> List.fold_left (AD.join) (AD.empty ())
| Int i ->
begin match Cilfacade.typeOf e with
| t when Cil.isPointerType t -> AD.of_int i (* integer used as pointer *)
Expand Down
Loading