Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
1 change: 1 addition & 0 deletions Strata/Languages/Laurel/DatatypeGrouping.lean
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@ def collectTypeRefs : HighTypeMd → List String
collectTypeRefs base ++ args.flatMap collectTypeRefs
| ⟨.Pure base, _⟩ => collectTypeRefs base
| ⟨.Intersection ts, _⟩ => ts.flatMap collectTypeRefs
| ⟨.TCore name, _⟩ => [name]
| _ => []

/-- Get all datatype names that a `DatatypeDefinition` references in its constructor args. -/
Expand Down
1 change: 1 addition & 0 deletions Strata/Languages/Python/PythonToLaurel.lean
Original file line number Diff line number Diff line change
Expand Up @@ -255,6 +255,7 @@ def wrapFieldInAny (ty : HighType) (expr : StmtExprMd) : Except TranslationError
| .TFloat64 => .ok <| mkStmtExprMd (.StaticCall "from_float" [expr])
| .TReal => .ok <| mkStmtExprMd (.StaticCall "from_float" [expr])
| .TString => .ok <| mkStmtExprMd (.StaticCall "from_string" [expr])
| .TCore "Any" => .ok expr
| other => .error (.typeError s!"wrapFieldInAny: no Any constructor for field type '{repr other}'")

/-- Look up a field's HighType, returning `none` if the class or field is not found. -/
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@

==== Verification Results ====
List_get_body_calls_List_get_0: ✅ pass
List_take_body_calls_List_take_0: ✅ pass
List_drop_body_calls_List_drop_0: ✅ pass
List_slice_body_calls_List_drop_0: ✅ pass
List_slice_body_calls_List_take_1: ✅ pass
List_set_body_calls_List_set_0: ✅ pass
DictStrAny_get_body_calls_DictStrAny_get_0: ✅ pass
Any_get_body_calls_DictStrAny_get_0: ✅ pass
Any_get_body_calls_List_get_1: ✅ pass
Any_get_body_calls_List_slice_2: ✅ pass
Any_get_body_calls_List_drop_3: ✅ pass
Any_get!_body_calls_DictStrAny_get_0: ✅ pass
Any_get!_body_calls_List_get_1: ✅ pass
Any_set_body_calls_List_set_0: ✅ pass
Any_set!_body_calls_List_set_0: ✅ pass
PFloorDiv_body_calls_Int.SafeDiv_0: ✅ pass
PFloorDiv_body_calls_Int.SafeDiv_1: ✅ pass
PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass
PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass
PAnd_body_calls_Any_to_bool_0: ✅ pass
POr_body_calls_Any_to_bool_0: ✅ pass
ret_type: ✅ pass (in prelude file)
ret_type: ✅ pass (in prelude file)
ret_pos: ✅ pass (in prelude file)
assert_name_is_foo: ✅ pass (in prelude file)
assert_opt_name_none_or_str: ✅ pass (in prelude file)
assert_opt_name_none_or_bar: ✅ pass (in prelude file)
ensures_maybe_except_none: ✅ pass (in prelude file)
2 changes: 1 addition & 1 deletion StrataTest/Languages/Python/run_py_analyze_sarif.py
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@

BOTH_SKIP = {"test_foo_client_folder", "test_invalid_client_type", "test_unsupported_config"}
SKIP_TESTS = BOTH_SKIP | {"test_class_field_use", "test_list", "test_subscription", "test_with_statement", "test_class_field_init", "test_break_continue", "test_try_except", "test_try_except_scoping", "test_loops",
"test_augmented_assign", "test_list_slice"} # sarif pipeline uses PythonToCore which doesn't yet support AugAssign
"test_augmented_assign", "test_list_slice", "test_class_field_any"} # sarif pipeline uses PythonToCore which doesn't yet support AugAssign
SKIP_TESTS_LAUREL = BOTH_SKIP


Expand Down
5 changes: 5 additions & 0 deletions StrataTest/Languages/Python/tests/test_class_field_any.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
class MyClass:
def __init__(self, some_field):
self.some_field: Any = some_field

c = MyClass([1,2])
Loading