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

Trace generation #330

Merged
merged 100 commits into from
Dec 2, 2024
Merged

Trace generation #330

merged 100 commits into from
Dec 2, 2024

Conversation

leventeBajczi
Copy link
Contributor

No description provided.

AdamZsofi added 30 commits June 13, 2022 15:05
@AdamZsofi
Added basic dfs trace generator; not tested yet
5e7b522
@AdamZsofi
tracgen half-done, but ran into some issues; refactor next
24e9ef6
@AdamZsofi
no propert concretizer in progress
b1c120d
@AdamZsofi
Writing generated traces into files
a709678
@AdamZsofi
minor changes
585c62a
@AdamZsofi
Generating maximal traces from xsts
0ad3ac9
@AdamZsofi
Deleted some commented code
c9bccbf
@AdamZsofi
Fixed xsts based bug generating extra traces
9d103eb
@AdamZsofi
Added temporary ARG to file to cegarchecker
130fcdf
@AdamZsofi
Started adding advanced arg trace for trace generation
cd6504c
@AdamZsofi
iterative trace lengthening works on small example
4a4018c
@AdamZsofi
Added get full traces as an option
5df7980
@AdamZsofi
Cleaning up tracegen code
9ed5b22
@AdamZsofi
Refactored full trace generation
0675afb
@AdamZsofi
Adding configurable initial precision
af92d1c
@AdamZsofi
Added some trace gen options
fc2b102
@AdamZsofi
Shortened tracegen algorithm code
8b6db64
@AdamZsofi
Fixed accidentally changed code
5225be8
@AdamZsofi
Patched tracegen feasibility check
d8d0731
@AdamZsofi
Patched xsts specific superfluous node removal
4a9ac61
@AdamZsofi
Patch superfluous node filtering
3c40481
@AdamZsofi
minor fix
b263b0f
@AdamZsofi
Fixed typo in shortened trace containment check
f3f79a6
@AdamZsofi
Added heuristics for incomplete abstract state coverages
750291e
@AdamZsofi
added correct check inbetween abstract states
b553dd6
@AdamZsofi
Fixed typo
7a959fd
@AdamZsofi
Added insecure delete to google recursive delete for windows
8e97f22
@AdamZsofi @leventeBajczi
Added basic dfs trace generator; not tested yet
008e6a5
@AdamZsofi @leventeBajczi
tracgen half-done, but ran into some issues; refactor next
7215db1
@AdamZsofi @leventeBajczi
no propert concretizer in progress
1f92802
AdamZsofi added 20 commits October 7, 2024 17:07
@AdamZsofi
summary concretization and least/most over approx arg node wip
b7df932
@AdamZsofi
working on summary concretization
077c7bf
@AdamZsofi
added feasible concretization and concrete summary
22d2896
@AdamZsofi
clean up some templates
a581e5f
@AdamZsofi
adding summary statuses
50672da
@AdamZsofi
basic summary concretization works
ef4ee50
@AdamZsofi
.cexs can exported, but todos for tracegen with abstraction still pre…
7c13253 
…sent
@AdamZsofi
wip tracegen to xcfa
aabe64e
@AdamZsofi
Merge branch 'master' into trace-generation
8cc79dc
@AdamZsofi
tracegen added to xcfa execute config
5520360
@AdamZsofi
xcfa-cli trace generation can be built, but not tested
e412918
@AdamZsofi
fix config node result type
74d3be7
@AdamZsofi
added some post tracegen log
6c110d3
@AdamZsofi
added trace concretizations to xcfa tracegen
8f7a3b9
@AdamZsofi
Merge branch 'master' into trace-generation
7e987e8
@AdamZsofi
reformatting after merge
21e7acf
@AdamZsofi
add _ in cexs node id
e3503f3
@AdamZsofi
added options to (not) get summary/trace set after tracegen for xsts
506f776
@AdamZsofi
added options to (not) get summary/trace set after tracegen for xsts
000ebfb
@AdamZsofi
fixed --traces and --summary in xsts cli
ec1a632
@leventeBajczi leventeBajczi changed the base branch from master to xta-to-xcfa-experiment December 2, 2024 13:01
@github-actions GitHub Actions
Copy link

github-actions bot commented Dec 2, 2024

❗ Please run ./gradlew spotlessApply on your branch to fix copyright headers.

@github-actions GitHub Actions
Copy link

github-actions bot commented Dec 2, 2024

❗ Please run ./gradlew spotlessApply on your branch to fix formatting.

@github-actions GitHub Actions
Copy link

github-actions bot commented Dec 2, 2024

❗ Please modify build.gradle.kts to contain a later version than 6.8.6. Current version is 6.8.6.

@leventeBajczi leventeBajczi marked this pull request as ready for review December 2, 2024 13:53
@leventeBajczi leventeBajczi merged commit 0fd5bbe into xta-to-xcfa-experiment Dec 2, 2024
45 of 79 checks passed
@leventeBajczi leventeBajczi deleted the trace-generation branch December 2, 2024 13:53
@leventeBajczi leventeBajczi restored the trace-generation branch December 2, 2024 13:54
@github-actions GitHub Actions
Copy link

github-actions bot commented Dec 2, 2024

Benchexec test report for a selection of SV-Benchmarks (correct / incorrect / all):

Rundefinition BOUNDED CEGAR HORN
SV-COMP25_no-data-race ❓ (0 / 0 / 415) HTML/CSV ✅ (50 / 0 / 120) HTML/CSV ❓ (0 / 0 / 415) HTML/CSV
SV-COMP25_no-overflow ✅ (30 / 0 / 310) HTML/CSV ✅ (30 / 0 / 307) HTML/CSV ✅ (29 / 0 / 292) HTML/CSV
SV-COMP25_termination ✅ (2 / 0 / 346) HTML/CSV ✅ (11 / 0 / 240) HTML/CSV ✅ (20 / 0 / 406) HTML/CSV
SV-COMP25_unreach-call ✅ (6 / 0 / 192) HTML/CSV ✅ (24 / 0 / 108) HTML/CSV ❗ (19 / 1 / 191) HTML/CSV
SV-COMP25_valid-memcleanup ❓ (0 / 0 / 65) HTML/CSV ❓ (0 / 0 / 65) HTML/CSV ❓ (0 / 0 / 65) HTML/CSV
SV-COMP25_valid-memsafety ❓ (0 / 0 / 452) HTML/CSV ❗ (32 / 2 / 374) HTML/CSV ✅ (8 / 0 / 434) HTML/CSV

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
@leventeBajczi @AdamZsofi