viktormalik / 2ls Goto Github PK
View Code? Open in Web Editor NEWThis project forked from diffblue/2ls
Static Analyzer and Verifier
Home Page: http://www.cprover.org/2LS
License: Other
This project forked from diffblue/2ls
Static Analyzer and Verifier
Home Page: http://www.cprover.org/2LS
License: Other
When trying to analyze the following example:
#include <stdlib.h>
extern int __VERIFIER_nondet_int(void);
struct list{
struct list* next;
};
int main()
{
struct list *p,*q;
p = malloc(sizeof(struct list));
q = malloc(sizeof(struct list));
p->next = malloc(sizeof(struct list));
p = q;
while(__VERIFIER_nondet_int) {
q = p->next;
q->next = malloc(sizeof(struct list));
p->next = q->next;
}
return 1;
}
2ls ends up with this assertion error:
2ls: strategy_solver_heap.cpp:141: virtual bool strategy_solver_heapt::iterate(strategy_solver_baset::invariantt&): Assertion `to_address_of_expr(ptr_value).object().id()==ID_symbol' failed.
currently, we transform an assignment with memory access at right hand side into SSA as follows:
a = p->next (original assignment in C/GOTO program)
a#cur-loc == p'obj.next#last-loc (SSA equality where cur-loc is the current location and last-loc is the location of the last assignment of p'obj.next)
this transformation is done by method local_SSAt::build_transfer
we check whether p'obj.next has been defined before (function all_symbolic_deref_called at line 469 in local_ssa.cpp)
but we also need to check whether p has not changed since last assignment of p'obj.next, because that would make p'obj.next invalid
in that case, we would have to use actual abstract object on the heap (dynamic_object$0.next) instead - this can be obtained by calling the function local_SSAt::dereference on p->next
I'd suggest including this check into build_transfer function
maybe it would be enough to check whether last definition of pointer p is before the last definition o p'obj.next - this information can be retrieved from ssa_analysis, for inspiration see all_symbolic_deref_defined (question is, is this really sound?)
retrieving pointer p from object p'obj should be possible using functions from ssa_pointed_objects.h, particularly get_pointer
merge into heap branch
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.