Skip to content

DEP: New form of WP without partitioning #385

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
Open
rasoolmaghareh wants to merge 76 commits into
base: master
Choose a base branch
from
Open

DEP: New form of WP without partitioning #385

rasoolmaghareh wants to merge 76 commits into from

Conversation

@rasoolmaghareh
Copy link
Member

@rasoolmaghareh rasoolmaghareh commented Feb 1, 2023

No description provided.

rasoolmaghareh and others added 30 commits April 1, 2021 22:25
@rasoolmaghareh
Adding only wp-interpolant check
e3b0ff9
@rasoolmaghareh
Undoing partitioning in TxWeakestPreCondition::updateSubsumptionTable…
90e57c1 
…Entry
@sanghu1790
Removed the first return statement from -getFunctionArgument()- funct…
2eb4e39 
…ion in TxWP.cpp file l.no.:615
@sanghu1790
Modified the TxWP.cpp by removing few return statements from function…
52a4e0a 
… getConstantExp, getBinaryInst, and getCmpCondition
@sanghu1790
removed the changes done in return statement of function --getCmpCond…
a01477d 
…ition-- of TxWP.cpp
@sanghu1790
added a check in --getFunctionArgument(llvm::Argument *arg)-- funtion
3d455a4
@sanghu1790
Print updates
0e971cc
@sanghu1790
Function argument mapping
150d455
@ArpitaDutta
.settings
1966a0f
@ArpitaDutta
nano.save
3c2d669
@ArpitaDutta
Release+Asserts
abaa839
@ArpitaDutta
Release+Asserts files added
386fb51
@ArpitaDutta
Mapping of function arguments by checking their correct index value
b08780c
@ArpitaDutta
updated supporting files
d485876
@ArpitaDutta
Assigning name to the unnamed llvm instructions with --TX_named_var--
1afe28c
@ArpitaDutta
Added some print statements
c2a5949
@rasoolmaghareh
Adding back deletion interpolation and partitioning
411178a
@ArpitaDutta
Deleted the file from the Debug+Assert
a227cbe
@ArpitaDutta
Deleted print statements
0b3f847
@ArpitaDutta
Merge branch 'new-wpinterpolant' of https://github.com/tracer-x/klee …
16301a3 
…into new-wpinterpolant
@ArpitaDutta
add updated files
96760b9
@ArpitaDutta
Deleted Release+Assert folder
8018301
@ArpitaDutta
removed files from lib/core/Debug+Asserts and lib/Solver/Debug+Asserts
ecb7fc3
@ArpitaDutta
removed files from lib/Baisc/Debug+Asserts and lib/Baisc/Release+Asserts
c8e051d
@ArpitaDutta
removed files from lib/Module/Debug+Asserts and lib/Module/Release+As…
1b7b72c 
…serts
@ArpitaDutta
removed files from lib/Core/Release+Assert/* and lib/Expr/Debug+Asser…
dd56d89 
…ts/*
@ArpitaDutta
removed files from lib/Expr/Release+Asserts/*
43f59fd
@ArpitaDutta
Deleted unwanted files
372ba04
@rasoolmaghareh
removing build files
8731f59
@rasoolmaghareh
removing other unwanted files
71b5619
ArpitaDutta and others added 22 commits June 27, 2022 23:19
@ArpitaDutta
supporting trunc instruction in TxWeakestPreCondition::getCondition()
54a059a
@ArpitaDutta
Fix in Partitioning for Global Variables
e328dd8
@ArpitaDutta
Fixed Global Variable Partitioning
2579aef
@ArpitaDutta
Int64 support added for FunctionArgumentSize
6831a10
@ArpitaDutta
Int64 support added for getGlobalVariabletSize
6db7823
@ArpitaDutta
Int64 support added for getGepSize
08deff5
@ArpitaDutta
Fixed empty if statement warnings
bb51926
@ArpitaDutta
Added array and pointer type support for getCastInst
7cc560b
@ArpitaDutta
Fix in getFunctionArgument()
44ebb0c
@ArpitaDutta
Checking the historical store
f3446cc
@ArpitaDutta
commented the block info and other unwanted print statements
da405c7
@ArpitaDutta
Global variable fix
b830321
@ArpitaDutta
Fix in miu closure
b447140
@ArpitaDutta @rasoolmaghareh
Commented few print statements for better readability
ca2ecbe
@sanghu1790 @rasoolmaghareh
Commented few print statements for better readability
b9ba43e
@sanghu1790 @rasoolmaghareh
Printing Block Info for Subsumption Table Entry
6090339
@sanghu1790 @rasoolmaghareh
added debugSubsumptionLevel as a function parameter
9d0e7c6
@ArpitaDutta @rasoolmaghareh
Create Sample.c
54af174
@ArpitaDutta @rasoolmaghareh
Add files via upload
db33402
@ArpitaDutta @rasoolmaghareh
Smoke Test file update
05abf21
@ArpitaDutta @rasoolmaghareh
Add files via upload
6db4088
@rasoolmaghareh
Removing partitioning
a6be554
@rasoolmaghareh rasoolmaghareh force-pushed the newInterpolantNoPartition branch from c9cea6a to a6be554 Compare February 1, 2023 15:30
@rasoolmaghareh rasoolmaghareh changed the title New form of WP without partitioning Experimental: New form of WP without partitioning Apr 25, 2023
@rasoolmaghareh
Copy link
Member Author

rasoolmaghareh commented Apr 25, 2023

We have found that some over-subsumption in some of the programs

@rasoolmaghareh rasoolmaghareh changed the title Experimental: New form of WP without partitioning DEP: New form of WP without partitioning Jun 26, 2023
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.

4 participants

@rasoolmaghareh @sanghu1790 @ArpitaDutta