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

HoareTripleChecker based on abstract post for Taipan #109

Closed
danieldietsch opened this issue Feb 13, 2017 · 0 comments
Closed

HoareTripleChecker based on abstract post for Taipan #109

danieldietsch opened this issue Feb 13, 2017 · 0 comments
Assignees
@danieldietsch @greitsch
Labels
abstract interpretation enhancement

Comments

@danieldietsch
Copy link
Member

danieldietsch commented Feb 13, 2017 •
edited
Loading

No description provided.

@danieldietsch danieldietsch self-assigned this Feb 13, 2017
danieldietsch added a commit that referenced this issue Feb 15, 2017
@danieldietsch
see #109 -- use variable provider to make states compatible during ho…
b5970ef 
…are triple check
danieldietsch added a commit that referenced this issue Feb 15, 2017
@danieldietsch
see #109 -- remaining bugs
be9902a
danieldietsch added a commit that referenced this issue Feb 15, 2017
@danieldietsch
see #109 -- fix AbsIntPredicate equals method (fixes PredicateUnifier…
eb3ec56 
… bug), remove method from basic predicate factory (not appropriate anymyore) , better logging for AbsIntHoareTripleChecker
danieldietsch added a commit that referenced this issue Feb 15, 2017
@danieldietsch
see #109 -- fix equals() bug in AbsIntPredicate
f46ddf7
danieldietsch added a commit that referenced this issue Feb 15, 2017
@danieldietsch
see #109 -- also report invalid
21f9078
danieldietsch added a commit that referenced this issue Feb 15, 2017
@danieldietsch
see #109 -- current fails
5de9907
danieldietsch added a commit that referenced this issue Feb 20, 2017
@danieldietsch
see #109 -- fix bug by always using post variables
9441526
danieldietsch added a commit that referenced this issue Feb 20, 2017
@danieldietsch
see #109 -- add soundness checks to absint htc
e7f71b8
danieldietsch added a commit that referenced this issue Feb 20, 2017
@danieldietsch
towards #109 -- sync
9bccfcb
danieldietsch added a commit that referenced this issue Feb 20, 2017
@danieldietsch
see #109 -- fix remaining soundness error in absint htc
3b29bbe
danieldietsch added a commit that referenced this issue Mar 21, 2017
@danieldietsch
see #109 -- added additional debug logging
27d561c
danieldietsch added a commit that referenced this issue Mar 23, 2017
@danieldietsch
see #109 -- add inductivity check for absint hoare triple checker
2b2ce53
danieldietsch added a commit that referenced this issue Mar 28, 2017
@danieldietsch
see #109 -- fix bug in call handling of AbsIntHoareTripleChecker
110ccf3
danieldietsch added a commit that referenced this issue Mar 28, 2017
@danieldietsch
see #109 -- some refactoring
e72d8e6
danieldietsch added a commit that referenced this issue Apr 2, 2017
@danieldietsch
see #82, see #109 -- use IcfgEdge when possible (path programs have i…
c82ae08 
…cfgedges), use getLabel() when old CodeBlocks are required, annotate BoogieIcfgContainer on itself (and not on Unit)

 * this removes the need for the boogiesymboltable and the old ISymbolTableAdapter workaround
 * this removes support for projecting path programs and requires the new path program structure
 * create new variable provider for AbsIntHoareTripleChecker (cannot reuse the one from fxpe computation because it has the symbol table of the path program)
 * remove some unnecessary fields
 * use getLabel() in result reporter
 * consider path program during interpolant generation (word alone is not enough, transitions are the ones from the path program)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@danieldietsch danieldietsch

@greitsch greitsch

Labels
abstract interpretation enhancement
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@danieldietsch @greitsch