Support specification-constructs in Pallas specifications#1289

Draft

RobertMensing wants to merge 14 commits intodevfrom integrate-llvm-spec-translation

+1,131-156

Commits on Dec 4, 2024

First draft of supporting \result in Pallas specifications
RobertMensing
committed
Fix bug where return-argument gets added to wrapper of pallas requires-clause
RobertMensing
committed

Commits on Dec 5, 2024

Support for \return with structs in pallas specifications (no yet working, due to missing type inference)
RobertMensing
committed
Fixed error when using Pallas contracts with \result and sret functions.
RobertMensing
committed

Commits on Dec 6, 2024

Use sret for type-inference and infer types of LLVM function-args.
RobertMensing
committed

Commits on Dec 11, 2024

Infer correct type for LLVMResult
RobertMensing
committed

Commits on Dec 14, 2024

Remove redundant *& when encoding LLVM-store and add permissions for sret-param
RobertMensing
committed

Commits on Dec 17, 2024

Extract statement-to-expression from PureMethodsToFunctions
RobertMensing
committed

Commits on Jan 7, 2025

First draft for inlining pallas wrappers
RobertMensing
committed

Commits on Jan 9, 2025

Commits on Jan 10, 2025