You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
While looking into how to parse single expressions, e.g. coming from a witness, I noticed how Goblint abuses Formatcil.cExp for that. Despite not being intended for user input parsing, it cannot parse logical operators:
glob == 0 || glob == 1 doesn't parse at all.
glob == 1 && i == 11 parses, but even more confusingly returns an incorrect AST: &(==(Lval(Var(glob, NoOffset)), Const(Int(1,int,1))),==(AddrOf(Var(i, NoOffset)), Const(Int(11,int,11)))). Since it doesn't recognize && as a token, this expression is parsed instead as glob == 1 &(& i == 11) (with a bitwise and, and address of).
This misparsing is very confusing because instead of immediate problems, it crashes Goblint in surprising ways: exception IntDomain.IncompatibleIKinds("ikinds int and unsigned long are incompatible. Values: (1) and (1)").
The use of Formatcil.cExp for semantic search in Goblint is quite liberal with the use of catch-all try blocks, which quietly hides both problems.
The text was updated successfully, but these errors were encountered:
While looking into how to parse single expressions, e.g. coming from a witness, I noticed how Goblint abuses
Formatcil.cExp
for that. Despite not being intended for user input parsing, it cannot parse logical operators:glob == 0 || glob == 1
doesn't parse at all.glob == 1 && i == 11
parses, but even more confusingly returns an incorrect AST:&(==(Lval(Var(glob, NoOffset)), Const(Int(1,int,1))),==(AddrOf(Var(i, NoOffset)), Const(Int(11,int,11))))
. Since it doesn't recognize&&
as a token, this expression is parsed instead asglob == 1 &(& i == 11)
(with a bitwise and, and address of).This misparsing is very confusing because instead of immediate problems, it crashes Goblint in surprising ways:
exception IntDomain.IncompatibleIKinds("ikinds int and unsigned long are incompatible. Values: (1) and (1)")
.The use of
Formatcil.cExp
for semantic search in Goblint is quite liberal with the use of catch-alltry
blocks, which quietly hides both problems.The text was updated successfully, but these errors were encountered: