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.

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

Annotations rebased #193

Open
wants to merge 91 commits into
base: master
Choose a base branch
from
Open

Annotations rebased #193

wants to merge 91 commits into from

Conversation

Dspil
Copy link
Collaborator

@Dspil Dspil commented May 8, 2022

This PR introduces the static analysis that characterizes certain parts of the ASTs of functions as safe or unsafe to prune them from the concolic testing search.

aggelgian and others added 30 commits January 19, 2022 15:21
Store original specs in kmodule

Get mfas to specs mappings

debug commit xxx

added spec checker, updated kfun api

added update of kmodules

added fixpoint computation, ready to change annotating function

kmodule updates

unification changes

Bugfix at updating kmodule

add cuter_maybe_error annotation

added the dynamic check

bugfix

updated cuter spec checker

unreachable clauses analysis

corrected module loading by xref

support opaque type declarations

Changed isForced flag to Options map. Pruning is now clever

removed obsolete functions from cuter_log

Support records in function spec and type extraction

added some unit tests for the static ananlysis

corrected unit tests, multiple spec functions discarded

Updated unreachable clauses logic

added dynamic type dependent function call and apply check

Bugfix

bugfix in type from pattern

removed unnecessary uncallable state

deleted trash code

fix point type passing

removed obsolete functions
aggelgian and others added 28 commits February 15, 2022 08:53
@Dspil Dspil requested review from aggelgian and kostis May 9, 2022 07:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants