Skip to content

Check cast safety in base invariant_fallback #1821

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

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Check cast safety in base invariant_fallback #1821

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f3da494
Add test 29-svcomp/37-weaver-invariant-cast (issue #1782)
sim642 Sep 5, 2025
56445a1
Check cast safety in base invariant_fallback (closes #1782)
sim642 Sep 5, 2025
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
8 changes: 7 additions & 1 deletion src/analyses/baseInvariant.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -237,7 +237,13 @@ struct
let switchedOp = function Lt -> Gt | Gt -> Lt | Le -> Ge | Ge -> Le | x -> x in (* a op b <=> b (switchedOp op) b *)
match exp with
(* Since we handle not only equalities, the order is important *)
| BinOp(op, Lval x, rval, typ) -> helper op x (VD.cast (Cilfacade.typeOfLval x) (eval_rv ~man st rval)) tv
| BinOp(op, Lval x, rval, typ) ->
let v = eval_rv ~man st rval in
let x_type = Cilfacade.typeOfLval x in
if VD.is_dynamically_safe_cast x_type (Cilfacade.typeOf rval) v then
helper op x (VD.cast x_type v) tv
else
`NotUnderstood
| BinOp(op, rval, Lval x, typ) -> derived_invariant (BinOp(switchedOp op, Lval x, rval, typ)) tv
| BinOp(op, CastE (t1, c1), CastE (t2, c2), t) when (op = Eq || op = Ne) && typeSig t1 = typeSig t2 && VD.is_statically_safe_cast t1 (Cilfacade.typeOf c1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf c2)
-> derived_invariant (BinOp (op, c1, c2, t)) tv
Expand Down
17 changes: 17 additions & 0 deletions tests/regression/29-svcomp/37-weaver-invariant-cast.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
// PARAM: --enable ana.int.interval --set ana.activated[+] abortUnless
#include <goblint.h>

extern void abort(void);
void assume_abort_if_not(int cond) {
if(!cond) {abort();}
}

int main() {
int n_update;

assume_abort_if_not(n_update >= 0);
assume_abort_if_not(n_update <= ( 4294967295UL / sizeof (char)));

__goblint_check(1); // reachable
return 0;
}
Loading