Skip to content

Commit

Permalink
replaced the use of type Cell with type Foo in these tests
Browse files Browse the repository at this point in the history
  • Loading branch information
shazqadeer committed May 4, 2024
1 parent 50a6de9 commit dbe2918
Show file tree
Hide file tree
Showing 4 changed files with 21 additions and 21 deletions.
12 changes: 6 additions & 6 deletions Test/monomorphize/issue-358.bpl
Original file line number Diff line number Diff line change
Expand Up @@ -2,16 +2,16 @@
// RUN: %diff "%s.expect" "%t"
// test for use of type synonyms

datatype Cell<T> { Mk(x: T) }
datatype Foo<T> { Mk(x: T) }

function foo<T>(): Cell T;
function foo<T>(): Foo T;

type Cell_int = Cell int;
type Cell_bool = Cell bool;
type Foo_int = Foo int;
type Foo_bool = Foo bool;

procedure p() {
var x: Cell_int;
var y: Cell_bool;
var x: Foo_int;
var y: Foo_bool;
x := Mk(1);
y := Mk(false);
assert x->x == 1;
Expand Down
8 changes: 4 additions & 4 deletions Test/monomorphize/issue-364.bpl
Original file line number Diff line number Diff line change
Expand Up @@ -2,15 +2,15 @@
// RUN: %diff "%s.expect" "%t"
// test for use of type synonyms

datatype Cell<T> { Cell(x: T) }
datatype Foo<T> { Foo(x: T) }

function foo<T>(): Cell T;
function foo<T>(): Foo T;

datatype Some { Some(x: int) }

type MyT = Some;

procedure p() {
var c1: Cell MyT;
var c2: Cell Some;
var c1: Foo MyT;
var c2: Foo Some;
}
8 changes: 4 additions & 4 deletions Test/monomorphize/monomorphize5.bpl
Original file line number Diff line number Diff line change
Expand Up @@ -2,20 +2,20 @@
// RUN: %diff "%s.expect" "%t"
// Issue #359

datatype Cell<T> { Mk(x: T) }
datatype Foo<T> { Mk(x: T) }


function foo<T>(): Cell T;
function foo<T>(): Foo T;

procedure p() {
var x: Cell int;
var x: Foo int;
x := Mk(1);
assume {:print "x=", x} true;
assert x->x == 1;
}

procedure q() {
var x: Cell int;
var x: Foo int;
x := Mk(1);
assume {:print "x=", x} true;
assert x->x == 0;
Expand Down
14 changes: 7 additions & 7 deletions Test/monomorphize/monomorphize6.bpl
Original file line number Diff line number Diff line change
Expand Up @@ -2,24 +2,24 @@
// RUN: %diff "%s.expect" "%t"
// Issue #361

datatype Cell<T> { Cell(x: T) }
datatype Foo<T> { Foo(x: T) }


datatype OtherCell<T> { OtherCell(x: T) }
datatype OtherFoo<T> { OtherFoo(x: T) }


function foo<T>(): Cell T;
function foo<T>(): Foo T;

procedure p() {
var x: Cell (OtherCell int);
x := Cell(OtherCell(1));
var x: Foo (OtherFoo int);
x := Foo(OtherFoo(1));
assume {:print "x=", x} true;
assert x->x->x == 1;
}

procedure q() {
var x: Cell (OtherCell int);
x := Cell(OtherCell(1));
var x: Foo (OtherFoo int);
x := Foo(OtherFoo(1));
assume {:print "x=", x} true;
assert x->x->x == 0;
}

0 comments on commit dbe2918

Please sign in to comment.