Skip to content

Asn1#294

Open
gewlar wants to merge 158 commits intomasterfrom
asn1
Open

Asn1#294
gewlar wants to merge 158 commits intomasterfrom
asn1

Conversation

@gewlar
Copy link
Copy Markdown
Collaborator

@gewlar gewlar commented Mar 22, 2026 •
edited by marcoeilers
Loading

This PR adds support for:

  • Bytearray & PByteSeq
  • Dataclasses
  • IntEnum
  • left and right bit shift
  • int.bit_length
  • String format
  • Timeout argument for benchmarks
  • Preprocessing mode for single file

This change is Reviewable

gewlar and others added 30 commits September 10, 2025 11:12
@gewlar
add build folder to gitingore
3c9ad83
@gewlar
Start working on bytearray implementation
0204b54
@gewlar
Merge remote-tracking branch 'origin/master' into asn1
4682cc3
@gewlar
Print name of unsupported function
612d0cd
@gewlar
Trying call extension
9fdbca8 
Just some work in progress
@gewlar
Working implementation for empty bytearray constructor
f2465f0
@gewlar
Working bytearray from bytearray and append method
86db8f3 
bytearray from list of ints fails
@gewlar
Extending bytearray support
10439f5
@gewlar
Add special predicate for access to bytearray
bd4517c
@gewlar
Implement Iterator for bytearray
7edab59
@gewlar
Update builtins.json
e9d7133
@gewlar
Add lshift to bitwise operations
9160e1e
@gewlar
Adjust error messages for bytearray bounds
0fd24d6
@gewlar
Get __initFromList__ working
9480b7b
@gewlar
Clean up call.py
e0d18e1
@gewlar
Add tests for bytearray
27365c6
@gewlar
Fix Low conditions
32dbda1
@gewlar
Extend bytearray tests
c0ef41c
@gewlar
Add tests for lshift and fix negative inputs
c66ffae
@gewlar
fix: spelling mistake
93689d9
@gewlar
Add dummy implementation for formatted strings
45f5531
@gewlar
Partial support for right shift
8b369b1
@gewlar
Disable right shift of negative numbers
bbe4219
@marcoeilers
Attempting to enable Unfold statements in pure functions
6a83817
@gewlar
Merge remote-tracking branch 'origin/master' into asn1
d5d4ed1
@gewlar
Merge remote-tracking branch 'origin/unfold_in_pure_functions' into asn1
27b9290
@gewlar
Checking type of assign during _assign_with_subscript
dd5af62 
Fixes #237
@gewlar
Ignore sign bit for bitvector operations
921418b
@gewlar
Adjust tests for larget bitsize
dba26d2
@gewlar
Add eq content check for bytearray
b60a507
gewlar and others added 30 commits February 17, 2026 14:41
@gewlar
Rename IntEnum __unbox__ to __int__ and register as viper function
ccd2655
@gewlar
More dataclass tests
49625cc
@gewlar
Improve dataclass decorator handling
b6ef671
@gewlar
Support field with default_factory=list for dataclass
e49a8b5
@gewlar
Use value equality handling for lists
c2af5a0
@gewlar
Add tests for contained list of dataclasses
6261b4a
@gewlar
Extend list equality check
3ba9f0a
@gewlar
Add test for desired property
a24c8f2
@marcoeilers
Trying out using simplified e1 in e2.list_acc expressions only in tri…
a52d420 
…ggers, not in lhs of quantifier bodies
@marcoeilers
Adding test
4ebb655
@marcoeilers
Fixing crashes
91b4c44
@marcoeilers
Doing the same for existentials
db80e6c
@marcoeilers
Test for existentials, some comments to explain what's happening
4537ac4
@marcoeilers
Using both expressions as triggers
2e68745
@gewlar
Fix failing tests
709e3a4
@marcoeilers
Trying stuff
8763511
@marcoeilers
Fixing things
66d4be1
@gewlar
Additional trigger for __seq_ref_to_seq_int
fee7e79
@gewlar
Merge remote-tracking branch 'origin/master' into asn1
fe19cb9
@gewlar
Merge remote-tracking branch 'origin/master' into asn1
1769f8c 
# Conflicts:
#	src/nagini_translation/resources/builtins.json
#	src/nagini_translation/resources/references.sil
#	src/nagini_translation/sif/resources/all.sil
#	src/nagini_translation/sif/resources/builtins.json
@marcoeilers
Merge branch 'master' into trying_trigger_stuff
eab1071
@gewlar
Merge remote-tracking branch 'origin/trying_trigger_stuff' into asn1
f4573eb
@gewlar
Add argument for time limit to benchmark
84ac73c
@gewlar
Use threads for benchmark to reliably stop them
a305167
@gewlar
Accumulate benchmark results
a098731
@gewlar
Fix name overwrite in benchmark
1860395 
(cherry picked from commit 23a4762)
@marcoeilers
Fixing let expression crash
e6b837c
@gewlar
Add support for non-frozen dataclasses
c697778 
Failing tests are due to list triggers
@gewlar
Merge remote-tracking branch 'origin/trying_trigger_stuff' into asn1
b60e75d
@gewlar
Revert "Fixing things"
ea43a7e 
This reverts commit 66d4be1.

Revert "Trying stuff"

This reverts commit 8763511.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@gewlar @marcoeilers