Skip to content

Add "Heap reference monotone" post condition for procedures that modify the Heap #1099

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.

Sign up for GitHub

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

Open
thanhnguyen-aws wants to merge 11 commits into
base: main2
Choose a base branch
from
Open

Add "Heap reference monotone" post condition for procedures that modify the Heap #1099

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
9f0ac52
add post condition: Heap reference monotone
thanhnguyen-aws May 1, 2026
b4967b9
revert changing Transparent procedure to Opaque, do it in Python -> L…
thanhnguyen-aws May 4, 2026
b5dca53
merge conflict
thanhnguyen-aws May 4, 2026
9771219
fix test
thanhnguyen-aws May 4, 2026
d23b9b7
Update Strata/Languages/Laurel/HeapParameterization.lean
thanhnguyen-aws May 4, 2026
1fc62fd
Merge branch 'main' into heapcountermono
thanhnguyen-aws May 5, 2026
725ee54
add Laurel test
thanhnguyen-aws May 5, 2026
32dc6ec
Merge branch 'main' into heapcountermono
thanhnguyen-aws May 5, 2026
a32340b
Update Strata/Languages/Laurel/HeapParameterization.lean
thanhnguyen-aws May 6, 2026
d1e920e
Update Strata/Languages/Laurel/HeapParameterization.lean
thanhnguyen-aws May 6, 2026
9335663
add source for monocond
thanhnguyen-aws May 11, 2026
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
13 changes: 11 additions & 2 deletions Strata/Languages/Laurel/HeapParameterization.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -471,6 +471,10 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform
-- Preconditions use $heap_in (the input state)
let preconditions' ← proc.preconditions.mapM (·.mapM (heapTransformExpr heapInName model))

let inHeapRef := mkMd $ .StaticCall "Heap..nextReference!" [mkMd $ .Var (.Local heapInName)]
let outHeapRef := mkMd $ .StaticCall "Heap..nextReference!" [mkMd $ .Var (.Local heapName)]
let monoCond : Condition := {condition:= {val:= .PrimitiveOp .Geq [outHeapRef, inHeapRef], source:= proc.name.source}, summary := s!"Heap reference counter monotone ({proc.name.text})"}

@keyboardDrummer keyboardDrummer Jun 11, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would it be possible to set free := true here ? I think monoCond holds by construction


let bodyValueIsUsed := !proc.outputs.isEmpty
let body' ← match proc.body with
| .Transparent bodyExpr =>
Expand All @@ -488,10 +492,15 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform
pure (some (mkMd (.Block [assignHeap, implExpr'] none)))
| none => pure none
let modif' ← modif.mapM (heapTransformExpr heapName model ·)
pure (.Opaque postconds' impl' modif')
-- When impl' = none, monoCond is axiomatic; it's safe to assume
-- because heapTransformExpr only uses updateField (preserves
-- nextReference) and increment (increases it by 1).
pure (.Opaque (monoCond::postconds') impl' modif')
Comment thread
thanhnguyen-aws marked this conversation as resolved.
| .Abstract postconds =>
let postconds' ← postconds.mapM (·.mapM (heapTransformExpr heapName model))
pure (.Abstract postconds')
-- monoCond is safe to assume because heapTransformExpr only uses
-- updateField (preserves nextReference) and increment (increases it by 1)
pure (.Abstract (monoCond::postconds'))
Comment thread
thanhnguyen-aws marked this conversation as resolved.
| .External => pure .External

return { proc with
Expand Down
17 changes: 17 additions & 0 deletions StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -158,6 +158,23 @@ procedure datatypeField()
// assert x == 4;
// }

procedure someWriteHeapProcedure(c: Container) returns ()
opaque
modifies c
{
c#intValue := 5
}
;

procedure callerUsesAllocateTwo()

@keyboardDrummer keyboardDrummer Jun 11, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't understand this test. Shouldn't it be:

procedure createsContainer(): Container opaque {
  return new Container;
}

procedure callCreatesContainer() {
  var a := createsContainer();
  var b := createsContainer();
  assert a != b
}

opaque
{
var c: Container;
var d: Container;
c := new Container;
someWriteHeapProcedure(c);
d := new Container;
assert c != d
procedure modifyHeapAndReturnMultiple(c: Container) returns (x: int, y: int, z: int)
opaque
ensures x == 1 && y == 2 && z == 3
Expand Down
6 changes: 3 additions & 3 deletions StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ procedure modifyContainerWildcard(c: Container) returns (i: int)
};

procedure modifyContainerWithoutPermission1(c: Container, d: Container)
// ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold
// ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause could not be proved

@tautschnig tautschnig May 4, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This error message changed from "modifies clause does not hold" to "modifies clause could not be proved". The former means the SMT solver found a counterexample; the latter means it timed out or returned unknown.

This is a diagnostic quality regression caused by the additional monotonicity postcondition making the VC harder for the solver. The same regression occurs at lines 130 and 155.

Please investigate whether the solver timeout can be avoided — e.g., by increasing the timeout for these VCs, or by structuring the postcondition differently so it doesn't interfere with the solver's ability to find counterexamples for unrelated assertions.

@thanhnguyen-aws thanhnguyen-aws May 11, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I acknowledge this one and have been woking with ATS to find a solution for it. It is more complicated than I think.

opaque
{
var i: int := modifyContainerWildcard(c)
Expand Down Expand Up @@ -127,7 +127,7 @@ procedure modifiesWildcardBodilessCaller()
var x: int := d#value;
modifiesWildcardBodiless(c, d);
assert x == d#value // this should fail because modifies * means anything can change
//^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
//^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
};

procedure modifiesWildcardWithBody(c: Container, d: Container)
Expand All @@ -152,7 +152,7 @@ procedure modifiesWildcardAndSpecificCaller()
var x: int := d#value;
modifiesWildcardAndSpecific(c, d);
assert x == d#value // fails because modifies * subsumes modifies c
//^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
//^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
};
"

Expand Down
1 change: 1 addition & 0 deletions StrataTest/Languages/Python/expected_interpret/test_heap_reference_monotone.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
\[ERROR\] procedure '__main__': expected 1 arguments, got 0
4 changes: 3 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_class_decl.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
test_class_decl.py(9, 4): ✅ pass - (CircularBuffer@__init__ requires) Type constraint of n
DETAIL: 1 passed, 0 failed, 0 inconclusive
test_class_decl.py(8, 0): ✅ pass - Heap reference counter monotone (main)
unknown location: ✅ pass - Heap reference counter monotone (__main__)
DETAIL: 3 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
4 changes: 3 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_class_empty.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
test_class_empty.py(5, 4): ✅ pass - callElimAssert_requires_4
test_class_empty.py(6, 4): ✅ pass - empty class instantiated
DETAIL: 2 passed, 0 failed, 0 inconclusive
test_class_empty.py(4, 0): ✅ pass - Heap reference counter monotone (test)
unknown location: ✅ pass - Heap reference counter monotone (__main__)
DETAIL: 4 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
4 changes: 3 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_class_field_any.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
test_class_field_any.py(2, 4): ✅ pass - Heap reference counter monotone (MyClass@__init__)
test_class_field_any.py(6, 0): ❓ unknown - assert(113)
DETAIL: 0 passed, 0 failed, 1 inconclusive
unknown location: ✅ pass - Heap reference counter monotone (__main__)
DETAIL: 2 passed, 0 failed, 1 inconclusive
RESULT: Inconclusive
3 changes: 2 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,2 +1,3 @@
DETAIL: 0 passed, 0 failed, 0 inconclusive
unknown location: ✔️ always true if reached - Heap reference counter monotone (__main__)
DETAIL: 1 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
3 changes: 2 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
test_class_field_use.py(14, 4): ✔️ always true if reached - Check PMul exception
test_class_field_use.py(14, 4): ✔️ always true if reached - assert(302)
test_class_field_use.py(15, 4): ✔️ always true if reached - Doubling of buffer did not work
DETAIL: 3 passed, 0 failed, 0 inconclusive
test_class_field_use.py(12, 0): ✔️ always true if reached - Heap reference counter monotone (main)
DETAIL: 4 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
3 changes: 2 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_class_inheritance_no_dispatch.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
test_class_inheritance_no_dispatch.py(25, 4): ❓ unknown - assert(714)
DETAIL: 0 passed, 0 failed, 1 inconclusive
unknown location: ✅ pass - Heap reference counter monotone (__main__)
DETAIL: 1 passed, 0 failed, 1 inconclusive
RESULT: Inconclusive
4 changes: 3 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_class_method_call_from_main.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
test_class_method_call_from_main.py(6, 4): ✅ pass - Heap reference counter monotone (Greeter@__init__)
test_class_method_call_from_main.py(10, 8): ❓ unknown - name must not be empty
test_class_method_call_from_main.py(9, 23): ❓ unknown - (Greeter@greet ensures) Return type constraint
test_class_method_call_from_main.py(14, 4): ✅ pass - (Greeter@__init__ requires) Type constraint of name
test_class_method_call_from_main.py(15, 4): ✅ pass - assert(415)
DETAIL: 2 passed, 0 failed, 2 inconclusive
unknown location: ✅ pass - Heap reference counter monotone (__main__)
DETAIL: 4 passed, 0 failed, 2 inconclusive
RESULT: Inconclusive
3 changes: 2 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_class_methods.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,5 +7,6 @@ test_class_methods.py(34, 4): ✔️ always true if reached - set_balance should
test_class_methods.py(31, 4): ✔️ always true if reached - assert_name_is_foo
test_class_methods.py(31, 4): ✔️ always true if reached - assert_opt_name_none_or_str
test_class_methods.py(31, 4): ✔️ always true if reached - assert_opt_name_none_or_bar
DETAIL: 9 passed, 0 failed, 0 inconclusive
unknown location: ✔️ always true if reached - Heap reference counter monotone (__main__)
DETAIL: 10 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
3 changes: 2 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_class_mixed_init.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
test_class_mixed_init.py(19, 0): ✔️ always true if reached - class with init
test_class_mixed_init.py(19, 0): ❓ unknown - class with init
DETAIL: 1 passed, 0 failed, 1 inconclusive
unknown location: ✔️ always true if reached - Heap reference counter monotone (__main__)
DETAIL: 2 passed, 0 failed, 1 inconclusive
RESULT: Inconclusive
4 changes: 3 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_class_no_init.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
test_class_no_init.py(5, 4): ✅ pass - callElimAssert_requires_4
test_class_no_init.py(6, 4): ❓ unknown - class without __init__
DETAIL: 1 passed, 0 failed, 1 inconclusive
test_class_no_init.py(4, 0): ✅ pass - Heap reference counter monotone (test)
unknown location: ✅ pass - Heap reference counter monotone (__main__)
DETAIL: 3 passed, 0 failed, 1 inconclusive
RESULT: Inconclusive
4 changes: 3 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_class_no_init_multi_field.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
test_class_no_init_multi_field.py(7, 4): ✅ pass - callElimAssert_requires_4
test_class_no_init_multi_field.py(8, 4): ✅ pass - class with multiple annotated fields no init
DETAIL: 2 passed, 0 failed, 0 inconclusive
test_class_no_init_multi_field.py(6, 0): ✅ pass - Heap reference counter monotone (test)
unknown location: ✅ pass - Heap reference counter monotone (__main__)
DETAIL: 4 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
4 changes: 3 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
test_class_no_init_with_method.py(4, 23): ❓ unknown - (WithMethod@get_x ensures) Return type constraint
test_class_no_init_with_method.py(8, 4): ✅ pass - callElimAssert_requires_4
test_class_no_init_with_method.py(9, 4): ✅ pass - class with method but no __init__
DETAIL: 2 passed, 0 failed, 1 inconclusive
test_class_no_init_with_method.py(7, 0): ✅ pass - Heap reference counter monotone (test)
unknown location: ✅ pass - Heap reference counter monotone (__main__)
DETAIL: 4 passed, 0 failed, 1 inconclusive
RESULT: Inconclusive
3 changes: 2 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,5 +5,6 @@ test_class_with_methods.py(32, 4): ✔️ always true if reached - get_name shou
test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_name_is_foo
test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_opt_name_none_or_str
test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_opt_name_none_or_bar
DETAIL: 7 passed, 0 failed, 0 inconclusive
unknown location: ✔️ always true if reached - Heap reference counter monotone (__main__)
DETAIL: 8 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
4 changes: 3 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_composite_return.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
test_composite_return.py(6, 4): ✅ pass - Heap reference counter monotone (MyService@__init__)
test_composite_return.py(10, 4): ✅ pass - (MyService@__init__ requires) Type constraint of name
DETAIL: 1 passed, 0 failed, 0 inconclusive
test_composite_return.py(9, 0): ✅ pass - Heap reference counter monotone (create_service)
DETAIL: 3 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
5 changes: 4 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_field_write.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@
test_field_write.py(4, 4): ✅ pass - Heap reference counter monotone (Cell@__init__)
test_field_write.py(8, 4): ✅ pass - (Cell@__init__ requires) Type constraint of val
test_field_write.py(10, 4): ✅ pass - field overwritten
DETAIL: 2 passed, 0 failed, 0 inconclusive
test_field_write.py(7, 0): ✅ pass - Heap reference counter monotone (test_oop_field_write)
unknown location: ✅ pass - Heap reference counter monotone (__main__)
DETAIL: 5 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
3 changes: 2 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,5 +6,6 @@ test_havoc_callee_after_hole_call.py(25, 0): ✔️ always true if reached - com
test_havoc_callee_after_hole_call.py(30, 0): ❓ unknown - expected unknown because argument locals should be havocked
test_havoc_callee_after_hole_call.py(36, 0): ❓ unknown - assume_assume(1193)_calls_PIn_0
test_havoc_callee_after_hole_call.py(37, 4): ✔️ always true if reached - for-loop over unmodeled iterator should not crash
DETAIL: 4 passed, 0 failed, 4 inconclusive
unknown location: ✔️ always true if reached - Heap reference counter monotone (__main__)
DETAIL: 5 passed, 0 failed, 4 inconclusive
RESULT: Inconclusive
7 changes: 7 additions & 0 deletions StrataTest/Languages/Python/expected_laurel/test_heap_reference_monotone.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
test_heap_reference_monotone.py(2, 4): ✅ pass - Heap reference counter monotone (ClassA@__init__)
test_heap_reference_monotone.py(5, 0): ✅ pass - (ClassA@__init__ requires) Type constraint of n
test_heap_reference_monotone.py(6, 0): ✅ pass - (ClassA@__init__ requires) Type constraint of n
test_heap_reference_monotone.py(11, 0): ✅ pass - assert(128)
unknown location: ✅ pass - Heap reference counter monotone (__main__)
DETAIL: 5 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
3 changes: 2 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_method_call_with_kwargs.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,5 +5,6 @@ test_method_call_with_kwargs.py(8, 0): ✅ pass - (MyClass@__init__ requires) Ty
test_method_call_with_kwargs.py(9, 0): ✅ pass - (MyClass@some_method requires) Type constraint of ip1
test_method_call_with_kwargs.py(9, 0): ✅ pass - (MyClass@some_method requires) Type constraint of ip2
test_method_call_with_kwargs.py(9, 0): ✅ pass - (MyClass@some_method requires) Type constraint of ip3
DETAIL: 7 passed, 0 failed, 0 inconclusive
unknown location: ✅ pass - Heap reference counter monotone (__main__)
DETAIL: 8 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
4 changes: 3 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
test_method_kwargs_no_hierarchy.py(2, 4): ✅ pass - Heap reference counter monotone (Calculator@__init__)
test_method_kwargs_no_hierarchy.py(5, 41): ❓ unknown - (Calculator@add ensures) Return type constraint
test_method_kwargs_no_hierarchy.py(9, 4): ✅ pass - (Calculator@__init__ requires) Type constraint of base
unknown location: ✅ pass - assert_assert(0)_calls_Any_get_or_none_0
Expand All @@ -7,6 +8,7 @@ test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - (Calculator@add requires)
test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - (Calculator@add requires) Type constraint of y
test_method_kwargs_no_hierarchy.py(11, 4): ✅ pass - assert(254)
test_method_kwargs_no_hierarchy.py(12, 4): ❓ unknown - assert(286)
test_method_kwargs_no_hierarchy.py(8, 0): ✅ pass - Heap reference counter monotone (main)
test_method_kwargs_no_hierarchy.py(8, 14): ✅ pass - (main ensures) Return type constraint
DETAIL: 8 passed, 0 failed, 2 inconclusive
DETAIL: 10 passed, 0 failed, 2 inconclusive
RESULT: Inconclusive
5 changes: 4 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_with_statement.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,12 @@
test_with_statement.py(17, 4): ✔️ always true if reached - assert(364)
test_with_statement.py(20, 4): ✔️ always true if reached - assert(426)
test_with_statement.py(15, 0): ✔️ always true if reached - Heap reference counter monotone (test_with_as)
test_with_statement.py(25, 8): ✔️ always true if reached - assert(525)
test_with_statement.py(26, 8): ✔️ always true if reached - assert(558)
test_with_statement.py(22, 0): ✔️ always true if reached - Heap reference counter monotone (test_with_no_as)
test_with_statement.py(32, 21): ✔️ always true if reached - Check PAdd exception
test_with_statement.py(32, 8): ✔️ always true if reached - assert(697)
test_with_statement.py(33, 8): ✔️ always true if reached - assert(724)
DETAIL: 7 passed, 0 failed, 0 inconclusive
test_with_statement.py(28, 0): ✔️ always true if reached - Heap reference counter monotone (test_with_multiple)
DETAIL: 10 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
6 changes: 5 additions & 1 deletion StrataTest/Languages/Python/expected_laurel/test_with_void_enter.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,8 @@
test_with_void_enter.py(2, 4): ✅ pass - Heap reference counter monotone (VoidManager@__init__)
test_with_void_enter.py(5, 4): ✅ pass - Heap reference counter monotone (VoidManager@__enter__)
test_with_void_enter.py(8, 4): ✅ pass - Heap reference counter monotone (VoidManager@__exit__)
test_with_void_enter.py(14, 8): ✅ pass - assert(272)
test_with_void_enter.py(15, 4): ✅ pass - assert(287)
DETAIL: 2 passed, 0 failed, 0 inconclusive
test_with_void_enter.py(11, 0): ✅ pass - Heap reference counter monotone (test_void_enter)
DETAIL: 6 passed, 0 failed, 0 inconclusive
RESULT: Analysis success
1 change: 1 addition & 0 deletions StrataTest/Languages/Python/run_py_analyze_sarif.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@
"test_dict_operations",
"test_for_loop",
"test_func_input_type_constraints",
"test_heap_reference_monotone",
"test_if_elif",
"test_ifexpr",
"test_list",
Expand Down
11 changes: 11 additions & 0 deletions StrataTest/Languages/Python/tests/test_heap_reference_monotone.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
class ClassA:
def __init__(self, n: int):
self.val : int = n

a1 = ClassA(1)
a2 = ClassA(2)

a1.val = 1
a2.val = 2

assert a1.val != a2.val
Comment thread
thanhnguyen-aws marked this conversation as resolved.
Loading