Skip to content

Formatcil doesn't support || and && operators #94

@sim642

Description

@sim642

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions