Commit 39742e5c authored by Sarah Grebing's avatar Sarah Grebing

minor

parent e7ca8e3f
Pipeline #15428 passed with stages
in 7 minutes and 38 seconds
......@@ -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);
......
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;
}
}
}
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
......@@ -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());
......
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++;
}
}
}
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:
}
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment