-
Notifications
You must be signed in to change notification settings - Fork 84
Labels
good first issuesv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnessestesting
Milestone
Description
@karoliineh found that our SV-COMP valid-memsafety verdict is impacted by inserting a __goblint_check
into the program.
That is supposed to not impact the analysis at all (only output), so this behavior is wrong.
The offending code is here:
analyzer/src/analyses/memLeak.ml
Lines 230 to 245 in 153ce28
| Assert { exp; _ } -> | |
begin match man.ask (Queries.EvalInt exp) with | |
| a when Queries.ID.is_bot a -> M.warn ~category:Assert "assert expression %a is bottom" d_exp exp | |
| a -> | |
begin match Queries.ID.to_bool a with | |
| Some true -> () | |
| Some false -> | |
(* If we know for sure that the expression in "assert" is false => need to check for memory leaks *) | |
warn_for_multi_threaded_due_to_abort man; | |
check_for_mem_leak man | |
| None -> | |
warn_for_multi_threaded_due_to_abort man; | |
check_for_mem_leak man ~assert_exp_imprecise:true ~exp:(Some exp) | |
end | |
end; | |
state |
In particular, it should probably only be handled when
Assert
has refine = true
or something.karoliineh
Metadata
Metadata
Assignees
Labels
good first issuesv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnessestesting