From 623a87c132abec61b5c74a6a00a7b162073a6a8d Mon Sep 17 00:00:00 2001 From: boehmes Date: Thu, 27 Sep 2012 17:13:42 +0200 Subject: Boogie: new syntax for integer division and modulus: use div and mod instead of / and % --- Test/livevars/bla1.bpl | 2 +- Test/livevars/daytona_bug2_ioctl_example_1.bpl | 2 +- Test/livevars/daytona_bug2_ioctl_example_2.bpl | 2 +- Test/livevars/stack_overflow.bpl | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) (limited to 'Test/livevars') diff --git a/Test/livevars/bla1.bpl b/Test/livevars/bla1.bpl index 2854e5df..12ccc44a 100644 --- a/Test/livevars/bla1.bpl +++ b/Test/livevars/bla1.bpl @@ -471,7 +471,7 @@ function {:inline true} INT_NEQ(x:int, y:int) returns (bool) {x != y} function {:inline true} INT_ADD(x:int, y:int) returns (int) {x + y} function {:inline true} INT_SUB(x:int, y:int) returns (int) {x - y} function {:inline true} INT_MULT(x:int, y:int) returns (int) {x * y} -function {:inline true} INT_DIV(x:int, y:int) returns (int) {x / y} +function {:inline true} INT_DIV(x:int, y:int) returns (int) {x div y} function {:inline true} INT_LT(x:int, y:int) returns (bool) {x < y} function {:inline true} INT_ULT(x:int, y:int) returns (bool) {x < y} function {:inline true} INT_LEQ(x:int, y:int) returns (bool) {x <= y} diff --git a/Test/livevars/daytona_bug2_ioctl_example_1.bpl b/Test/livevars/daytona_bug2_ioctl_example_1.bpl index 1decba12..ae8ff08c 100644 --- a/Test/livevars/daytona_bug2_ioctl_example_1.bpl +++ b/Test/livevars/daytona_bug2_ioctl_example_1.bpl @@ -510,7 +510,7 @@ function {:inline true} INT_NEQ(x:int, y:int) returns (bool) {x != y} function {:inline true} INT_ADD(x:int, y:int) returns (int) {x + y} function {:inline true} INT_SUB(x:int, y:int) returns (int) {x - y} function {:inline true} INT_MULT(x:int, y:int) returns (int) {x * y} -function {:inline true} INT_DIV(x:int, y:int) returns (int) {x / y} +function {:inline true} INT_DIV(x:int, y:int) returns (int) {x div y} function {:inline true} INT_LT(x:int, y:int) returns (bool) {x < y} function {:inline true} INT_ULT(x:int, y:int) returns (bool) {x < y} function {:inline true} INT_LEQ(x:int, y:int) returns (bool) {x <= y} diff --git a/Test/livevars/daytona_bug2_ioctl_example_2.bpl b/Test/livevars/daytona_bug2_ioctl_example_2.bpl index 0b49364b..44e51827 100644 --- a/Test/livevars/daytona_bug2_ioctl_example_2.bpl +++ b/Test/livevars/daytona_bug2_ioctl_example_2.bpl @@ -521,7 +521,7 @@ function {:inline true} INT_NEQ(x:int, y:int) returns (bool) {x != y} function {:inline true} INT_ADD(x:int, y:int) returns (int) {x + y} function {:inline true} INT_SUB(x:int, y:int) returns (int) {x - y} function {:inline true} INT_MULT(x:int, y:int) returns (int) {x * y} -function {:inline true} INT_DIV(x:int, y:int) returns (int) {x / y} +function {:inline true} INT_DIV(x:int, y:int) returns (int) {x div y} function {:inline true} INT_LT(x:int, y:int) returns (bool) {x < y} function {:inline true} INT_ULT(x:int, y:int) returns (bool) {x < y} function {:inline true} INT_LEQ(x:int, y:int) returns (bool) {x <= y} diff --git a/Test/livevars/stack_overflow.bpl b/Test/livevars/stack_overflow.bpl index 242acd65..fae3e863 100644 --- a/Test/livevars/stack_overflow.bpl +++ b/Test/livevars/stack_overflow.bpl @@ -831,7 +831,7 @@ function {:inline true} INT_NEQ(x:int, y:int) returns (bool) {x != y} function {:inline true} INT_ADD(x:int, y:int) returns (int) {x + y} function {:inline true} INT_SUB(x:int, y:int) returns (int) {x - y} function {:inline true} INT_MULT(x:int, y:int) returns (int) {x * y} -function {:inline true} INT_DIV(x:int, y:int) returns (int) {x / y} +function {:inline true} INT_DIV(x:int, y:int) returns (int) {x div y} function {:inline true} INT_LT(x:int, y:int) returns (bool) {x < y} function {:inline true} INT_ULT(x:int, y:int) returns (bool) {x < y} function {:inline true} INT_LEQ(x:int, y:int) returns (bool) {x <= y} -- cgit v1.2.3