From 08e1dc93d185e221b65bd59ccc167526937ee4d4 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 28 May 2014 16:32:14 +0100 Subject: Removed old test infrastructure files except for ./AbsHoudini/ ./doomed/ ./z3api/ ./test17/ because their conversion to lit incomplete. --- Test/test20/Answer | 191 ------------------------------------------------ Test/test20/runtest.bat | 26 ------- 2 files changed, 217 deletions(-) delete mode 100644 Test/test20/Answer delete mode 100644 Test/test20/runtest.bat (limited to 'Test/test20') diff --git a/Test/test20/Answer b/Test/test20/Answer deleted file mode 100644 index 7e7af57b..00000000 --- a/Test/test20/Answer +++ /dev/null @@ -1,191 +0,0 @@ -TypeDecls0.bpl(22,5): Error: more than one declaration of type name: C -TypeDecls0.bpl(15,12): Error: more than one declaration of type variable: a -TypeDecls0.bpl(16,18): Error: more than one declaration of type variable: a -TypeDecls0.bpl(20,17): Error: type variable must occur in map arguments: b -TypeDecls0.bpl(24,9): Error: type constructor received wrong number of arguments: C -TypeDecls0.bpl(26,9): Error: undeclared type: A0 -TypeDecls0.bpl(27,9): Error: undeclared type: F -TypeDecls0.bpl(30,9): Error: type constructor received wrong number of arguments: E -TypeDecls0.bpl(32,9): Error: type constructor received wrong number of arguments: E -TypeDecls0.bpl(34,9): Error: type constructor received wrong number of arguments: E -TypeDecls0.bpl(40,11): Error: type constructor received wrong number of arguments: E -TypeDecls0.bpl(40,13): Error: type constructor received wrong number of arguments: E -12 name resolution errors detected in TypeDecls0.bpl -TypeDecls1.bpl(9,13): Error: invalid type for argument 0 in map select: int (expected: [b]a) -TypeDecls1.bpl(15,25): Error: right-hand side in map store with wrong type: int (expected: bool) -TypeDecls1.bpl(21,36): Error: invalid type for argument 0 in map select: [c]c (expected: [b]a) -TypeDecls1.bpl(23,13): Error: invalid type for argument 0 in map select: [[b]a]bool (expected: [b]a) -4 type checking errors detected in TypeDecls1.bpl -Prog0.bpl(19,10): Error: type variable must occur in map arguments: a -Prog0.bpl(31,27): Error: more than one declaration of type variable: beta -Prog0.bpl(34,22): Error: undeclared type: alpha -Prog0.bpl(35,35): Error: undeclared type: alpha -4 name resolution errors detected in Prog0.bpl -Prog1.bpl(20,11): Error: invalid type for argument 0 in map select: int (expected: ref) -Prog1.bpl(21,14): Error: invalid type for argument 1 in map select: int (expected: Field a) -Prog1.bpl(22,17): Error: invalid argument types (bool and int) to binary operator >= -3 type checking errors detected in Prog1.bpl -Prog2.bpl(8,14): Error: trigger does not mention alpha, which does not occur in variables types either -1 type checking errors detected in Prog2.bpl -PolyFuns0.bpl(25,33): Error: invalid type for argument 1 in application of fieldValue: ref (expected: Field a) -PolyFuns0.bpl(42,18): Error: invalid type for argument 1 in application of lessThan: bool (expected: a) -PolyFuns0.bpl(43,43): Error: invalid type for argument 1 in application of lessThan: b (expected: a) -PolyFuns0.bpl(55,55): Error: invalid argument types ([Field c]a and [Field d]d) to binary operator == -4 type checking errors detected in PolyFuns0.bpl -PolyFuns1.bpl(12,9): Error: invalid type for argument 0 in application of F: [c]c (expected: [b]a) -PolyFuns1.bpl(13,9): Error: invalid type for argument 0 in map select: [c]c (expected: [b]a) -PolyFuns1.bpl(14,31): Error: invalid type for argument 0 in application of F: [c]c (expected: [b]a) -PolyFuns1.bpl(15,31): Error: invalid type for argument 0 in map select: [c]c (expected: [b]a) -PolyFuns1.bpl(19,55): Error: invalid argument types ([Field c]a and [Field d]d) to binary operator == -PolyFuns1.bpl(20,55): Error: invalid argument types ([Field c]a and [Field d]d) to binary operator == -PolyFuns1.bpl(30,11): Error: invalid type for argument 0 in call to Uhu:
[Field dd]dd (expected: [Field c]a) -PolyFuns1.bpl(31,15): Error: invalid type for argument 1 in call to Uhu: [Field cc]T (expected: [Field d]d) -PolyFuns1.bpl(32,12): Error: invalid argument types ([Field cc]T and
[Field dd]dd) to binary operator == -PolyFuns1.bpl(33,12): Error: invalid argument types (
[Field dd]dd and [Field cc]T) to binary operator == -PolyFuns1.bpl(35,15): Error: invalid type for argument 1 in call to Uhu: [Field T]ee (expected: [Field d]d) -PolyFuns1.bpl(43,11): Error: invalid argument types ([a,a]int and [b,int]int) to binary operator == -PolyFuns1.bpl(44,11): Error: invalid argument types ([b,int]int and [int,c]int) to binary operator == -PolyFuns1.bpl(45,11): Error: invalid argument types ([a,a]int and [int,c]int) to binary operator == -PolyFuns1.bpl(52,11): Error: invalid argument types ([a,a,b]int and [a,b,b]int) to binary operator == -PolyFuns1.bpl(59,54): Error: invalid argument types (Field b and NagainCtor b) to binary operator == -16 type checking errors detected in PolyFuns1.bpl -PolyProcs0.bpl(13,16): Error: invalid type for argument 0 in map select: Field b (expected: ref) -PolyProcs0.bpl(13,19): Error: invalid type for argument 1 in map select: ref (expected: Field a) -PolyProcs0.bpl(23,30): Error: invalid type for argument 1 in call to FieldAccess: Field int (expected: ref) -PolyProcs0.bpl(23,34): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b) -PolyProcs0.bpl(27,7): Error: invalid type for out-parameter 0 in call to FieldAccess: bool (expected: int) -PolyProcs0.bpl(28,35): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b) -6 type checking errors detected in PolyProcs0.bpl -TypeSynonyms0.bpl(13,5): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving) -TypeSynonyms0.bpl(14,5): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving) -TypeSynonyms0.bpl(16,5): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving) -TypeSynonyms0.bpl(26,10): Error: type constructor received wrong number of arguments: Field -TypeSynonyms0.bpl(27,10): Error: type synonym received wrong number of arguments: Set -TypeSynonyms0.bpl(30,10): Error: type variable must occur in map arguments: a -6 name resolution errors detected in TypeSynonyms0.bpl -TypeSynonyms1.bpl(48,8): Error: invalid type for argument 0 in application of h: [b,b,[b2,b,int]int]int (expected: nested2) -1 type checking errors detected in TypeSynonyms1.bpl - -Boogie program verifier finished with 1 verified, 0 errors - -type Set a = [a]bool; - -type Field _; - -type Heap = [ref,Field a]a; - -type notAllParams a b = Field b; - -type Cyclic0 = Cyclic1; - -type Cyclic1 = Cyclic0; - -type AlsoCyclic a = [AlsoCyclic b]int; - -type C _ _; - -type C2 b a = C a b; - -function f(C int bool) : int; - -const x: C2 bool int; - -const y: Field int bool; - -const z: Set int bool; - -const d: [notAllParams a b]int; - -type ref; -(10,-1): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving) -(12,-1): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving) -(14,-1): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving) -(24,8): Error: type constructor received wrong number of arguments: Field -(26,8): Error: type synonym received wrong number of arguments: Set -(28,8): Error: type variable must occur in map arguments: a -6 name resolution errors detected in TypeSynonyms0.bpl - -type Set a = [a]bool; - -function union(x: Set a, y: Set a) : Set a; - -axiom (forall x: Set a, y: Set a, z: a :: (x[z] || y[z]) == union(x, y)[z]); - -const intSet0: Set int; - -axiom (forall x: int :: intSet0[x] == (x == 0 || x == 2 || x == 3)); - -const intSet1: Set int; - -axiom (forall x: int :: intSet1[x] == (x == -5 || x == 3)); - -procedure P(); - - - -implementation P() -{ - assert (forall x: int :: union(intSet0, intSet1)[x] == (x == -5 || x == 0 || x == 2 || x == 3)); -} - - - -type Set a = [a]bool; - -function union(x: Set a, y: Set a) : Set a; - -axiom (forall x: Set a, y: Set a, z: a :: x[z] || y[z] <==> union(x, y)[z]); - -const intSet0: Set int; - -axiom (forall x: int :: intSet0[x] <==> x == 0 || x == 2 || x == 3); - -const intSet1: Set int; - -axiom (forall x: int :: intSet1[x] <==> x == -5 || x == 3); - -procedure P(); - - - -implementation P() -{ - assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == -5 || x == 0 || x == 2 || x == 3); -} - - - -Boogie program verifier finished with 0 verified, 0 errors -PolyPolyPoly.bpl(14,26): Error: invalid argument types ([]? and []C a) to binary operator == -PolyPolyPoly.bpl(17,23): Error: invalid argument types ([]? and []C a) to binary operator == -PolyPolyPoly.bpl(23,57): Error: invalid type for argument 1 in map select: b (expected: a) -3 type checking errors detected in PolyPolyPoly.bpl -PolyPolyPoly2.bpl(7,8): Warning: type parameter a is ambiguous, instantiating to int -PolyPolyPoly2.bpl(9,8): Warning: type parameter a is ambiguous, instantiating to [arg0]res -PolyPolyPoly2.bpl(13,8): Warning: type parameter a is ambiguous, instantiating to bv0 -PolyPolyPoly2.bpl(13,15): Warning: type parameter a is ambiguous, instantiating to bv0 -PolyPolyPoly2.bpl(13,27): Warning: type parameter a is ambiguous, instantiating to bv17 -PolyPolyPoly2.bpl(14,8): Warning: type parameter a is ambiguous, instantiating to bv17 -PolyPolyPoly2.bpl(14,15): Warning: type parameter a is ambiguous, instantiating to bv0 -PolyPolyPoly2.bpl(24,7): Warning: type parameter a is ambiguous, instantiating to int -PolyPolyPoly2.bpl(33,3): Warning: type parameter a is ambiguous, instantiating to int -PolyPolyPoly2.bpl(34,3): Warning: type parameter a is ambiguous, instantiating to int - -Boogie program verifier finished with 0 verified, 0 errors -ProcParamReordering.bpl(15,15): Error: mismatched type of in-parameter in implementation P: y (named b in implementation) -ProcParamReordering.bpl(17,15): Error: mismatched number of type parameters in procedure implementation: P -2 type checking errors detected in ProcParamReordering.bpl -ParallelAssignment.bpl(19,2): Error: mismatched types in assignment command (cannot assign bool to int) -ParallelAssignment.bpl(20,4): Error: invalid type for argument 0 in map assignment: bool (expected: int) -ParallelAssignment.bpl(22,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: z -3 type checking errors detected in ParallelAssignment.bpl -ParallelAssignment2.bpl(11,7): Error: number of left-hand sides does not match number of right-hand sides -ParallelAssignment2.bpl(12,9): Error: variable a is assigned more than once in parallel assignment -2 name resolution errors detected in ParallelAssignment2.bpl -Coercions.bpl(13,8): Error: int cannot be coerced to E [a]int -Coercions.bpl(15,8): Error: C cannot be coerced to D -Coercions.bpl(17,9): Error: int cannot be coerced to D -Coercions.bpl(18,9): Error: int cannot be coerced to E int -4 type checking errors detected in Coercions.bpl - -Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/test20/runtest.bat b/Test/test20/runtest.bat deleted file mode 100644 index 0e607a1f..00000000 --- a/Test/test20/runtest.bat +++ /dev/null @@ -1,26 +0,0 @@ -@echo off -setlocal - -set BGEXE=..\..\Binaries\Boogie.exe -rem set BGEXE=mono ..\..\Binaries\Boogie.exe - -%BGEXE% %* /noVerify TypeDecls0.bpl -%BGEXE% %* /noVerify TypeDecls1.bpl -%BGEXE% %* /noVerify Prog0.bpl -%BGEXE% %* /noVerify Prog1.bpl -%BGEXE% %* /noVerify Prog2.bpl -%BGEXE% %* /noVerify PolyFuns0.bpl -%BGEXE% %* /noVerify PolyFuns1.bpl -%BGEXE% %* /noVerify PolyProcs0.bpl -%BGEXE% %* /noVerify TypeSynonyms0.bpl -%BGEXE% %* /noVerify TypeSynonyms1.bpl -%BGEXE% %* TypeSynonyms2.bpl -%BGEXE% %* /noVerify /print:- /env:0 TypeSynonyms0.bpl -%BGEXE% %* /noVerify /print:- /env:0 /printDesugared TypeSynonyms2.bpl -%BGEXE% %* /noVerify PolyPolyPoly.bpl -%BGEXE% %* /noVerify PolyPolyPoly2.bpl -%BGEXE% %* /noVerify ProcParamReordering.bpl -%BGEXE% %* /noVerify ParallelAssignment.bpl -%BGEXE% %* /noVerify ParallelAssignment2.bpl -%BGEXE% %* /noVerify Coercions.bpl -%BGEXE% %* /noVerify EmptySeq.bpl -- cgit v1.2.3