Runtime checks - #1452

Draft

cedihegi wants to merge 49 commits into

viperproject:masterfrom

cedihegi:runtime-checks

Commits on Apr 12, 2023

Override built_mir method to have mutable access to mir
cedihegi
committed
01923a9

Commits on May 1, 2023

Change a single assertion to test output
cedric
committed
613db71

Commits on Aug 1, 2023

Add runtime checks for preconditions and insert them in MIR
cedihegi
committed
531842a
Fix the problem of introducing loops in CFG when modifying it.
cedihegi
committed
9dc1072
Check postconditions too and handle result
cedihegi
committed
d4cbd89
Handle old operator in runtime checks
cedihegi
committed
2ecdda6
Make postconditions with old expressions checkable at runtime
cedihegi
committed
393748c
Runtime check support for quantifiers, old stores and postconditions
cedihegi
committed
00d47fc
Add option, to provide boundaries for quantifier runtime checks manually
cedihegi
committed
61355c2
Fix bug with mem forget

cedric
authored and
cedihegi
committed
a4ce18b
Interpret moved values in postconditions as old values too

cedric
authored and
cedihegi
committed
8001fe5
Now able to insert runtime checks for pledges.
cedihegi
committed
4759f3b
Add runtime checks for pledges
cedihegi
committed
0351d45
Fix a bug for runtime checks
cedihegi
committed
fafabe0
Runtime checks for prusti_assert and prusti_assume
cedihegi
committed
96807d6
Working old checks in prusti_assume, assert etc.

cedric
authored and
cedihegi
committed
823e766
Re-organized runtime check structure a bit, remove warnings
cedihegi
committed
107ef3b
Only clone arguments for old if they are mutable
cedihegi
committed
17b73d7
Runtime checks without store function for old values
cedihegi
committed
3c82745
Fix check signature mutability issues with runtime checks
cedihegi
committed
ec781ae
Insert drops for manually cloned MIR locals
cedihegi
committed
a6daab3
Merge remote-tracking branch 'upstream/master' into runtime-checks
cedihegi
committed
ddcf67c

Commits on Aug 5, 2023

Refactor runtime checks
cedihegi
committed
a3b88e0

Commits on Aug 6, 2023

Add boolean guards for pledge checks
cedric
committed
b276862

Commits on Aug 9, 2023

Optmization based on verification and reachability
cedihegi
committed
6f089cd

Commits on Aug 16, 2023

Pledges without annotations and Dead Code Eliminiation
cedihegi
committed
4bff3d6

Commits on Aug 17, 2023

Fix pledge checks in case of zombie loans
cedihegi
committed
f3ec99b

Commits on Aug 20, 2023

Remove unneeded assertions and checked operations
cedihegi
committed
98c0317
cleanup changes that are no longer required
cedihegi
committed
066ecc5

Commits on Aug 21, 2023

Undo accidental formatting
cedihegi
committed
bcbb303

Commits on Aug 25, 2023

syncing! override by amending!
cedihegi
committed
a4891c9

Commits on Aug 26, 2023

merging with master
cedihegi
committed
8300225
Fix tests, add option to always insert runtime checks
cedihegi
committed
351e9fa

Commits on Aug 28, 2023

Add flags for runtime checks debugging
cedric
committed
be5482c

Commits on Sep 1, 2023

Extend error reporting of runtime checks
cedihegi
committed
294884b
Add tests for runtime checks and optimizations
cedihegi
committed
d3cacc7

Commits on Sep 6, 2023

Add better error messages to runtime checks
cedihegi
committed
4a0f5b6
Run formatting
cedihegi
committed
de67aa4
Refactoring and resolving clippy warnings
cedihegi
committed
2fbeed9

Commits on Sep 10, 2023

Stop std feature from importing prusti-specs
cedihegi
committed
f4aa968
Merge remote-tracking branch 'upstream/master' into runtime-checks
cedihegi
committed
04e66dd

Commits on Sep 11, 2023

Document, refactor and explain with comments
cedihegi
committed
ae80faa

Commits on Sep 12, 2023

Add runtime checks for predicates
cedihegi
committed
bd3b3dd

Commits on Sep 13, 2023

More comments, documentation and a test for predicate
cedihegi
committed
5c05f2e

Commits on Sep 18, 2023

Update predicates and predicate checking + other things
cedihegi
committed
2e8fb1e

Commits on Sep 20, 2023

Add new flags to dev-guide
cedihegi
committed
2f5d8e6

Commits on Sep 22, 2023

Merge remote-tracking branch 'upstream/master' into runtime-checks
cedihegi
committed
5cfb19a

Commits on Oct 9, 2023

Remove prints, add comments, slight adjustment of old_values
cedihegi
committed
2c92e1a

Commits on Oct 26, 2023

Small changes and fixes
cedihegi
committed
6279743