Together with #1450, @karoliineh found SV-COMP no-overflow tasks where the abortUnless analysis from #875 does help us. Without it, we learn nothing from assume_abort_if_not conditions which are often used to assume bounds on variables that are key to proving overflow-freedom.
We did some quick benchmarks and it could be worth adding abortUnless to our svcomp conf, however it causes a lot of Not_found crashes from witness generation.
Specifically during combine_env:
|
let combine_env ctx lval fexp f args fc au f_ask = |
|
if au then ( |
|
(* Assert before combine_assign, so if variables in `arg` are assigned to, asserting doesn't unsoundly yield bot *) |
|
(* See test 62/03 *) |
|
match args with |
|
| [arg] -> ctx.emit (Events.Assert arg) |
|
| _ -> () |
|
); |
|
false |
There's probably some issue with emitting events from
combine_env, but before
combine_assign.
Together with #1450, @karoliineh found SV-COMP no-overflow tasks where the abortUnless analysis from #875 does help us. Without it, we learn nothing from
assume_abort_if_notconditions which are often used to assume bounds on variables that are key to proving overflow-freedom.We did some quick benchmarks and it could be worth adding abortUnless to our svcomp conf, however it causes a lot of
Not_foundcrashes from witness generation.Specifically during
combine_env:analyzer/src/analyses/abortUnless.ml
Lines 51 to 59 in 5cd8650
There's probably some issue with emitting events from
combine_env, but beforecombine_assign.