Skip to content

Fix if condition with no refinement#210

Open
CatarinaGamboa wants to merge 4 commits intomainfrom
cond-true-fix
Open

Fix if condition with no refinement#210
CatarinaGamboa wants to merge 4 commits intomainfrom
cond-true-fix

Conversation

@CatarinaGamboa
Copy link
Copy Markdown
Collaborator

Before:
When the guard condition had no refinement, we used the default of true.
That, however, became a problem after joining ifs (with no else), since we assumed the condition was true.

Now:
We still create new fresh boolean but leave it empty, leaving the verification to the SMT solver.
We also remove the branches that cannot complete normally from the If joining (return, throw, break, continue).
(This can still be improved if Latte was used.)

Example:

  String loadFirstSetting(String path, String fallback) throws IOException {                                                         
      BufferedReader reader = new BufferedReader(new FileReader(path));                                                              
      String header = reader.readLine();        // reader: open                                                                      
                                                                                                                                     
      if (header.startsWith("#")) {             // condition has no refinement                                                       
          String value = reader.readLine();     // reader: still open                                                                
          reader.close();                       // reader: closed                                                                    
          return value;                                                                                                              
      }
      // Before: State Refinement Error here — the join assumed the                                                         
      //         then-branch was taken, so reader was seen as `closed` and the                                                       
      //         close() below failed its `!closed` precondition.                                                                    
      // Now:    the then-branch returns and contributes nothing to the join,                                                        
      //         so reader is still `open` and the close() is accepted.                                                                                                                 
      reader.close();                           // reader: closed
      return header;
  }

@CatarinaGamboa CatarinaGamboa requested a review from rcosta358 May 7, 2026 14:02
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.

2 participants