diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests')
12 files changed, 214 insertions, 0 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.classpath b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.classpath new file mode 100644 index 00000000..1287f96c --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.classpath | |||
@@ -0,0 +1,9 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <classpath> | ||
3 | <classpathentry kind="src" path="src"/> | ||
4 | <classpathentry kind="src" path="src-gen"/> | ||
5 | <classpathentry kind="src" path="xtend-gen"/> | ||
6 | <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/> | ||
7 | <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/> | ||
8 | <classpathentry kind="output" path="bin"/> | ||
9 | </classpath> | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.gitignore new file mode 100644 index 00000000..ae3c1726 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.gitignore | |||
@@ -0,0 +1 @@ | |||
/bin/ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.project b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.project new file mode 100644 index 00000000..323ea59f --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.project | |||
@@ -0,0 +1,34 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <projectDescription> | ||
3 | <name>ca.mcgill.ecse.dslreasoner.vampire.language.tests</name> | ||
4 | <comment></comment> | ||
5 | <projects> | ||
6 | </projects> | ||
7 | <buildSpec> | ||
8 | <buildCommand> | ||
9 | <name>org.eclipse.xtext.ui.shared.xtextBuilder</name> | ||
10 | <arguments> | ||
11 | </arguments> | ||
12 | </buildCommand> | ||
13 | <buildCommand> | ||
14 | <name>org.eclipse.jdt.core.javabuilder</name> | ||
15 | <arguments> | ||
16 | </arguments> | ||
17 | </buildCommand> | ||
18 | <buildCommand> | ||
19 | <name>org.eclipse.pde.ManifestBuilder</name> | ||
20 | <arguments> | ||
21 | </arguments> | ||
22 | </buildCommand> | ||
23 | <buildCommand> | ||
24 | <name>org.eclipse.pde.SchemaBuilder</name> | ||
25 | <arguments> | ||
26 | </arguments> | ||
27 | </buildCommand> | ||
28 | </buildSpec> | ||
29 | <natures> | ||
30 | <nature>org.eclipse.xtext.ui.shared.xtextNature</nature> | ||
31 | <nature>org.eclipse.jdt.core.javanature</nature> | ||
32 | <nature>org.eclipse.pde.PluginNature</nature> | ||
33 | </natures> | ||
34 | </projectDescription> | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.settings/org.eclipse.core.resources.prefs b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.settings/org.eclipse.core.resources.prefs new file mode 100644 index 00000000..4824b802 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.settings/org.eclipse.core.resources.prefs | |||
@@ -0,0 +1,2 @@ | |||
1 | eclipse.preferences.version=1 | ||
2 | encoding/<project>=UTF-8 | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.settings/org.eclipse.jdt.core.prefs b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 00000000..295926d9 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/.settings/org.eclipse.jdt.core.prefs | |||
@@ -0,0 +1,7 @@ | |||
1 | eclipse.preferences.version=1 | ||
2 | org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled | ||
3 | org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 | ||
4 | org.eclipse.jdt.core.compiler.compliance=1.8 | ||
5 | org.eclipse.jdt.core.compiler.problem.assertIdentifier=error | ||
6 | org.eclipse.jdt.core.compiler.problem.enumIdentifier=error | ||
7 | org.eclipse.jdt.core.compiler.source=1.8 | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/META-INF/MANIFEST.MF b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/META-INF/MANIFEST.MF new file mode 100644 index 00000000..7e9ef500 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/META-INF/MANIFEST.MF | |||
@@ -0,0 +1,21 @@ | |||
1 | Manifest-Version: 1.0 | ||
2 | Bundle-ManifestVersion: 2 | ||
3 | Bundle-Name: ca.mcgill.ecse.dslreasoner.vampire.language.tests | ||
4 | Bundle-Vendor: My Company | ||
5 | Bundle-Version: 1.0.0.qualifier | ||
6 | Bundle-SymbolicName: ca.mcgill.ecse.dslreasoner.vampire.language.tests; singleton:=true | ||
7 | Bundle-ActivationPolicy: lazy | ||
8 | Require-Bundle: ca.mcgill.ecse.dslreasoner.vampire.language, | ||
9 | org.junit;bundle-version="4.12.0", | ||
10 | org.eclipse.xtext.testing, | ||
11 | org.eclipse.xtext.xbase.testing, | ||
12 | org.eclipse.xtext.xbase.lib | ||
13 | Bundle-RequiredExecutionEnvironment: JavaSE-1.8 | ||
14 | Export-Package: ca.mcgill.ecse.dslreasoner.tests;x-internal=true | ||
15 | Import-Package: org.hamcrest.core, | ||
16 | org.junit;version="4.5.0", | ||
17 | org.junit.runners.model;version="4.5.0", | ||
18 | org.junit.runner;version="4.5.0", | ||
19 | org.junit.runners;version="4.5.0", | ||
20 | org.junit.runner.manipulation;version="4.5.0", | ||
21 | org.junit.runner.notification;version="4.5.0" | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/build.properties b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/build.properties new file mode 100644 index 00000000..4c654e9b --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/build.properties | |||
@@ -0,0 +1,6 @@ | |||
1 | source.. = src/,\ | ||
2 | src-gen/,\ | ||
3 | xtend-gen/ | ||
4 | bin.includes = .,\ | ||
5 | META-INF/ | ||
6 | bin.excludes = **/*.xtend | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/src-gen/ca/mcgill/ecse/dslreasoner/tests/VampireLanguageInjectorProvider.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/src-gen/ca/mcgill/ecse/dslreasoner/tests/VampireLanguageInjectorProvider.java new file mode 100644 index 00000000..f3c1588b --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/src-gen/ca/mcgill/ecse/dslreasoner/tests/VampireLanguageInjectorProvider.java | |||
@@ -0,0 +1,66 @@ | |||
1 | /* | ||
2 | * generated by Xtext 2.12.0 | ||
3 | */ | ||
4 | package ca.mcgill.ecse.dslreasoner.tests; | ||
5 | |||
6 | import ca.mcgill.ecse.dslreasoner.VampireLanguageRuntimeModule; | ||
7 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup; | ||
8 | import com.google.inject.Guice; | ||
9 | import com.google.inject.Injector; | ||
10 | import org.eclipse.xtext.testing.GlobalRegistries; | ||
11 | import org.eclipse.xtext.testing.GlobalRegistries.GlobalStateMemento; | ||
12 | import org.eclipse.xtext.testing.IInjectorProvider; | ||
13 | import org.eclipse.xtext.testing.IRegistryConfigurator; | ||
14 | |||
15 | public class VampireLanguageInjectorProvider implements IInjectorProvider, IRegistryConfigurator { | ||
16 | |||
17 | protected GlobalStateMemento stateBeforeInjectorCreation; | ||
18 | protected GlobalStateMemento stateAfterInjectorCreation; | ||
19 | protected Injector injector; | ||
20 | |||
21 | static { | ||
22 | GlobalRegistries.initializeDefaults(); | ||
23 | } | ||
24 | |||
25 | @Override | ||
26 | public Injector getInjector() { | ||
27 | if (injector == null) { | ||
28 | stateBeforeInjectorCreation = GlobalRegistries.makeCopyOfGlobalState(); | ||
29 | this.injector = internalCreateInjector(); | ||
30 | stateAfterInjectorCreation = GlobalRegistries.makeCopyOfGlobalState(); | ||
31 | } | ||
32 | return injector; | ||
33 | } | ||
34 | |||
35 | protected Injector internalCreateInjector() { | ||
36 | return new VampireLanguageStandaloneSetup() { | ||
37 | @Override | ||
38 | public Injector createInjector() { | ||
39 | return Guice.createInjector(createRuntimeModule()); | ||
40 | } | ||
41 | }.createInjectorAndDoEMFRegistration(); | ||
42 | } | ||
43 | |||
44 | protected VampireLanguageRuntimeModule createRuntimeModule() { | ||
45 | // make it work also with Maven/Tycho and OSGI | ||
46 | // see https://bugs.eclipse.org/bugs/show_bug.cgi?id=493672 | ||
47 | return new VampireLanguageRuntimeModule() { | ||
48 | @Override | ||
49 | public ClassLoader bindClassLoaderToInstance() { | ||
50 | return VampireLanguageInjectorProvider.class | ||
51 | .getClassLoader(); | ||
52 | } | ||
53 | }; | ||
54 | } | ||
55 | |||
56 | @Override | ||
57 | public void restoreRegistry() { | ||
58 | stateBeforeInjectorCreation.restoreGlobalState(); | ||
59 | } | ||
60 | |||
61 | @Override | ||
62 | public void setupRegistry() { | ||
63 | getInjector(); | ||
64 | stateAfterInjectorCreation.restoreGlobalState(); | ||
65 | } | ||
66 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/src/ca/mcgill/ecse/dslreasoner/tests/VampireLanguageParsingTest.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/src/ca/mcgill/ecse/dslreasoner/tests/VampireLanguageParsingTest.xtend new file mode 100644 index 00000000..6d13b455 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/src/ca/mcgill/ecse/dslreasoner/tests/VampireLanguageParsingTest.xtend | |||
@@ -0,0 +1,29 @@ | |||
1 | /* | ||
2 | * generated by Xtext 2.12.0 | ||
3 | */ | ||
4 | package ca.mcgill.ecse.dslreasoner.tests | ||
5 | |||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
7 | import com.google.inject.Inject | ||
8 | import org.eclipse.xtext.testing.InjectWith | ||
9 | import org.eclipse.xtext.testing.XtextRunner | ||
10 | import org.eclipse.xtext.testing.util.ParseHelper | ||
11 | import org.junit.Assert | ||
12 | import org.junit.Test | ||
13 | import org.junit.runner.RunWith | ||
14 | |||
15 | @RunWith(XtextRunner) | ||
16 | @InjectWith(VampireLanguageInjectorProvider) | ||
17 | class VampireLanguageParsingTest { | ||
18 | @Inject | ||
19 | ParseHelper<VampireModel> parseHelper | ||
20 | |||
21 | @Test | ||
22 | def void loadModel() { | ||
23 | val result = parseHelper.parse(''' | ||
24 | Hello Xtext! | ||
25 | ''') | ||
26 | Assert.assertNotNull(result) | ||
27 | Assert.assertTrue(result.eResource.errors.isEmpty) | ||
28 | } | ||
29 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/.VampireLanguageParsingTest.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/.VampireLanguageParsingTest.xtendbin new file mode 100644 index 00000000..dc0af0a6 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/.VampireLanguageParsingTest.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/.gitignore new file mode 100644 index 00000000..032d1dcf --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/.gitignore | |||
@@ -0,0 +1 @@ | |||
/.VampireLanguageParsingTest.java._trace | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/VampireLanguageParsingTest.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/VampireLanguageParsingTest.java new file mode 100644 index 00000000..3bce3488 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.tests/xtend-gen/ca/mcgill/ecse/dslreasoner/tests/VampireLanguageParsingTest.java | |||
@@ -0,0 +1,38 @@ | |||
1 | /** | ||
2 | * generated by Xtext 2.12.0 | ||
3 | */ | ||
4 | package ca.mcgill.ecse.dslreasoner.tests; | ||
5 | |||
6 | import ca.mcgill.ecse.dslreasoner.tests.VampireLanguageInjectorProvider; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
8 | import com.google.inject.Inject; | ||
9 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
10 | import org.eclipse.xtext.testing.InjectWith; | ||
11 | import org.eclipse.xtext.testing.XtextRunner; | ||
12 | import org.eclipse.xtext.testing.util.ParseHelper; | ||
13 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
14 | import org.junit.Assert; | ||
15 | import org.junit.Test; | ||
16 | import org.junit.runner.RunWith; | ||
17 | |||
18 | @RunWith(XtextRunner.class) | ||
19 | @InjectWith(VampireLanguageInjectorProvider.class) | ||
20 | @SuppressWarnings("all") | ||
21 | public class VampireLanguageParsingTest { | ||
22 | @Inject | ||
23 | private ParseHelper<VampireModel> parseHelper; | ||
24 | |||
25 | @Test | ||
26 | public void loadModel() { | ||
27 | try { | ||
28 | StringConcatenation _builder = new StringConcatenation(); | ||
29 | _builder.append("Hello Xtext!"); | ||
30 | _builder.newLine(); | ||
31 | final VampireModel result = this.parseHelper.parse(_builder); | ||
32 | Assert.assertNotNull(result); | ||
33 | Assert.assertTrue(result.eResource().getErrors().isEmpty()); | ||
34 | } catch (Throwable _e) { | ||
35 | throw Exceptions.sneakyThrow(_e); | ||
36 | } | ||
37 | } | ||
38 | } | ||