diff --git a/regression/cbmc/ACSL/operators.c b/regression/cbmc/ACSL/operators.c new file mode 100644 index 00000000000..0c1628b5188 --- /dev/null +++ b/regression/cbmc/ACSL/operators.c @@ -0,0 +1,28 @@ +void boolean() +{ + __CPROVER_bool a, b; + __CPROVER_assert((a ≡ b) == (a == b), "≥"); + __CPROVER_assert((a ≢ b) == (a != b), "≢"); + __CPROVER_assert((a ⇒ b) == (!a || b), "⇒"); + __CPROVER_assert((a ⇔ b) == (a == b), "⇔"); + __CPROVER_assert((a ∧ b) == (a && b), "∧"); + __CPROVER_assert((a ∨ b) == (a || b), "∨"); + __CPROVER_assert((a ⊻ b) == (a != b), "⊻"); + __CPROVER_assert((¬ a) == (!a), "¬"); +} + +void relations() +{ + int a, b; + __CPROVER_assert((a ≥ b) == (a >= b), "≥"); + __CPROVER_assert((a ≤ b) == (a <= b), "≤"); + __CPROVER_assert((a ≡ b) == (a == b), "≥"); + __CPROVER_assert((a ≢ b) == (a != b), "≢"); + __CPROVER_assert((− a) == (-a), "−"); +} + +int main() +{ + boolean(); + relations(); +} diff --git a/regression/cbmc/ACSL/operators.desc b/regression/cbmc/ACSL/operators.desc new file mode 100644 index 00000000000..fbaf5072a5c --- /dev/null +++ b/regression/cbmc/ACSL/operators.desc @@ -0,0 +1,8 @@ +CORE +operators.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index d3eb466ddc4..05bc72cad31 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -180,7 +180,9 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr) typecheck_expr_unary_arithmetic(expr); else if(expr.id()==ID_not) typecheck_expr_unary_boolean(expr); - else if(expr.id()==ID_and || expr.id()==ID_or || expr.id()==ID_implies) + else if( + expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies || + expr.id() == ID_xor) typecheck_expr_binary_boolean(expr); else if(expr.id()==ID_address_of) typecheck_expr_address_of(expr); diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 5e8572e82b1..f06058bc621 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3815,7 +3815,7 @@ std::string expr2ct::convert_with_precedence( return convert_multi_ary(src, "||", precedence=4, false); else if(src.id()==ID_xor) - return convert_multi_ary(src, "^", precedence=7, false); + return convert_multi_ary(src, "!=", precedence = 9, false); else if(src.id()==ID_implies) return convert_binary(src, "==>", precedence=3, true); diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 539e8494b00..6627e7819ae 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -174,6 +174,7 @@ extern char *yyansi_ctext; %token TOK_EXISTS "exists" %token TOK_ACSL_FORALL "\\forall" %token TOK_ACSL_EXISTS "\\exists" +%token TOK_ACSL_LET "\\let" %token TOK_ARRAY_OF "array_of" %token TOK_CPROVER_BITVECTOR "__CPROVER_bitvector" %token TOK_CPROVER_FLOATBV "__CPROVER_floatbv" @@ -190,6 +191,7 @@ extern char *yyansi_ctext; %token TOK_CPROVER_ENSURES "__CPROVER_ensures" %token TOK_IMPLIES "==>" %token TOK_EQUIVALENT "<==>" +%token TOK_XORXOR "^^" %token TOK_TRUE "TRUE" %token TOK_FALSE "FALSE" %token TOK_REAL "__real__" @@ -775,9 +777,15 @@ logical_and_expression: { binary($$, $1, $2, ID_and, $3); } ; -logical_or_expression: +logical_xor_expression: logical_and_expression - | logical_or_expression TOK_OROR logical_and_expression + | logical_xor_expression TOK_XORXOR logical_and_expression + { binary($$, $1, $2, ID_xor, $3); } + ; + +logical_or_expression: + logical_xor_expression + | logical_or_expression TOK_OROR logical_xor_expression { binary($$, $1, $2, ID_or, $3); } ; diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 09125b12da8..a5e3e0c818c 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -1223,41 +1223,67 @@ __decltype { if(PARSER.cpp98 && "__CPROVER_requires" { loc(); return TOK_CPROVER_REQUIRES; } "__CPROVER_ensures" { loc(); return TOK_CPROVER_ENSURES; } -"\x22\x00" | +"\xe2\x88\x80" | "\\forall" { /* Non-standard, obviously. Found in ACSL syntax. */ loc(); return TOK_ACSL_FORALL; } -"\x22\x03" | +"\xe2\x88\x83" | "\\exists" { /* Non-standard, obviously. Found in ACSL syntax. */ loc(); return TOK_ACSL_EXISTS; } -"\x21\xD2" | + +"\\let" { /* Non-standard, obviously. Found in ACSL syntax. */ + loc(); return TOK_ACSL_LET; + } + +"\xe2\x87\x92" | "==>" { /* Non-standard, obviously. Found in Spec# and ACSL syntax. */ loc(); return TOK_IMPLIES; } -"\x21\xD4" | +"\xe2\x87\x94" | "<==>" { /* Non-standard, obviously. Found in Spec# and ACSL syntax. */ loc(); return TOK_EQUIVALENT; } -"\x22\x65" { /* Non-standard, obviously. Found in ACSL syntax. */ +"\xe2\x89\xa5" { /* Non-standard, obviously. Found in ACSL syntax. */ loc(); return TOK_GE; } -"\x22\x64" { /* Non-standard, obviously. Found in ACSL syntax. */ +"\xe2\x89\xa1" { /* Non-standard, obviously. Found in ACSL syntax. */ + loc(); return TOK_EQ; + } + +"\xe2\x89\xa2" { /* Non-standard, obviously. Found in ACSL syntax. */ + loc(); return TOK_NE; + } + +"\xe2\x89\xa4" { /* Non-standard, obviously. Found in ACSL syntax. */ loc(); return TOK_LE; } -"\x22\x27" { /* Non-standard, obviously. Found in ACSL syntax. */ +"\xe2\x88\xa7" { /* Non-standard, obviously. Found in ACSL syntax. */ loc(); return TOK_ANDAND; } -"\x22\x28" { /* Non-standard, obviously. Found in ACSL syntax. */ +"\xe2\x88\xa8" { /* Non-standard, obviously. Found in ACSL syntax. */ loc(); return TOK_OROR; } +"\xc2\xac" { /* Non-standard, obviously. Found in ACSL syntax. */ + loc(); return '!'; + } + +"\xe2\x8a\xbb" | +"^^" { /* Non-standard, obviously. Found in ACSL syntax. */ + loc(); return TOK_XORXOR; + } + +"\xe2\x88\x92" { /* Non-standard, obviously. Found in ACSL syntax. */ + loc(); return '-'; + } + "\\true" { /* Non-standard, obviously. Found in ACSL syntax. */ loc(); return TOK_TRUE; }