Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Slhv encoding #7

Merged
merged 133 commits into from
Oct 11, 2024
Merged

Slhv encoding #7

merged 133 commits into from
Oct 11, 2024

Conversation

SpencerL-Y
Copy link
Owner

No description provided.

zhuyutian57 and others added 30 commits July 10, 2024 17:39
@zhuyutian57
update slhv encoding and refactor
db24bfa
@zhuyutian57
heap update encoding
617aec2
@zhuyutian57
finish encoding(pending for locadd)
e4c7df9
@zhuyutian57
encoding and dump smt2
f4d7d55
@SpencerL-Y
add tests
596fde0
@SpencerL-Y
Merge branch 'slhv_encoding' of github.com:SpencerL-Y/esbmc into slhv…
63a952b 
…_encoding
@zhuyutian57
add z3-slhv dec_check
5c843a9
@SpencerL-Y
add print smt, using --output
adaa3f7
@SpencerL-Y
update
f63115a
@zhuyutian57
update
f004652
@zhuyutian57
make hvar and lvar via specific api
da171cb
@zhuyutian57
use z3_conv get_bool
1c1df80
@zhuyutian57
adjust to byte-level points-to
06d8caf
@SpencerL-Y
update
c9ce912
@zhuyutian57
write vccs and its smt formulas in file
ec27cb3
@zhuyutian57
add symex_assign on heap_load = val
6850b76
@zhuyutian57
set default points-to bytes(4)
293124d
@SpencerL-Y
add definition of heap append
52cc112
@SpencerL-Y
add create value for heap append
734fb5c
@zhuyutian57
add encoding of heap_append and slicing
460c196
@SpencerL-Y
update for merge
e754e5e
@SpencerL-Y
Merge branch 'slhv_encoding' of github.com:SpencerL-Y/esbmc into slhv…
f5b3ed7 
…_encoding
@SpencerL-Y
add heap free
e56a982
@SpencerL-Y
add heap delete
481c3a6
@SpencerL-Y
add heap delete, change bug check encoding
8e148f3
@zhuyutian57
heap_delete encoding
581e99e
@zhuyutian57
add slicing
1e9bbd0
@zhuyutian57
add heap_region and adjust some exprs for SLHV
1335839
@zhuyutian57
encoding same_object in SLHV
82e49f7
@zhuyutian57
update
739a605
zhuyutian57 and others added 29 commits September 28, 2024 15:45
@zhuyutian57
support alloca
373c014
@zhuyutian57
update svcomp script
e71d340
@zhuyutian57
remove pthread program
00d1d4a
@zhuyutian57
fix: removing pthread
8c21b86
@zhuyutian57
encoding dead semantic in SLHV
d777778
@zhuyutian57
fix alignment
d0ed292
@zhuyutian57
remove padded field and record its width
4bd4267
@zhuyutian57
fix if expr in pt
8667aac
@zhuyutian57
fix ite in pt
e71c108
@zhuyutian57
fix script typo
0414e1d
@zhuyutian57
update script
98196d7
@zhuyutian57
calculate totaltime for each case
db41e67
@zhuyutian57
support loc2int
4caf359
@zhuyutian57
update script
1ae4e49
@zhuyutian57
disable building error trace
cbb29bb
@zhuyutian57
update x.py for running esbmc
d8a8635
@zhuyutian57
support constant struct
7d48529
@zhuyutian57
support location_of a stack variable
65bb089
@zhuyutian57
fix renaming location_of
8af081d
@zhuyutian57
fix disjointness
9c3a044
@zhuyutian57
support struct assignment
cc7efe6
@zhuyutian57
update x.py
62a03d1
@zhuyutian57
add statistic of atomic heap terms
347852a
@zhuyutian57
save aht svg correctly
a4a2533
@zhuyutian57
add theory solving statistics
025a44d
@zhuyutian57
add bench-0125
f121f00
@SpencerL-Y
stage for merge
9424186
@SpencerL-Y
Merge branch 'slhv_encoding' of github.com:SpencerL-Y/esbmc into slhv…
e5bcfc3 
…_encoding
@SpencerL-Y
merge with main
4936e4c
@SpencerL-Y SpencerL-Y merged commit ce56bb7 into main Oct 11, 2024
4 of 10 checks passed
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
@SpencerL-Y @zhuyutian57