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

Define String, SConst, StringLit, and associated funcs #29

Closed
wants to merge 5 commits into from
Closed

Define String, SConst, StringLit, and associated funcs #29

wants to merge 5 commits into from

Commits on Jun 18, 2020

  1. Define String, SConst, StringLit, and associated funcs 

    Translate CPure SConst only for z3.ml and smtsolver.ml
All other provers call failwith() or illegal() when translating
    @zhengqunkoo
    zhengqunkoo committed Jun 18, 2020
    Configuration menu
    Copy the full SHA
    b4777ef View commit details
    Browse the repository at this point in the history

  2. Translate TInt(IChar), autogenerate char_star with char field

    @zhengqunkoo
    zhengqunkoo committed Jun 18, 2020
    Configuration menu
    Copy the full SHA
    9ef31b7 View commit details
    Browse the repository at this point in the history

  3. Expand subtyping, allow assignments char *s = "..."

    @zhengqunkoo
    zhengqunkoo committed Jun 18, 2020
    Configuration menu
    Copy the full SHA
    59a8606 View commit details
    Browse the repository at this point in the history

  4. Support checking of SConst expressions

    @zhengqunkoo
    zhengqunkoo committed Jun 18, 2020
    Configuration menu
    Copy the full SHA
    5aaba1e View commit details
    Browse the repository at this point in the history

Commits on Jun 19, 2020

  1. Try to force variable s to only be type String

    @zhengqunkoo
    zhengqunkoo committed Jun 19, 2020
    Configuration menu
    Copy the full SHA
    60392cb View commit details
    Browse the repository at this point in the history