Skip to content

Commit b706149

Browse files
SaloedSaloed
committed
initial
0 parents  commit b706149

36 files changed

+7503
-0
lines changed

‎.gitignore

+42
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
.gradle
2+
build/
3+
!gradle/wrapper/gradle-wrapper.jar
4+
!**/src/main/**/build/
5+
!**/src/test/**/build/
6+
7+
### IntelliJ IDEA ###
8+
.idea/modules.xml
9+
.idea/jarRepositories.xml
10+
.idea/compiler.xml
11+
.idea/libraries/
12+
*.iws
13+
*.iml
14+
*.ipr
15+
out/
16+
!**/src/main/**/out/
17+
!**/src/test/**/out/
18+
19+
### Eclipse ###
20+
.apt_generated
21+
.classpath
22+
.factorypath
23+
.project
24+
.settings
25+
.springBeans
26+
.sts4-cache
27+
bin/
28+
!**/src/main/**/bin/
29+
!**/src/test/**/bin/
30+
31+
### NetBeans ###
32+
/nbproject/private/
33+
/nbbuild/
34+
/dist/
35+
/nbdist/
36+
/.nb-gradle/
37+
38+
### VS Code ###
39+
.vscode/
40+
41+
### Mac OS ###
42+
.DS_Store

‎approximations/build.gradle.kts

+28
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
plugins {
2+
java
3+
`maven-publish`
4+
}
5+
6+
repositories {
7+
mavenCentral()
8+
}
9+
10+
dependencies {
11+
compileOnly("org.jacodb:jacodb-approximations:1.2.0")
12+
compileOnly(files(rootDir.resolve("usvm-api/usvm-api.jar")))
13+
}
14+
15+
group = "org.usvm.approximations.java.stdlib"
16+
version = "0.0.0"
17+
18+
tasks.withType<JavaCompile> {
19+
options.release = 11
20+
}
21+
22+
publishing {
23+
publications {
24+
create<MavenPublication>("maven") {
25+
from(components["java"])
26+
}
27+
}
28+
}

‎approximations/src/main/java/generated/java/lang/AutoCloseable.java

+35
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
// Generated by the LibSL translator. DO NOT EDIT!
2+
// source: ?
3+
//
4+
package generated.java.lang;
5+
6+
import org.jacodb.approximation.annotation.Approximate;
7+
import org.usvm.api.Engine;
8+
import runtime.LibSLRuntime;
9+
10+
/**
11+
* AutoCloseableAutomaton for LSLAutoCloseable ~> java.lang.AutoCloseable
12+
*/
13+
@Approximate(java.lang.AutoCloseable.class)
14+
public interface AutoCloseable extends LibSLRuntime.Automaton {
15+
Class __$_lsl_INIT_INTERFACE_AutoCloseableAutomaton_d61c3b46 = Void.class;
16+
17+
/**
18+
* [FUNCTION] AutoCloseableAutomaton::close(LSLAutoCloseable) -> void
19+
*/
20+
default void close() {
21+
/* body */ {
22+
}
23+
}
24+
25+
final class __$lsl_States {
26+
public static final byte Initialized = (byte) 0;
27+
}
28+
29+
@Approximate(AutoCloseable.class)
30+
final class __hook {
31+
private __hook(Void o1, Void o2) {
32+
Engine.assume(false);
33+
}
34+
}
35+
}

‎approximations/src/main/java/generated/java/lang/Object.java

+74
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
// Generated by the LibSL translator. DO NOT EDIT!
2+
// source: ?
3+
//
4+
package generated.java.lang;
5+
6+
import org.jacodb.approximation.annotation.Approximate;
7+
import org.usvm.api.Engine;
8+
import runtime.LibSLRuntime;
9+
10+
/**
11+
* ObjectAutomaton for LSLObject ~> java.lang.Object
12+
*/
13+
@Approximate(java.lang.Object.class)
14+
public class Object implements LibSLRuntime.Automaton {
15+
static {
16+
/* ObjectAutomaton::__clinit__() */ {
17+
;
18+
}
19+
}
20+
21+
@LibSLRuntime.AutomatonConstructor
22+
public Object(Void __$lsl_token, final byte p0) {
23+
}
24+
25+
@LibSLRuntime.AutomatonConstructor
26+
public Object(final Void __$lsl_token) {
27+
this(__$lsl_token, __$lsl_States.Initialized);
28+
}
29+
30+
/**
31+
* [FUNCTION] ObjectAutomaton::equals(LSLObject, Object) -> boolean
32+
*/
33+
public boolean equals(java.lang.Object obj) {
34+
boolean result = false;
35+
/* body */ {
36+
result = this == obj;
37+
}
38+
return result;
39+
}
40+
41+
/**
42+
* [FUNCTION] ObjectAutomaton::hashCode(LSLObject) -> int
43+
*/
44+
public int hashCode() {
45+
int result = 0;
46+
/* body */ {
47+
result = Engine.makeSymbolicInt();
48+
}
49+
return result;
50+
}
51+
52+
/**
53+
* [FUNCTION] ObjectAutomaton::toString(LSLObject) -> String
54+
*/
55+
public String toString() {
56+
String result = null;
57+
/* body */ {
58+
result = Engine.makeSymbolic(String.class);
59+
Engine.assume(result != null);
60+
}
61+
return result;
62+
}
63+
64+
public static final class __$lsl_States {
65+
public static final byte Initialized = (byte) 0;
66+
}
67+
68+
@Approximate(Object.class)
69+
public static final class __hook {
70+
private __hook(Void o1, Void o2) {
71+
Engine.assume(false);
72+
}
73+
}
74+
}

‎approximations/src/main/java/generated/java/lang/Throwable.java

+112
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,112 @@
1+
// Generated by the LibSL translator. DO NOT EDIT!
2+
// source: ?
3+
//
4+
package generated.java.lang;
5+
6+
import org.jacodb.approximation.annotation.Approximate;
7+
import org.usvm.api.Engine;
8+
import runtime.LibSLRuntime;
9+
10+
import java.io.Serializable;
11+
12+
/**
13+
* ThrowableAutomaton for LSLThrowable ~> java.lang.Throwable
14+
*/
15+
@Approximate(java.lang.Throwable.class)
16+
public class Throwable implements LibSLRuntime.Automaton, Serializable {
17+
private static long serialVersionUID = -3042686055658047285L;
18+
19+
private static String NULL_CAUSE_MESSAGE = "Cannot suppress a null exception.";
20+
21+
private static String SELF_SUPPRESSION_MESSAGE = "Self-suppression not permitted";
22+
23+
private static String CAUSE_CAPTION = "Caused by: ";
24+
25+
private static String SUPPRESSED_CAPTION = "Suppressed: ";
26+
27+
static {
28+
}
29+
30+
@LibSLRuntime.AutomatonConstructor
31+
public Throwable(Void __$lsl_token, final byte p0) {
32+
}
33+
34+
@LibSLRuntime.AutomatonConstructor
35+
public Throwable(final Void __$lsl_token) {
36+
this(__$lsl_token, __$lsl_States.Initialized);
37+
}
38+
39+
/**
40+
* [FUNCTION] ThrowableAutomaton::addSuppressed(LSLThrowable, Throwable) -> void
41+
*/
42+
public final synchronized void addSuppressed(java.lang.Throwable exception) {
43+
/* body */ {
44+
}
45+
}
46+
47+
/**
48+
* [FUNCTION] ThrowableAutomaton::fillInStackTrace(LSLThrowable) -> Throwable
49+
*/
50+
public synchronized java.lang.Throwable fillInStackTrace() {
51+
java.lang.Throwable result = null;
52+
/* body */ {
53+
result = Engine.makeSymbolic(java.lang.Throwable.class);
54+
}
55+
return result;
56+
}
57+
58+
/**
59+
* [FUNCTION] ThrowableAutomaton::getStackTrace(LSLThrowable) -> array<StackTraceElement>
60+
*/
61+
public StackTraceElement[] getStackTrace() {
62+
StackTraceElement[] result = null;
63+
/* body */ {
64+
final int size = Engine.makeSymbolicInt();
65+
Engine.assume(size >= 0);
66+
Engine.assume(size < 99);
67+
result = Engine.makeSymbolicArray(StackTraceElement.class, size);
68+
}
69+
return result;
70+
}
71+
72+
/**
73+
* [FUNCTION] ThrowableAutomaton::getSuppressed(LSLThrowable) -> array<Throwable>
74+
*/
75+
public final synchronized java.lang.Throwable[] getSuppressed() {
76+
java.lang.Throwable[] result = null;
77+
/* body */ {
78+
final int size = Engine.makeSymbolicInt();
79+
Engine.assume(size >= 0);
80+
Engine.assume(size < 99);
81+
result = Engine.makeSymbolicArray(java.lang.Throwable.class, size);
82+
}
83+
return result;
84+
}
85+
86+
/**
87+
* [FUNCTION] ThrowableAutomaton::printStackTrace(LSLThrowable) -> void
88+
*/
89+
public void printStackTrace() {
90+
/* body */ {
91+
}
92+
}
93+
94+
/**
95+
* [FUNCTION] ThrowableAutomaton::setStackTrace(LSLThrowable, array<StackTraceElement>) -> void
96+
*/
97+
public void setStackTrace(StackTraceElement[] stackTrace) {
98+
/* body */ {
99+
}
100+
}
101+
102+
public static final class __$lsl_States {
103+
public static final byte Initialized = (byte) 0;
104+
}
105+
106+
@Approximate(Throwable.class)
107+
public static final class __hook {
108+
private __hook(Void o1, Void o2) {
109+
Engine.assume(false);
110+
}
111+
}
112+
}

0 commit comments

Comments
 (0)