From 39742e5cb23b77195a3f21358914c422e0a07d7a Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Tue, 14 Nov 2017 15:17:48 +0100 Subject: [PATCH] minor --- .../psdbg/lint/checkers/EmptyBlocks.java | 5 +++ .../lint/checkers/NegatedMatchWithUsing.java | 10 ++++- .../lint/checkers/SuccessiveGoalSelector.java | 10 +++-- .../checkers/VariableDeclarationCheck.java | 5 +++ .../examples/java/sumAndMax/SumAndMax.java | 39 +++++++++++++++++++ .../psdbg/examples/java/sumAndMax/script.kps | 23 +++++++++++ 6 files changed, 86 insertions(+), 6 deletions(-) create mode 100644 ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/sumAndMax/SumAndMax.java create mode 100644 ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/sumAndMax/script.kps diff --git a/lint/src/main/java/edu/kit/iti/formal/psdbg/lint/checkers/EmptyBlocks.java b/lint/src/main/java/edu/kit/iti/formal/psdbg/lint/checkers/EmptyBlocks.java index e5e0606b..c982fa83 100644 --- a/lint/src/main/java/edu/kit/iti/formal/psdbg/lint/checkers/EmptyBlocks.java +++ b/lint/src/main/java/edu/kit/iti/formal/psdbg/lint/checkers/EmptyBlocks.java @@ -17,6 +17,11 @@ public class EmptyBlocks extends AbstractLintRule { private static class EmptyBlockSearcher extends Searcher { + @Override + public Void visit(FunctionCall func) { + return null; + } + public void check(ASTNode node, Statements statements) { if (statements.size() == 0) { problem(EMPTY_BLOCK, node); diff --git a/lint/src/main/java/edu/kit/iti/formal/psdbg/lint/checkers/NegatedMatchWithUsing.java b/lint/src/main/java/edu/kit/iti/formal/psdbg/lint/checkers/NegatedMatchWithUsing.java index db69c201..dc8d027a 100644 --- a/lint/src/main/java/edu/kit/iti/formal/psdbg/lint/checkers/NegatedMatchWithUsing.java +++ b/lint/src/main/java/edu/kit/iti/formal/psdbg/lint/checkers/NegatedMatchWithUsing.java @@ -1,9 +1,10 @@ package edu.kit.iti.formal.psdbg.lint.checkers; -import edu.kit.iti.formal.psdbg.parser.ast.MatchExpression; -import edu.kit.iti.formal.psdbg.parser.ast.UnaryExpression; import edu.kit.iti.formal.psdbg.lint.Issue; import edu.kit.iti.formal.psdbg.lint.IssuesRepository; +import edu.kit.iti.formal.psdbg.parser.ast.FunctionCall; +import edu.kit.iti.formal.psdbg.parser.ast.MatchExpression; +import edu.kit.iti.formal.psdbg.parser.ast.UnaryExpression; /** * @author Alexander Weigl @@ -27,5 +28,10 @@ public class NegatedMatchWithUsing extends AbstractLintRule { } return super.visit(ue); } + + @Override + public Void visit(FunctionCall func) { + return null; + } } } diff --git a/lint/src/main/java/edu/kit/iti/formal/psdbg/lint/checkers/SuccessiveGoalSelector.java b/lint/src/main/java/edu/kit/iti/formal/psdbg/lint/checkers/SuccessiveGoalSelector.java index 8565bd7b..8635233b 100644 --- a/lint/src/main/java/edu/kit/iti/formal/psdbg/lint/checkers/SuccessiveGoalSelector.java +++ b/lint/src/main/java/edu/kit/iti/formal/psdbg/lint/checkers/SuccessiveGoalSelector.java @@ -1,11 +1,8 @@ package edu.kit.iti.formal.psdbg.lint.checkers; -import edu.kit.iti.formal.psdbg.parser.ast.ForeachStatement; -import edu.kit.iti.formal.psdbg.parser.ast.GoalSelector; -import edu.kit.iti.formal.psdbg.parser.ast.RepeatStatement; -import edu.kit.iti.formal.psdbg.parser.ast.TheOnlyStatement; import edu.kit.iti.formal.psdbg.lint.Issue; import edu.kit.iti.formal.psdbg.lint.IssuesRepository; +import edu.kit.iti.formal.psdbg.parser.ast.*; import java.util.Objects; @@ -67,5 +64,10 @@ public class SuccessiveGoalSelector extends AbstractLintRule { } return super.visit(repeat); } + + @Override + public Void visit(FunctionCall func) { + return null; + } } } \ No newline at end of file diff --git a/lint/src/main/java/edu/kit/iti/formal/psdbg/lint/checkers/VariableDeclarationCheck.java b/lint/src/main/java/edu/kit/iti/formal/psdbg/lint/checkers/VariableDeclarationCheck.java index db5c86fa..47fa2d6e 100644 --- a/lint/src/main/java/edu/kit/iti/formal/psdbg/lint/checkers/VariableDeclarationCheck.java +++ b/lint/src/main/java/edu/kit/iti/formal/psdbg/lint/checkers/VariableDeclarationCheck.java @@ -65,6 +65,11 @@ public class VariableDeclarationCheck extends AbstractLintRule { return null; } + @Override + public Void visit(FunctionCall func) { + return null; + } + private void declare(Variable var, Type type) { if (current.getType(var) != null) { problem(REDECLARE_VARIABLE).tokens(var.getToken()); diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/sumAndMax/SumAndMax.java b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/sumAndMax/SumAndMax.java new file mode 100644 index 00000000..bd160e65 --- /dev/null +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/sumAndMax/SumAndMax.java @@ -0,0 +1,39 @@ +class SumAndMax { + + int sum; + int max; + + /*@ normal_behaviour + @ requires (\forall int i; 0 <= i && i < a.length; 0 <= a[i]); + @ assignable sum, max; + @ ensures (\forall int i; 0 <= i && i < a.length; a[i] <= max); + @ ensures (a.length > 0 + @ ==> (\exists int i; 0 <= i && i < a.length; max == a[i])); + @ ensures sum == (\sum int i; 0 <= i && i < a.length; a[i]); + @ ensures sum <= a.length * max; + @*/ + void sumAndMax(int[] a) { + sum = 0; + max = 0; + int k = 0; + + /*@ loop_invariant + @ 0 <= k && k <= a.length + @ && (\forall int i; 0 <= i && i < k; a[i] <= max) + @ && (k == 0 ==> max == 0) + @ && (k > 0 ==> (\exists int i; 0 <= i && i < k; max == a[i])) + @ && sum == (\sum int i; 0 <= i && i< k; a[i]) + @ && sum <= k * max; + @ + @ assignable sum, max; + @ decreases a.length - k; + @*/ + while(k < a.length) { + if(max < a[k]) { + max = a[k]; + } + sum += a[k]; + k++; + } + } +} diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/sumAndMax/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/sumAndMax/script.kps new file mode 100644 index 00000000..2b5a4519 --- /dev/null +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/sumAndMax/script.kps @@ -0,0 +1,23 @@ + +script auto1() { + auto; +} + +script sumandmax() { +symbex; +cases{ + case match `wellFormed(heap)`: //1486 ähnlich wie 1288 + andRight; + cases{ + case `==> true`: //Case 1 + closeTrue; + + default: //Case 2 + } + default: + +} + + +} + -- GitLab