Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
P
ProofScriptParser
Project overview
Project overview
Details
Activity
Releases
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
24
Issues
24
List
Boards
Labels
Milestones
Merge Requests
4
Merge Requests
4
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
sarah.grebing
ProofScriptParser
Commits
932ccd8b
Commit
932ccd8b
authored
Aug 17, 2017
by
Alexander Weigl
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
missing files
parent
f3c061d8
Pipeline
#12899
failed with stage
in 1 minute and 36 seconds
Changes
5
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
475 additions
and
0 deletions
+475
-0
src/main/java/edu/kit/formal/psdb/lint/checkers/IssuesId.java
...main/java/edu/kit/formal/psdb/lint/checkers/IssuesId.java
+15
-0
src/main/java/edu/kit/formal/psdb/lint/checkers/NegatedMatchWithUsing.java
.../kit/formal/psdb/lint/checkers/NegatedMatchWithUsing.java
+31
-0
src/main/resources/edu/kit/formal/psdb/gui/debugger-ui.less
src/main/resources/edu/kit/formal/psdb/gui/debugger-ui.less
+297
-0
src/test/java/edu/kit/formal/psdb/lint/LinterTest.java
src/test/java/edu/kit/formal/psdb/lint/LinterTest.java
+49
-0
src/test/java/edu/kit/formal/psdb/parser/EvalTest.java
src/test/java/edu/kit/formal/psdb/parser/EvalTest.java
+83
-0
No files found.
src/main/java/edu/kit/formal/psdb/lint/checkers/IssuesId.java
0 → 100644
View file @
932ccd8b
package
edu
.
kit
.
formal
.
psdb
.
lint
.
checkers
;
/**
* Should correspond to <code>issues-list-en.xml</code>
*
* @author Alexander Weigl
* @version 1 (23.05.17)
*/
public
enum
IssuesId
{
EMPTY_BLOCKS
,
EQUAL_SCRIPT_NAMES
,
NEGATED_MATCH_WITH_USING
,
SUCC_SAME_BLOCK
,
FOREACH_AFTER_THEONLY
,
REDECLARE_VARIABLE
,
REDECLARE_VARIABLE_TYPE_MISMATCH
,
VARIABLE_NOT_DECLARED
,
VARIABLE_NOT_USED
,
THEONLY_AFTER_FOREACH
}
src/main/java/edu/kit/formal/psdb/lint/checkers/NegatedMatchWithUsing.java
0 → 100644
View file @
932ccd8b
package
edu
.
kit
.
formal
.
psdb
.
lint
.
checkers
;
import
edu.kit.formal.psdb.parser.ast.MatchExpression
;
import
edu.kit.formal.psdb.parser.ast.UnaryExpression
;
import
edu.kit.formal.psdb.lint.Issue
;
import
edu.kit.formal.psdb.lint.IssuesRepository
;
/**
* @author Alexander Weigl
* @version 1 (23.05.17)
*/
public
class
NegatedMatchWithUsing
extends
AbstractLintRule
{
private
static
Issue
ISSUE
=
IssuesRepository
.
getIssue
(
IssuesId
.
NEGATED_MATCH_WITH_USING
);
public
NegatedMatchWithUsing
()
{
super
(
NMWUSearcher:
:
new
);
}
static
class
NMWUSearcher
extends
Searcher
{
@Override
public
Void
visit
(
UnaryExpression
ue
)
{
if
(
ue
.
getExpression
()
instanceof
MatchExpression
)
{
MatchExpression
me
=
(
MatchExpression
)
ue
.
getExpression
();
if
(
me
.
getSignature
()
!=
null
&&
me
.
getSignature
().
size
()
>
0
)
{
problem
(
ISSUE
,
ue
,
me
);
}
}
return
super
.
visit
(
ue
);
}
}
}
src/main/resources/edu/kit/formal/psdb/gui/debugger-ui.less
0 → 100644
View file @
932ccd8b
@base03: rgb(0, 43, 54);
@base02: rgb(7, 54, 66);
@base01: rgb(88, 110, 117);
@base00: rgb(101, 123, 131);
@base0: rgb(131, 148, 150);
@base1: rgb(147, 161, 161);
@base2: rgb(238, 232, 213);
@base3: rgb(253, 246, 227);
@yellow: rgb(181, 137, 0);
@orange: rgb(203, 75, 22);
@red: rgb(220, 50, 47);
@magenta: rgb(211, 54, 130);
@violet: rgb(108, 113, 196);
@blue: rgb(38, 139, 210);
@cyan: rgb(42, 161, 152);
@green: rgb(133, 153, 0);
.solarized-dark() {
background-color: @base03;
color: @base0;
}
.solarized-light() {
background-color: @base3;
color: @base00;
}
.script-area {
-fx-background-color: @base3;
-fx-font-family: "Fira Code Medium", monospace;
-fx-font-size: 12pt;
-fx-fill: @base00;
.lineno {
}
.EXE_MARKER {
-fx-fill: @violet;
-fx-border-color: red;
-fx-font-size: 120%;
-fx-font-weight: bold;
}
.NON_EXE_AREA {
-rtfx-background: @cyan;
-rtfx-underline-cap: butt;
-rtfx-underline-color: @cyan;
-rtfx-underline-width: 1px;
}
// Structures
.FOREACH, .CASES, .CASE, .DEFAULT
.THEONLY, .SCRIPT, .USING, .REPEAT {
-fx-fill: @blue;
-fx-font-weight: bold;
}
// Operators
.MATCH, .PLUS, .MINUS,
.MUL, .DIV, .EQ, .NEQ,
.GEQ, .LEQ, .GE,
.LE, .AND, .OR,
.IMP, .EQUIV, .NOT {
-fx-fill: @green;
}
//
.INDENT, .DEDENT, .COLON, .ASSIGN, .LPAREN, .RPAREN, .LBRACKET, .RBRACKET {
-fx-font-weight: bold;
-fx-fill: blueviolet;
}
.DIGITS, .TRUE, .FALSE {
-fx-fill: @orange;
}
.TERM_LITERAL {
-fx-fill: @green;
}
.STRING_LITERAL {
-fx-fill: @violet;
}
.SINGLE_LINE_COMMENT, .MULTI_LINE_COMMENT {
-fx-fill: @base01;
-fx-font-weight: 100;
}
.IDENTIFIER {
-fx-fill: @orange;
-fx-font-weight: bold;
}
.problem {
// -rtfx-background-color: @magenta;
-rtfx-underline-cap: butt;
-rtfx-underline-color: red;
-rtfx-underline-width: 2px;
-fx-underline: true;
}
.line-highlight-postmortem {
-rtfx-background-color: @blue;
}
.line-unhighlight {
-fx-background-color: @base3;
}
.line-highlight-mainScript {
-rtfx-background-color: @green;
}
}
/**********************************************************************************************************************/
.breakpoint-menu {
-fx-skin: "com.sun.javafx.scene.control.skin.ContextMenuSkin";
-fx-font-family: sans-serif;
-fx-font-size: 9pt;
}
.java-area {
-fx-background-color: @base3;
-fx-font-family: "Fira Code Medium", monospace;
-fx-font-size: 12pt;
-fx-fill: @base01;
.ABSTRACT, .ASSERT, .BOOLEAN, .BREAK, .BYTE, .CASE, .CATCH, .CHAR, .CLASS, .CONST,
.CONTINUE, .DEFAULT, .DO, .DOUBLE, .ELSE, .ENUM, .EXTENDS, .FINAL, .FINALLY,
.FLOAT, .FOR, .IF, .GOTO, .IMPLEMENTS, .IMPORT, .INSTANCEOF, .INT,
.INTERFACE, .LONG, .NATIVE, .NEW, .PACKAGE, .PRIVATE, .PROTECTED, .PUBLIC, .RETURN,
.SHORT, .STATIC, .STRICTFP, .SUPER, .SWITCH, .SYNCHRONIZED, .THIS, .THROW, .THROWS,
.TRANSIENT, .TRY, .VOID, .VOLATILE, .WHILE {
-fx-fill: darkgreen;
-fx-font-weight: bold;
}
.hl-line {
-rtfx-background-color: @base03 !important;
-fx-fill: @base2;
-fx-font-weight: bold;
}
.NullLiteral {
-fx-font-weight: bold;
-fx-fill: @blue;
}
.LPAREN, .RPAREN, .LBRACE, .RBRACE, .LBRACK, .RBRACK, .SEMI, .COMMA, .DOT {
}
.INTEGER_LITERAL {
-fx-fill: @blue;
}
.StringLiteral, .CharacterLiteral {
-fx-fill: @green;
-fx-font-smoothing-type: lcd;
}
.LINE_COMMENT, .COMMENT {
-fx-fill: @base01;
-fx-font-family: "Fira Code Light";
}
.Identifier {
-fx-fill: @orange;
-fx-font-weight: bold;
}
.problem {
-fx-fill: firebrick !important;
-fx-underline: true;
}
.line-highlight {
-rtfx-background-color: @blue;
}
.line-un-highlight {
-rtfx-background-color: @base3;
}
}
/**********************************************************************************************************************/
.problem-popup {
-fx-background-color: @base03;
-fx-text-fill: @base3;
-fx-text-alignment: center;
-fx-wrap-text: true;
-fx-fill-width: true;
}
.problem-popup-label {
-fx-wrap-text: true;
}
.problem-popup-label-error {
-fx-text-fill: @red;
}
.problem-popup-label-warn, .problem-popup-label-warning {
-fx-text-fill: @orange;
}
.problem-popup-label-info {
-fx-text-fill: @blue;
}
.header {
-fx-font-size: 120%;
-fx-font-weight: bold;
-fx-padding: 5px;
}
.sequent-view {
-fx-font-size: 14pt;
-fx-background-color: @base2;
-fx-fill: black;
.sequent-highlight {
-rtfx-background-color: @base0;
-fx-fill: black;
}
}
.closed-sequent-view {
-fx-font-size: 14pt;
-fx-background-color: @green;
.sequent-highlight {
-rtfx-background-color: @base01;
-fx-fill: @base1
}
}
.section-pane {
.title {
-fx-font-weight: bold;
-fx-font-size: 14pt;
}
.header-box {
-fx-padding: 5px;
}
.header-buttons .button {
}
.header-buttons .button {
}
}
.contract-chooser {
.head {
-fx-font-weight: bold;
-fx-font-size: 120%;
}
.contract {
-fx-wrap-text: true;
-fx-font-family: monospace;
}
}
.tab-pane {
-fx-skin: "edu.kit.formal.psdb.gui.controls.CustomTabPaneSkin";
}
/**********************************************************************************************************************/
.inspection-view-tab {
&.LIVING {
-fx-background-color: forestgreen;
}
&.DEAD {
-fx-background-color: darkgrey;
}
&.POSTMORTEM {
-fx-background-color: blueviolet;
}
}
/**********************************************************************************************************************/
.context-menu {
-fx-skin: "com.sun.javafx.scene.control.skin.ContextMenuSkin";
-fx-font-family: sans-serif;
-fx-font-size: 9pt;
}
src/test/java/edu/kit/formal/psdb/lint/LinterTest.java
0 → 100644
View file @
932ccd8b
package
edu
.
kit
.
formal
.
psdb
.
lint
;
import
edu.kit.formal.psdb.parser.Facade
;
import
edu.kit.formal.psdb.parser.ast.ProofScript
;
import
org.antlr.v4.runtime.CharStreams
;
import
org.junit.Test
;
import
java.io.IOException
;
import
java.util.List
;
import
static
org
.
junit
.
Assert
.
assertEquals
;
/**
* @author Alexander Weigl
* @version 1 (23.05.17)
*/
public
class
LinterTest
{
@Test
public
void
testRegisteredLinter
()
{
assertEquals
(
5
,
LinterStrategy
.
getDefaultLinter
().
getCheckers
().
size
());
}
@Test
public
void
testLint1
()
throws
IOException
{
runLint
(
"lint1.kps"
);
}
@Test
public
void
testLint2
()
throws
IOException
{
runLint
(
"lint2.kps"
);
}
public
void
runLint
(
String
filename
)
throws
IOException
{
LinterStrategy
ls
=
LinterStrategy
.
getDefaultLinter
();
List
<
ProofScript
>
nodes
=
Facade
.
getAST
(
CharStreams
.
fromStream
(
getClass
().
getResourceAsStream
(
filename
)));
List
<
LintProblem
>
problems
=
ls
.
check
(
nodes
);
for
(
LintProblem
lp
:
problems
)
{
System
.
out
.
printf
(
"@%03d > (%s-%04d|%s) : %s%n"
,
lp
.
getLineNumber
(),
lp
.
getIssue
().
getSeverity
(),
lp
.
getIssue
().
getId
(),
lp
.
getIssue
().
getRulename
(),
lp
.
getMessage
().
trim
());
}
}
}
\ No newline at end of file
src/test/java/edu/kit/formal/psdb/parser/EvalTest.java
0 → 100644
View file @
932ccd8b
package
edu
.
kit
.
formal
.
psdb
.
parser
;
/*-
* #%L
* ProofScriptParser
* %%
* Copyright (C) 2017 Application-oriented Formal Verification
* %%
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public
* License along with this program. If not, see
* <http://www.gnu.org/licenses/gpl-3.0.html>.
* #L%
*/
import
edu.kit.formal.psdb.interpreter.Evaluator
;
import
edu.kit.formal.psdb.interpreter.data.GoalNode
;
import
edu.kit.formal.psdb.interpreter.data.Value
;
import
edu.kit.formal.psdb.interpreter.data.VariableAssignment
;
import
edu.kit.formal.psdb.parser.ast.Expression
;
import
edu.kit.formal.psdb.parser.types.SimpleType
;
import
org.junit.Assert
;
import
org.junit.Test
;
import
org.junit.runner.RunWith
;
import
org.junit.runners.Parameterized
;
import
java.io.IOException
;
@RunWith
(
Parameterized
.
class
)
public
class
EvalTest
{
@Parameterized
.
Parameters
(
name
=
"{0}"
)
public
static
Iterable
<
Object
[]>
getGoodExpressions
()
throws
IOException
{
return
TestHelper
.
loadLines
(
"eval.txt"
,
2
);
}
@Parameterized
.
Parameter
(
0
)
public
String
testExpression
;
@Parameterized
.
Parameter
(
1
)
public
String
expResult
;
@Test
public
void
test
()
throws
IOException
,
NotWelldefinedException
{
Expression
e_is
=
TestHelper
.
toExpr
(
testExpression
);
Expression
e_exp
=
TestHelper
.
toExpr
(
expResult
);
VariableAssignment
s
=
createAssignments
();
Evaluator
evaluator
=
new
Evaluator
(
s
,
new
GoalNode
(
null
,
null
,
true
));
Value
is
=
evaluator
.
eval
(
e_is
);
Value
exp
=
evaluator
.
eval
(
e_exp
);
Assert
.
assertEquals
(
exp
,
is
);
}
public
static
VariableAssignment
createAssignments
()
{
VariableAssignment
va
=
new
VariableAssignment
();
va
.
declare
(
"a"
,
SimpleType
.
INT
);
va
.
assign
(
"a"
,
Value
.
from
(
10
));
va
.
declare
(
"b"
,
SimpleType
.
INT
);
va
.
assign
(
"b"
,
Value
.
from
(
2
));
va
.
declare
(
"c"
,
SimpleType
.
INT
);
va
.
assign
(
"c"
,
Value
.
from
(
10
));
va
.
declare
(
"d"
,
SimpleType
.
INT
);
va
.
assign
(
"d"
,
Value
.
from
(
10
));
return
va
;
}
}
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment