Support 4-6 argument function applications in GOTO backend - #1430

Closed

keyboardDrummer-bot wants to merge 119 commits into

strata-org:removeFunctionsfrom

keyboardDrummer:fix-cbmc-nary-app

Commits on Jun 16, 2026

Per-invariant source ranges for loop-invariant diagnostics (#1361)
kadirayk
authored
24b8f04
Code review
keyboardDrummer
committed
878f325
Fix early return
keyboardDrummer
committed
e0c8b68
Fix lifting bug
keyboardDrummer
committed
a63384a
Merge remote-tracking branch 'origin/reviewed-kbd-will-merge-to-main' into issue-924-contract-and-proof-pass
keyboardDrummer
committed
02ad82c
Merge branch 'issue-924-contract-and-proof-pass' into removeFunctions
keyboardDrummer
committed
edbfda1
Add comment
keyboardDrummer
committed
16f57e6
feat(laurel): Adding surface syntax for calling instance procedures & lowering to Core (#1328)

AD1024
and
olivier-aws
authored
4d3cbac
Merge remote-tracking branch 'origin/reviewed-kbd-will-merge-to-main' into issue-924-contract-and-proof-pass
keyboardDrummer
committed
799f167

Commits on Jun 17, 2026

Fixes
keyboardDrummer
committed
ced5837
Fixes
keyboardDrummer
committed
952a8e6
Fix to contract pass and test expectations
keyboardDrummer
committed
ceeb050
Fix in lifting pass
keyboardDrummer
committed
f7eef03
Fix tests
keyboardDrummer
committed
6767211
Add extra test to T2_ImpureExpressions
keyboardDrummer
committed
2df41be
update test
keyboardDrummer
committed
3459035
Drop info output in tests
keyboardDrummer
committed
5c87a7f
Fixes
keyboardDrummer
committed
6c78979
Add test-case to T2
keyboardDrummer
committed
e98598f
Fix to lift pass
keyboardDrummer
committed
1c78fe1
Add local variable inlining pass
keyboardDrummer
committed
bcdef57
Remove tmp file
keyboardDrummer
committed
6f7b93d
Merge branch 'issue-924-contract-and-proof-pass' into removeFunctions
keyboardDrummer
committed
23eca53
Remove more info output
keyboardDrummer
committed
f82910a
Update Python files
keyboardDrummer
committed
7ab0725
fix(laurel): datatype `==`/`!=` mis-lowered to reference comparison in heap-writing procedures (#1349)

fabiomadge
and
ssomayyajula
authored
0c99354
update for Python
keyboardDrummer
committed
5c4a0b6

Commits on Jun 18, 2026

Port fixes to lifting pass
keyboardDrummer
committed
83e793b
Merge branch 'reviewed-kbd-will-merge-to-main' into issue-924-contract-and-proof-pass
keyboardDrummer
authored
6e0ce93
Add type checking to Laurel resolution pass (#1121)

authored
9c40e44
Merge remote-tracking branch 'origin/reviewed-kbd-will-merge-to-main' into issue-924-contract-and-proof-pass
keyboardDrummer
committed
e1fc044
Some fixes for resolution during phases
keyboardDrummer
committed
dcfb0e9
Fixes to resolution so it throws fewer errors during passes
keyboardDrummer
committed
a0ec015
Emit resolution errors during passes
keyboardDrummer
committed
25f1d5d
Source fix
keyboardDrummer
committed
fa7f844
Improve well-formedness of the 3 heap passes
keyboardDrummer
committed
441ec1e
Fix for type hierarchy
keyboardDrummer
committed
cf706b2
Refactoring
keyboardDrummer
committed
66589c5
Allow dangling addition in blocks
keyboardDrummer
committed
903f89e
Fix diagnostic and test
keyboardDrummer
committed
1a0e8ae
Remove function return type expectation check
keyboardDrummer
committed
018939b
Update resolver check to use procedure instead of function
keyboardDrummer
committed
8d34b32
Small improvements
keyboardDrummer
committed
d9b39ac
Merge branch 'issue-924-contract-and-proof-pass' of github.com:keyboardDrummer/Strata into issue-924-contract-and-proof-pass
keyboardDrummer
committed
a24cc86
Merge branch 'fixResolutionErrorsDuringPhases' into issue-924-contract-and-proof-pass
keyboardDrummer
committed
c438d8c
Fix merge
keyboardDrummer
committed
fcb3903
Remove obsolete test
keyboardDrummer
committed
4efaebd
fix(laurel): Run LiftInstanceProcedure before EliminateValueInReturns (#1381)
olivier-aws
authored
45784fa
File-relative error reporting (#1367)

leo-leesco
and
claude
authored
925423b

Commits on Jun 19, 2026

Fix resolution errors during phases (#1389)

keyboardDrummer
and
keyboardDrummer-bot
authored
81f20ab
Add multi output test-case to ImpureExpressions
keyboardDrummer
committed
8ce6fc6
Merge remote-tracking branch 'origin/reviewed-kbd-will-merge-to-main' into issue-924-contract-and-proof-pass
keyboardDrummer
committed
157ec6b
Refactor liftImperative
keyboardDrummer
committed
d7a4c3c
Simplify lift pass
keyboardDrummer
committed
0b03bff
Bring back test
keyboardDrummer
committed
97e3146
Recursion proof refactoring
keyboardDrummer
committed
ffcc39d
Fix proofs
keyboardDrummer
committed
1ef148f

Commits on Jun 20, 2026

laurel: wire old() to Core two-state semantics (#1203)

authored
0abd9ef

Commits on Jun 22, 2026

Merge remote-tracking branch 'origin/reviewed-kbd-will-merge-to-main' into issue-924-contract-and-proof-pass
keyboardDrummer
committed
a279ff7
Cleanup
keyboardDrummer
committed
34c850f
Fix
keyboardDrummer
committed
12b5e59
Fix test
keyboardDrummer
committed
bfc0b6c
Fix tests
keyboardDrummer
committed
2e2a7b3
Update expect file
keyboardDrummer
committed
5f46178
fix(laurel) : incorrect reporting of mismatched annotation location (#1401)

leo-leesco
and
claude
authored
a6e0cee
fix(core): isolate path conditions at the procedure boundary (#1391)
fabiomadge
authored
064e019

Commits on Jun 23, 2026

Merge branch 'issue-924-contract-and-proof-pass' into removeFunctions
keyboardDrummer
committed
98b76bc
returnLabel match_pattern
keyboardDrummer
committed
f1cb6c4
Fix warning
keyboardDrummer
committed
4e9173a
feat(laurel): add body-tested do-while loop (#1358)
fabiomadge
authored
2c8eaa1
Fixes
keyboardDrummer
committed
ed51271
Fixes
keyboardDrummer
committed
bfd1750
Test fixes
keyboardDrummer
committed
823add6
feat(laurel): paren-free field ++/--, and chained-field-access test coverage (#1382)
fabiomadge
authored
8d6aa98
Fix to lift pass
keyboardDrummer
committed
d4aba94
[Laurel] Support constrained types as composite fields (#1364)

authored
6a074b1
Merge remote-tracking branch 'origin/reviewed-kbd-will-merge-to-main' into issue-924-contract-and-proof-pass
keyboardDrummer
committed
16be9b5
Undo added test and fix related to that
keyboardDrummer
committed
97870a3
Enable calling procedures in contracts (#1352)

authored
49c3e1a

Commits on Jun 24, 2026

Merge branch 'issue-924-contract-and-proof-pass' into removeFunctions
keyboardDrummer
committed
7abd32d
Fixes
keyboardDrummer
committed
04da456
Fixes
keyboardDrummer
committed
01f0f75
Mute overly verbose test
keyboardDrummer
committed
5270ab1
Merge commit '49c3e1aac6' into removeFunctions
keyboardDrummer
committed
090aa9c
While related fixes
keyboardDrummer
committed
7c653f7
Add test and fix for lift imperative pass
keyboardDrummer
committed
89051e1
Improve Python debugging
keyboardDrummer
committed
8d765fa
Fix IncrDecr lift test
keyboardDrummer
committed
c76ffd9
Fix py_interpret failures after removing isFunctional
keyboardDrummer-bot
committed
2b66b97

Commits on Jun 25, 2026

Laurel: avoid quantified modifies frames when using array theory (#1374)

authored
0a4a29b

Commits on Jun 26, 2026

Attempted fix
keyboardDrummer
committed
a3345b6
Update some expect files
keyboardDrummer
committed
b75d3ad
Merge remote-tracking branch 'origin/reviewed-kbd-will-merge-to-main' into removeFunctions
keyboardDrummer
committed
805d546
Add missing save
keyboardDrummer
committed
4ef42d2
Fix merge
keyboardDrummer
committed
1e6dae6
Fix contract pass asserting free postconditions in body
keyboardDrummer-bot
committed
39a29e4

Commits on Jun 27, 2026

Turn the alwaysCallFunctions flag on again for Python
keyboardDrummer
committed
1f2543b

Commits on Jun 29, 2026

mapConst changes
keyboardDrummer
committed
8c5e13d
Fixes
keyboardDrummer
committed
620593f
Fix T2c/T2d test failures: disable alwaysCallCoreFunctions for array-theory modifies tests
keyboardDrummer-bot
committed
0221896
Revert "Fix T2c/T2d test failures: disable alwaysCallCoreFunctions for array-theory modifies tests"
keyboardDrummer
committed
816382a
Fix T2c/T2d test failures: exclude heap-output procs from function redirection
keyboardDrummer-bot
committed
2bcd810
Revert "Fix T2c/T2d test failures: exclude heap-output procs from function redirection"
keyboardDrummer
committed
f897209
Call procedure when interpreting
keyboardDrummer
committed
b3cac0b
Fix return in PythonToLaurel, and related things
keyboardDrummer
committed
9349000
Get rid of bodyLabel
keyboardDrummer
committed
dc8d8f4
Test updates
keyboardDrummer
committed
fce801d
More test changes
keyboardDrummer
committed
9320e88
Remove bad bodylabel reference
keyboardDrummer
committed
7205c4c
Fix modifiesClauses
keyboardDrummer
committed
07a4dab
Update tests
keyboardDrummer
committed
d149221
Update test
keyboardDrummer
committed
3c5b8c5
Fix
keyboardDrummer
committed
d3e7594
Revert "Fix"
keyboardDrummer
committed
582937b
Fix related to holes and Core's behavior around empty procedures
keyboardDrummer
committed
d6be6e8
Fix warning
keyboardDrummer
committed
1f5b8f2
Update expect files
keyboardDrummer
committed
b1fb519
Fix run_py_interpret.sh: use wildcard assertion IDs in expected files
keyboardDrummer-bot
committed
b46ab22
Support 4-6 argument function applications in GOTO backend
keyboardDrummer-bot
committed
8a3bbe4