Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Rusty equalsMod #13

Merged
merged 23 commits into from
Oct 1, 2024
Merged
Changes from 1 commit
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
2a02f5c
delete EqualsModProperty interface
tobias-rnh Aug 26, 2024
70a5651
Merge remote-tracking branch 'refs/remotes/drodt/rusty-while' into ru…
tobias-rnh Aug 26, 2024
b5adbe3
improve RenamingProgramElementProperty (WIP)
tobias-rnh Aug 27, 2024
36d760f
spotless
tobias-rnh Aug 27, 2024
53a9330
Merge remote-tracking branch 'refs/remotes/drodt/rusty' into rusty-eq…
tobias-rnh Sep 19, 2024
3b17c09
delete empty files leftover from merge
tobias-rnh Sep 19, 2024
47d8e27
handle more cases in RenamingProgramElementProperty
tobias-rnh Sep 19, 2024
e694892
implement equals methods for literal expressions
tobias-rnh Sep 23, 2024
0ce444c
change how IdentPattern is handled in RenamingProgramElementProperty
tobias-rnh Sep 23, 2024
222baef
write tests for RenamingProgramElementProperty
tobias-rnh Sep 23, 2024
ce66b3a
change package of EnhancedStringBuffer
tobias-rnh Sep 23, 2024
e2576d3
make literal equals methods null-safe
tobias-rnh Sep 23, 2024
02e2a78
use names instead of identifiers in NameAbstractionTable to handle pr…
tobias-rnh Sep 25, 2024
8eddd9e
write tests for RenamingProgramElementProperty
tobias-rnh Sep 26, 2024
c1d674d
delete ProofIrrelevancyProperty.java
tobias-rnh Sep 26, 2024
6223542
move tests out of BasicTest
tobias-rnh Sep 26, 2024
1f28afa
make hidden children visible for RenamingProgramElementProperty
tobias-rnh Sep 26, 2024
7594208
add hashCode methods to literals
tobias-rnh Sep 26, 2024
91c4581
match hashCodeModThisProperty to equalsModThisProperty
tobias-rnh Sep 27, 2024
2727a85
fix issue where programs with modality were not considered equal
tobias-rnh Sep 29, 2024
0b05908
spotless
tobias-rnh Sep 29, 2024
cfac148
implement a few equals and hashCode methods for RustyProgramElements
tobias-rnh Sep 29, 2024
29489e1
remove todo
tobias-rnh Sep 30, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
move tests out of BasicTest
tobias-rnh committed Sep 26, 2024

Verified

This commit was signed with the committer’s verified signature.
gorhill Raymond Hill
commit 62235420026386cb48db854f7a90fd3d20b27000
61 changes: 0 additions & 61 deletions keyext.rusty/src/test/java/org/key_project/rusty/BasicTest.java
Original file line number Diff line number Diff line change
@@ -9,7 +9,6 @@
import org.key_project.logic.Name;
import org.key_project.rusty.ast.abstraction.KeYRustyType;
import org.key_project.rusty.logic.*;
import org.key_project.rusty.logic.op.Modality;
import org.key_project.rusty.logic.op.ProgramVariable;
import org.key_project.rusty.proof.Goal;
import org.key_project.rusty.proof.Node;
@@ -27,7 +26,6 @@
import org.junit.jupiter.api.Test;

import static org.junit.jupiter.api.Assertions.*;
import static org.key_project.rusty.logic.equality.RenamingProgramElementProperty.RENAMING_PROGRAM_ELEMENT_PROPERTY;

public class BasicTest {
public static final String STANDARD_RUST_RULES_KEY =
@@ -302,63 +300,4 @@ public void testSwap() {
p.getRoot().sequent().succedent().getFirst().formula();
// continue manual proof like for example in TestApplyTaclet
}

@Test
public void testRenamingProgramElementProperty() {
TacletForTests.clear();
TacletForTests.parse(new RustProfile());
// seems like you must always give a type when using let
var t1 = TacletForTests.parseTerm(
"\\<{ let i: u32 = 5u32; 1u32 }\\>TRUE");
var t2 = TacletForTests.parseTerm(
"\\<{ let j: u32 = 5u32; 1u32 }\\>TRUE");

var program1 = ((Modality) t1.op()).program().program();
var program2 = ((Modality) t2.op()).program().program();

assertTrue(
RENAMING_PROGRAM_ELEMENT_PROPERTY.equalsModThisProperty(program1, program2,
new NameAbstractionTable()));

// Test 2
var t3 = TacletForTests.parseTerm(
"\\<{ 1u32 < 2u32 }\\>TRUE");
var t4 = TacletForTests.parseTerm(
"\\<{ 1u32 > 2u32 }\\>TRUE");

var program3 = ((Modality) t3.op()).program().program();
var program4 = ((Modality) t4.op()).program().program();

assertFalse(
RENAMING_PROGRAM_ELEMENT_PROPERTY.equalsModThisProperty(program3, program4,
new NameAbstractionTable()));

// Test 3
var t5 = TacletForTests.parseTerm("\\<{ i += 5u32 }\\>TRUE");
var t6 = TacletForTests.parseTerm("\\<{ i -= 5u32 }\\>TRUE");

var program5 = ((Modality) t5.op()).program().program();
var program6 = ((Modality) t6.op()).program().program();

// This passes as += and -= are not considered as different operations in the property as of
// now
// and the PV i is the one defined in testrules.key and therefore equals returns true.
// This currently does not work when using the let statement to introduce i.
assertTrue(
RENAMING_PROGRAM_ELEMENT_PROPERTY.equalsModThisProperty(program5, program6,
new NameAbstractionTable()));

// Test 4
var t7 = TacletForTests.parseTerm(
"\\<{ let mut i: u32 = 0u32; let mut j: u32 = 1u32; i = 2u32; j = i; 1u32}\\>TRUE");
var t8 = TacletForTests.parseTerm(
"\\<{ let mut i: u32 = 0u32; let mut k: u32 = 1u32; i = 2u32; k = i; 1u32}\\>TRUE");

var program7 = ((Modality) t7.op()).program().program();
var program8 = ((Modality) t8.op()).program().program();

// assertTrue(
// RENAMING_PROGRAM_ELEMENT_PROPERTY.equalsModThisProperty(program7, program8,
// new NameAbstractionTable()));
}
}