Fixes

Author: keyboardDrummer

Strata/Languages/Laurel/HeapParameterization.lean

@@ -98,12 +98,9 @@ def analyzeProc (proc : Procedure) : AnalysisResult :=
   let bodyResult := match proc.body with
     | .Transparent b => (collectExprMd b).run {} |>.2
     | .Opaque postconds impl modif =>
-        -- A non-empty modifies clause (excluding wildcard `*`) implies the procedure
-        -- reads and writes the heap; no need to inspect the body further in that case.
-        -- Wildcard modifies does not imply heap access — it only suppresses the frame condition.
-        let isWildcard (e : StmtExprMd) : Bool := match e.1 with | .All => true | _ => false
-        let concreteModifies := modif.filter (fun e => !isWildcard e)
-        if !concreteModifies.isEmpty then
+        -- A non-empty modifies clause implies the procedure reads and writes the heap;
+        -- no need to inspect the body further in that case.
+        if !modif.isEmpty then
           { readsHeapDirectly := true, writesHeapDirectly := true, callees := [] }
         else
           let r1 := postconds.foldl (fun (acc : AnalysisResult) (pc : Condition) =>

Strata/Languages/Python/PythonToLaurel.lean

@@ -2455,11 +2455,7 @@ def PreludeInfo.ofLaurelProgram (prog : Laurel.Program) : PreludeInfo where
     prog.staticProcedures.filterMap fun p =>
       if p.body.isExternal || p.isFunctional then none else some p.name.text
   inlinableProcedures :=
-    prog.staticProcedures.foldl (init := {}) fun s p =>
-      match p.body with
-      | .Transparent _ => s.insert p.name.text
-      | .Opaque _ (some _) _ => s.insert p.name.text
-      | _ => if !p.preconditions.isEmpty then s.insert p.name.text else s
+    prog.staticProcedures.foldl (init := {}) fun s p => s.insert p.name.text
 
 /-- Merge two `PreludeInfo` values by concatenating each field. -/
 def PreludeInfo.merge (a b : PreludeInfo) : PreludeInfo where

StrataTest/Languages/Python/expected_laurel/test_class_decl.expected

@@ -1,3 +1,3 @@
-test_class_decl.py(9, 4): ✅ pass - callElimAssert_requires_15
+test_class_decl.py(9, 4): ✅ pass - (CircularBuffer@__init__ requires) Type constraint of n
 DETAIL: 1 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success