Closed APotyomkin closed 2 years ago
[] > test [] > parent [self x] > f x.sub 5 > t seq > @ assert (0.less t) x [self y1] > g self.f self y1 > @ [self y2] > gg self.g self y2 > @ [self y3] > ggg self.gg self y3 > @ [self z] > h z > @ [] > child test.parent > @ [self y] > f y > @ [self z] > h self.ggg self z > @
RESULT BY AnOdin: [Unjustified Assumption] Method g is not referentially transparent
RESULT BY AnOdin: Odin is not able to analyze the code, due to: Symbol value-of-before-f not declared
I suppose that it is somehow related to a length of a calls chain.(not confirmed based on #36) With shortened chain, it works well.
[] > test [] > parent [self x] > f x.sub 5 > t seq > @ assert (0.less t) x [self y1] > g self.f self y1 > @ [self y2] > gg self.g self y2 > @ [self z] > h z > @ [] > child test.parent > @ [self y] > f y > @ [self z] > h self.gg self z > @
@Leosimetti as discussed, we need to use define-funs-rec to enable (mutually) recursive definitions of function values and function properties.
define-funs-rec
Problematic code
Expected result
Actual result
Assumption
I suppose that it is somehow related to a length of a calls chain.(not confirmed based on #36) With shortened chain, it works well.Code
Results