From b582b8afe8fa3316eac24c878197a04c55336d55 Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Fri, 16 Jul 2021 10:33:39 +0200 Subject: [PATCH 1/2] Reinstate History.pvl Ensure RandomizedIf introduces random methods properly (call them with a "this" argument, and generate final methods). Also ensure any recursive calls generated by left_merge in CheckProcessAlgebra have a this argument. --- examples/histories/History.pvl | 12 ++---------- .../java/vct/col/rewrite/CheckProcessAlgebra.java | 2 +- src/main/java/vct/col/rewrite/RandomizedIf.java | 5 +++-- 3 files changed, 6 insertions(+), 13 deletions(-) diff --git a/examples/histories/History.pvl b/examples/histories/History.pvl index 3ba97d2655..37d1e5f4a1 100644 --- a/examples/histories/History.pvl +++ b/examples/histories/History.pvl @@ -1,23 +1,16 @@ -// -*- tab-width:2 ; indent-tabs-mode:nil -*- //:: cases HistoryLoop //:: cases HistoryDefined -//:: suite problem-fail //:: tools silicon //:: options --check-defined +//:: verdict Pass //:: cases HistoryAxioms -//:: suite problem-fail //:: tools silicon //:: options --check-axioms - -/* - Checking the correctness of the defined processes and/or axioms is disabled due - refactoring. -*/ +//:: verdict Pass class History { - int x; modifies x; @@ -45,6 +38,5 @@ class History { requires m>=0 && n >= 0 ; ensures single(m)*single(n)==single(m+n); void single_axiom(int m,int n); - } diff --git a/src/main/java/vct/col/rewrite/CheckProcessAlgebra.java b/src/main/java/vct/col/rewrite/CheckProcessAlgebra.java index 03f2f9aa9f..c829cb0efb 100644 --- a/src/main/java/vct/col/rewrite/CheckProcessAlgebra.java +++ b/src/main/java/vct/col/rewrite/CheckProcessAlgebra.java @@ -361,7 +361,7 @@ private ASTNode left_merge(ASTNode m_body, ASTNode other) { } for(ASTNode n:m0.getArgs()) args.add(n); for(ASTNode n:m1.getArgs()) args.add(n); - ASTNode guess=create.invokation(null,null,merged,args.toArray(new ASTNode[0])); + ASTNode guess=create.invokation(create.reserved_name(ASTReserved.This),null,merged,args.toArray(new ASTNode[0])); return create.expression(StandardOperator.Mult,p0,guess); } case ITE:{ diff --git a/src/main/java/vct/col/rewrite/RandomizedIf.java b/src/main/java/vct/col/rewrite/RandomizedIf.java index 0878a7b5c9..922a659066 100644 --- a/src/main/java/vct/col/rewrite/RandomizedIf.java +++ b/src/main/java/vct/col/rewrite/RandomizedIf.java @@ -21,7 +21,8 @@ public RandomizedIf(ProgramUnit source) { public void visit(ASTClass cl){ DeclarationStatement args[]=new DeclarationStatement[0]; Method if_any_method=create.method_decl(create.primitive_type(PrimitiveSort.Boolean), null, "if_any_random", args, null); - + if_any_method.setFlag(ASTFlags.FINAL, true); + if (if_any_method.getOrigin() == null) { if_any_method.setOrigin(new MessageOrigin("Default origin")); } @@ -66,7 +67,7 @@ public void visit(IfStatement s){ IfStatement res=new IfStatement(); currentBlock.addStatement( create.assignment(create.local_name("if_any_bool"), - create.invokation(null,null,"if_any_random")) + create.invokation(create.reserved_name(ASTReserved.This),null,"if_any_random")) ); res.addClause(create.local_name("if_any_bool"), rewrite(s.getStatement(0))); res.addClause(IfStatement.elseGuard(), rewrite(s.getStatement(1))); From a8646d098ce4f333a41450d0df452ba5326a143d Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Mon, 19 Jul 2021 13:53:58 +0200 Subject: [PATCH 2/2] Move fixed tests back to their regular folders --- examples/{known-problems => }/gpgpu/simple-ltid.cu | 0 examples/{known-problems => }/histories/History.pvl | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename examples/{known-problems => }/gpgpu/simple-ltid.cu (100%) rename examples/{known-problems => }/histories/History.pvl (100%) diff --git a/examples/known-problems/gpgpu/simple-ltid.cu b/examples/gpgpu/simple-ltid.cu similarity index 100% rename from examples/known-problems/gpgpu/simple-ltid.cu rename to examples/gpgpu/simple-ltid.cu diff --git a/examples/known-problems/histories/History.pvl b/examples/histories/History.pvl similarity index 100% rename from examples/known-problems/histories/History.pvl rename to examples/histories/History.pvl