Skip to content

Commit f9a8da3

Browse files
alcidesalcides
committed
Added Formatter
1 parent e6bf933 commit f9a8da3

File tree

372 files changed

+4097
-4712
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

372 files changed

+4097
-4712
lines changed

‎.gitignore‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
/target/
22
!.mvn/wrapper/maven-wrapper.jar
3-
3+
spooned
44
### STS ###
55
.apt_generated
66
.classpath
@@ -162,4 +162,4 @@ $RECYCLE.BIN/
162162

163163
.DS_Store
164164

165-
# End of https://www.gitignore.io/api/git,java,maven,eclipse,windows
165+
# End of https://www.gitignore.io/api/git,java,maven,eclipse,windows

‎.pre-commit-config.yaml‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
repos:
2+
- repo: https://github.com/ejba/pre-commit-maven
3+
rev: v0.3.3
4+
hooks:
5+
- id: maven
6+
args: [clean compile clean]
7+
- repo: https://github.com/macisamuele/language-formatters-pre-commit-hooks
8+
rev: v2.11.0
9+
hooks:
10+
- id: pretty-format-java
11+
args: [--autofix]
12+
- id: pretty-format-yaml
13+
args: [--autofix, --indent, '2']

liquidjava-umbrella/.vscode/settings.json renamed to .vscode/settings.json

File renamed without changes.

liquidjava-umbrella/liquidjava-api/pom.xml renamed to liquidjava-api/pom.xml

File renamed without changes.

liquidjava-umbrella/liquidjava-api/src/main/java/example/NumericExample.java renamed to liquidjava-api/src/main/java/example/NumericExample.java

Lines changed: 13 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -3,35 +3,32 @@
33
* Administrator of the National Aeronautics and Space Administration.
44
* All rights reserved.
55
*
6-
* Symbolic Pathfinder (jpf-symbc) is licensed under the Apache License,
6+
* Symbolic Pathfinder (jpf-symbc) is licensed under the Apache License,
77
* Version 2.0 (the "License"); you may not use this file except
88
* in compliance with the License. You may obtain a copy of the License at
9-
*
10-
* http://www.apache.org/licenses/LICENSE-2.0.
9+
*
10+
* http://www.apache.org/licenses/LICENSE-2.0.
1111
*
1212
* Unless required by applicable law or agreed to in writing, software
1313
* distributed under the License is distributed on an "AS IS" BASIS,
1414
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15-
* See the License for the specific language governing permissions and
15+
* See the License for the specific language governing permissions and
1616
* limitations under the License.
1717
*/
1818

1919
package example;
2020

2121
public class NumericExample {
2222

23-
public static int test(int a, int b) {
24-
int c = a/(b+a -2);
25-
if(c>0)
26-
System.out.println(">0");
27-
else
28-
System.out.println("<=0");
29-
30-
return c;
31-
}
32-
public static void main(String[] args) {
33-
test(0,0);
23+
public static int test(int a, int b) {
24+
int c = a / (b + a - 2);
25+
if (c > 0) System.out.println(">0");
26+
else System.out.println("<=0");
3427

35-
}
28+
return c;
29+
}
3630

31+
public static void main(String[] args) {
32+
test(0, 0);
33+
}
3734
}

liquidjava-umbrella/liquidjava-api/src/main/java/example/NumericExample.jpf renamed to liquidjava-api/src/main/java/example/NumericExample.jpf

File renamed without changes.

‎liquidjava-api/src/main/java/example/Simple.java‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
package example;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
@Refinement("super.x > 10")
6+
public class Simple extends ToSimple {
7+
8+
@Refinement("z > 0 && z > super.x")
9+
private int z;
10+
11+
@Refinement("\\return == x + 1")
12+
public static int function1(@Refinement("x > 0") final int x) {
13+
14+
@Refinement("y > 0")
15+
int y = x + 1;
16+
17+
return y;
18+
}
19+
}

liquidjava-umbrella/liquidjava-api/src/main/java/example/ToSimple.java renamed to liquidjava-api/src/main/java/example/ToSimple.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
package example;
22

33
public class ToSimple {
4-
5-
protected int x;
4+
5+
protected int x;
66
}

‎liquidjava-api/src/main/java/liquidjava/Main.java‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
package liquidjava;
2+
3+
import example.Simple;
4+
import java.util.List;
5+
import liquidjava.infer.InducedRefinementsParser;
6+
import liquidjava.utils.Processor;
7+
8+
/** Main class for the Repair system */
9+
public class Main {
10+
11+
public static void main(String[] args) throws Exception {
12+
13+
List<String> refinements = (new Processor()).getRefinement(new Simple());
14+
15+
List<String> inducedRefinements = InducedRefinementsParser.parseRefinements("output3");
16+
17+
System.out.println(refinements);
18+
System.out.println(inducedRefinements);
19+
20+
String finalRefinement = "";
21+
22+
if (!refinements.isEmpty()) {
23+
finalRefinement += String.join(" && ", refinements);
24+
25+
if (!refinements.isEmpty())
26+
finalRefinement += " && " + String.join(" && ", inducedRefinements);
27+
} else if (!inducedRefinements.isEmpty())
28+
finalRefinement = String.join(" && ", inducedRefinements);
29+
30+
System.out.println(finalRefinement);
31+
}
32+
}

‎liquidjava-api/src/main/java/liquidjava/infer/InducedRefinementsParser.java‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
package liquidjava.infer;
2+
3+
import java.io.BufferedReader;
4+
import java.io.FileReader;
5+
import java.io.IOException;
6+
import java.util.ArrayList;
7+
import java.util.List;
8+
9+
public class InducedRefinementsParser {
10+
11+
private static final String STARTER =
12+
"====================================================== search started:";
13+
private static final String ENDER = "*************Summary***************";
14+
15+
public InducedRefinementsParser() {
16+
// Does nothing
17+
}
18+
19+
public static List<String> parseRefinements(String file) throws IOException {
20+
21+
List<String> result = new ArrayList<>();
22+
23+
try (BufferedReader reader = new BufferedReader(new FileReader(file))) {
24+
25+
String line = reader.readLine();
26+
27+
boolean start = false;
28+
boolean end = false;
29+
30+
while ((line = reader.readLine()) != null && !end) {
31+
if (!start) {
32+
start = line.startsWith(STARTER);
33+
continue;
34+
} else end = line.startsWith(ENDER);
35+
36+
if (start && !end)
37+
if (line.contains("NPC constraint")) {
38+
39+
line = reader.readLine();
40+
41+
while (line.endsWith("&&") || line.endsWith("||")) line += reader.readLine();
42+
43+
if (line.startsWith("%")) line = line.substring(line.indexOf("%", 2) + 1);
44+
45+
result.add(line);
46+
}
47+
}
48+
49+
} catch (IOException e) {
50+
e.printStackTrace();
51+
}
52+
53+
return result;
54+
}
55+
}

0 commit comments

Comments
 (0)