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

Regnant crashes on simple null check assertion. #7

Open
aigarashi opened this issue Sep 18, 2021 · 0 comments
Open

Regnant crashes on simple null check assertion. #7

aigarashi opened this issue Sep 18, 2021 · 0 comments
Labels
bug Something isn't working

Comments

@aigarashi
Copy link
Contributor

When we pass the following Java code into regnant:

public class NullCheck {
    public static void main(String[] args){
        String s = null;
        assert(s != null);
    }
}

The current implementation of regnant will output code which looks like this:

NullCheck_main(){
  ifnull null then {
    fail;
  }else{
    return 0
  }
}

{ NullCheck_main() }

ifnull null seems to be the cause of the error.
However, modifying the semantics of ConSORT seems to mess with ownership and may cause issues.

Modifying how ConditionExpr gets treated with null literals in regnant (src/main/java/edu/kyoto/fos/regnant/translation/Translate.java ) outputs the following ConSORT:

NullCheck_main(){
  {
    fail;
    return 0
  }

}

{ NullCheck_main() }

This also fails with line 2, col 2 in file mono.imp: Dead code.
There's probably a better way to generate the code when we hit this case so that we don't generate the "dead code".

@aigarashi aigarashi added the bug Something isn't working label Sep 18, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

1 participant